Lecture Notes: First-Order Logic - Model Checking, Satisfiability, and the Domino Problem

Author

Your Name

Published

February 5, 2025

Introduction

This lecture delves into the algorithmic aspects of first-order logic, with a particular emphasis on the complexity of the model checking and satisfiability problems. We will investigate how the semantics of first-order logic can be systematically translated into concrete algorithms. A significant portion of our discussion will address the challenges that arise when dealing with infinite universes. Furthermore, we will introduce the domino problem, also known in the literature as the tiling problem. We will demonstrate its undecidability by establishing a reduction from the well-known halting problem. The primary objectives of this lecture are twofold: to gain a thorough understanding of the computational facets of first-order logic and to acquire the skills necessary to prove the undecidability of a given problem.

Review of Key Concepts

It is crucial to have a firm grasp of the examples discussed in previous lectures. These examples serve as crucial illustrations of fundamental concepts. In particular, pay close attention to those demonstrating:

The concept of "infinitely many."
The quantificational patterns "there exists for all" ($\exists \forall$) and "for all there exists" ($\forall \exists$).

Furthermore, understanding how to represent a string or any function mapping into a finite co-domain through partitioning into unary relations is essential. This technique provides a powerful tool for translating complex structures into a format amenable to logical analysis. Mastering these concepts will provide a solid foundation for the material covered in this lecture.

Algorithms for First-Order Logic

We will now discuss algorithms for first-order logic, focusing on the model checking and satisfiability problems.

Model Checking Problem

The model checking problem is generally the simplest problem to solve for a logic. Given a formula $\phi$ and a structure $\mathcal{M}$, the task is to evaluate whether $\mathcal{M} \models \phi$, that is, whether the formula holds true over the structure, using the semantics of the formalism.

Consider a formula $\phi$ in first-order logic and a structure $\mathcal{M} = (U, \{R_i\}, \{c_j\})$ containing a universe $U$, relations $R_i$, and constants $c_j$. Let $s$ be an assignment function that maps variables to elements in $U$. To evaluate $\phi$ over $\mathcal{M}$ with assignment $s$, we proceed by induction on the structure of $\phi$:

Base Case (Atomic Statement): If $\phi$ is an atomic statement, e.g., $R(x_1, \dots, x_k)$, where $R$ is a relational symbol and $x_1, \dots, x_k$ are variables, we look up the relation $R^{\mathcal{M}}$ corresponding to $R$ in $\mathcal{M}$ and the objects $s(x_1), \dots, s(x_k)$ corresponding to the variables. We check if the tuple $(s(x_1), \dots, s(x_k))$ belongs to the relation $R^{\mathcal{M}}$. If it does, we return true; otherwise, we return false.
Boolean Connectives:
- For $\phi = \neg \psi$, we return true if the recursive call on $\psi$ returns false, and vice-versa.
- For $\phi = \psi_1 \land \psi_2$, we return true if both recursive calls on $\psi_1$ and $\psi_2$ return true; otherwise, we return false.
- For $\phi = \psi_1 \lor \psi_2$, we return true if at least one of the recursive calls on $\psi_1$ and $\psi_2$ returns true; otherwise, we return false.
Existential Quantification: For a formula $\phi = \exists x \psi(x)$, we recursively call the model checking procedure on $\psi(x)$ with the structure $\mathcal{M}$ and the assignment $s'$ which is the same as $s$ except that $s'(x) = u$, for each object $u$ in the universe $U$. If any call returns true, we return true; otherwise, we return false.
Universal Quantification: For a formula $\phi = \forall x \psi(x)$, we recursively call the model checking procedure on $\psi(x)$ with the structure $\mathcal{M}$ and the assignment $s'$ which is the same as $s$ except that $s'(x) = u$, for each object $u$ in the universe $U$. If all calls return true, we return true; otherwise, we return false.

Input: A first-order formula $\phi$, a structure $\mathcal{M} = (U, \{R_i\}, \{c_j\})$, and an assignment $s$. Output: True if $\mathcal{M}, s \models \phi$, False otherwise.

$R^{\mathcal{M}} \gets$ the relation corresponding to $R$ in $\mathcal{M}$ $(s(x_1), \dots, s(x_k)) \in R^{\mathcal{M}}$ not and or $s' \gets s[x \mapsto u]$ True False $s' \gets s[x \mapsto u]$ False True

Challenges with Infinite Universes

Algorithm [alg:model-checking] faces challenges when the universe $U$ is infinite. For instance, if $U = \mathbb{N}$, the set of natural numbers, iterating over all elements (lines 12 and 19) is impossible, leading to non-termination.

Issue: The algorithm assumes a finite universe. An infinite universe leads to non-termination.
Possible Solution: If the structure is provided explicitly, it must be finite by definition. The problem arises when the structure is given implicitly, such as through a set of axioms or a generative process.

Handling Infinite Strings

Consider the infinite string $AAB, AAB, AAB, \dots$. We can represent it implicitly as $(AAB)^\omega$. For such periodic strings, we can use heuristics to avoid checking all positions. For instance, we might check only the first period and then infer the truth value for the entire string based on its periodicity.

Complexity of Model Checking

Propositional Logic: Model checking is in P (polynomial time).
QBF: Model checking is PSPACE-complete (polynomial space complete).
First-Order Logic: Model checking is PSPACE-complete.

The model checking algorithm for first-order logic (Algorithm [alg:model-checking]) runs in polynomial space. Each recursive call expands the structure by a constant amount (binding one variable), and the number of these expansions is at most the number of quantifiers in the formula, which is linear in the size of the formula. Thus, the space used by the expanded structure is polynomial in the size of the formula. The depth of the recursion is also linear in the size of the formula. Therefore, the total space used is polynomial. Moreover, the problem is PSPACE-hard because QBF, a PSPACE-complete problem, can be reduced to first-order logic model checking. Hence, first-order logic model checking is PSPACE-complete.

Satisfiability Problem

The satisfiability problem for first-order logic is significantly harder than for QBF. It involves finding not just the variable assignments but also the universe and relations that make the formula true. In other words, given a formula $\phi$, we need to find a structure $\mathcal{M}$ such that $\mathcal{M} \models \phi$.

Consider the formula $\phi(x, y) = \forall z (A(x, z) \implies \exists t (B(t, y) \land C(x)))$. The satisfiability problem asks if there exists a structure $\mathcal{M} = (U, A^{\mathcal{M}}, B^{\mathcal{M}}, C^{\mathcal{M}})$ and an assignment $s$ such that $\mathcal{M}, s \models \phi$. This requires specifying the universe $U$ and the interpretations of the predicates $A$, $B$, and $C$.

Undecidability of Satisfiability

(Trakhtenbrot, 1950) The satisfiability problem for first-order logic is undecidable. This means there is no algorithm that can solve the satisfiability problem for all first-order formulas.

Proof Idea: Reduction from the Halting Problem

To prove undecidability, we can reduce the halting problem to the satisfiability problem.

Halting Problem: Given a Turing machine $M$ and an input $w$, does $M$ halt on $w$? (Here we consider the case where $w$ is the empty string)
Reduction: Map a Turing machine $M$ to a first-order formula $\phi_M$ such that $M$ halts on an empty tape if and only if $\phi_M$ is satisfiable.

If such a reduction exists, and since the halting problem is undecidable, it follows that the satisfiability problem for first-order logic is also undecidable.

The Domino Problem (Tiling Problem)

The domino problem, also known as the tiling problem, is a classic decision problem in computer science and mathematics. It asks, given a finite set of tile types, whether it is possible to tile an infinite plane or a rectangle of unknown size using these tiles, subject to certain constraints.

Problem Definition

Input: A finite set $T$ of tiles, where each tile is a square with colored edges. Formally, each tile $t \in T$ can be represented as a tuple $t = (c_1, c_2, c_3, c_4)$, where $c_1, c_2, c_3, c_4$ are the colors of the top, right, bottom, and left edges, respectively.
Rules:
1. Tiles cannot be rotated. They must be placed in the orientation they are given.
2. Adjacent edges of neighboring tiles must have matching colors.
3. We have an infinite number of copies of each tile type.
4. The borders of the rectangle must be a specific color (e.g. color 0)
Question: Does there exist a rectangle of any size (with borders of color 0) that can be completely tiled with the given tiles, adhering to the specified rules? Formally, does there exist a positive integers $m, n$ and a function $f: \{1, \dots, m\} \times \{1, \dots, n\} \to T$ such that the tiling is valid according to the rules?

Suppose we are given the following set of tiles, where the colors are represented by numbers:

The question is: can we tile a rectangle of unknown size such that adjacent edges match in color, and the border is color 0?

Undecidability of the Domino Problem

The domino problem is undecidable. This means that there is no algorithm that can correctly determine, for any given set of tiles, whether a valid tiling exists. We will sketch a proof of this by reducing the halting problem to the domino problem.

Reduction from the Halting Problem to the Domino Problem

We will outline a two-step reduction strategy:

Reduce the halting problem to the domino problem.
Reduce the domino problem to the satisfiability problem for first-order logic.

The first step is the core of the argument, while the second step is a more general connection between computability and logic.

Reduction Idea: Map a Turing machine $M$ to a set of tiles $T_M$ such that $M$ halts on an empty tape if and only if there exists a tiling of a rectangle of unknown size (with borders of color 0) with tiles from $T_M$.

Intuition for the Reduction

The tiles in $T_M$ are constructed such that any valid tiling of a rectangle corresponds to a computation history of the Turing machine $M$. Each row in the tiling represents a configuration of the Turing machine at a specific time step. The colors and symbols on the tiles encode the state of the Turing machine, the contents of its tape, and the position of the tape head. The transition rules of the Turing machine are encoded in the color-matching rules of the tiles.

Missing Detail: The specific construction of tiles $T_M$ from the Turing machine $M$ is not detailed in this lecture. This is a crucial part of the reduction and will be elaborated on in the next lecture.
Suggestion: The tiles should be designed to meticulously encode the transition rules of the Turing machine. This ensures that adjacent tiles in a valid tiling represent valid transitions of the Turing machine. For example, if the machine in state $q$ reads symbol $a$ and transitions to state $q'$, writing symbol $b$ and moving right, there should be a tile that enforces this transition in the tiling.

Illustration of how a tiling can represent the computation of a Turing machine. Each row represents a configuration of the machine at a given time step. The colored squares represent the state of the machine and the head position. The symbols represent the tape contents. The halting state is (q_H).

Conclusion

In this lecture, we delved into the intricacies of the model checking and satisfiability problems within the realm of first-order logic. We navigated the challenges posed by infinite universes and established that the model checking problem is PSPACE-complete. We also examined Trakhtenbrot’s seminal result, which states that the satisfiability problem for first-order logic is undecidable. To further illuminate the concept of undecidability, we introduced the domino problem and outlined a strategy for proving its undecidability by means of a reduction from the halting problem.

Key Takeaways

Model checking for first-order logic is PSPACE-complete.
Satisfiability for first-order logic is undecidable.
The domino problem is undecidable and serves as a powerful tool for proving the undecidability of other problems.

Follow-up Questions

How can we systematically construct tiles from a given Turing machine to execute the reduction from the halting problem to the domino problem? (This will be a central focus of the next lecture.)
What are the practical implications of the undecidability of the satisfiability problem for first-order logic in real-world applications, such as program verification and automated reasoning?
Can we explore other variants of the domino problem, such as those with different boundary conditions or tiling regions, and analyze their respective computational complexities?

For the next lecture, we will delve deeper into the reduction from the halting problem to the domino problem, providing a detailed explanation of the tile construction process, as mentioned in Section 4.2.2. We will also discuss the broader implications of these undecidability results in more detail, connecting them to practical concerns in computer science and logic.

--- title: "Lecture Notes: First-Order Logic - Model Checking, Satisfiability, and the Domino Problem" author: "Your Name" date: "2025-02-05" format: html: toc: true # Table of Contents toc-depth: 2 code-tools: true theme: cosmo # Or "journal" for Distill-like minimalism --- # Introduction This lecture delves into the algorithmic aspects of first-order logic, with a particular emphasis on the complexity of the **model checking** and **satisfiability** problems. We will investigate how the semantics of first-order logic can be systematically translated into concrete algorithms. A significant portion of our discussion will address the challenges that arise when dealing with infinite universes. Furthermore, we will introduce the **domino problem**, also known in the literature as the **tiling problem**. We will demonstrate its undecidability by establishing a reduction from the well-known **halting problem**. The primary objectives of this lecture are twofold: to gain a thorough understanding of the computational facets of first-order logic and to acquire the skills necessary to prove the undecidability of a given problem. # Review of Key Concepts It is crucial to have a firm grasp of the examples discussed in previous lectures. These examples serve as crucial illustrations of fundamental concepts. In particular, pay close attention to those demonstrating: - The concept of \"infinitely many.\" - The quantificational patterns \"there exists for all\" ($\exists \forall$) and \"for all there exists\" ($\forall \exists$). Furthermore, understanding how to represent a string or any function mapping into a finite co-domain through partitioning into unary relations is essential. This technique provides a powerful tool for translating complex structures into a format amenable to logical analysis. Mastering these concepts will provide a solid foundation for the material covered in this lecture. # Algorithms for First-Order Logic We will now discuss algorithms for first-order logic, focusing on the **model checking** and **satisfiability** problems. ## Model Checking Problem The model checking problem is generally the simplest problem to solve for a logic. Given a formula $\phi$ and a structure $\mathcal{M}$, the task is to evaluate whether $\mathcal{M} \models \phi$, that is, whether the formula holds true over the structure, using the semantics of the formalism. ::: tcolorbox []{#ex:model-checking label="ex:model-checking"} Consider a formula $\phi$ in first-order logic and a structure $\mathcal{M} = (U, \{R_i\}, \{c_j\})$ containing a universe $U$, relations $R_i$, and constants $c_j$. Let $s$ be an assignment function that maps variables to elements in $U$. To evaluate $\phi$ over $\mathcal{M}$ with assignment $s$, we proceed by induction on the structure of $\phi$: - **Base Case (Atomic Statement)**: If $\phi$ is an atomic statement, e.g., $R(x_1, \dots, x_k)$, where $R$ is a relational symbol and $x_1, \dots, x_k$ are variables, we look up the relation $R^{\mathcal{M}}$ corresponding to $R$ in $\mathcal{M}$ and the objects $s(x_1), \dots, s(x_k)$ corresponding to the variables. We check if the tuple $(s(x_1), \dots, s(x_k))$ belongs to the relation $R^{\mathcal{M}}$. If it does, we return true; otherwise, we return false. - **Boolean Connectives**: - For $\phi = \neg \psi$, we return true if the recursive call on $\psi$ returns false, and vice-versa. - For $\phi = \psi_1 \land \psi_2$, we return true if both recursive calls on $\psi_1$ and $\psi_2$ return true; otherwise, we return false. - For $\phi = \psi_1 \lor \psi_2$, we return true if at least one of the recursive calls on $\psi_1$ and $\psi_2$ returns true; otherwise, we return false. - **Existential Quantification**: For a formula $\phi = \exists x \psi(x)$, we recursively call the model checking procedure on $\psi(x)$ with the structure $\mathcal{M}$ and the assignment $s'$ which is the same as $s$ except that $s'(x) = u$, for each object $u$ in the universe $U$. If any call returns true, we return true; otherwise, we return false. - **Universal Quantification**: For a formula $\phi = \forall x \psi(x)$, we recursively call the model checking procedure on $\psi(x)$ with the structure $\mathcal{M}$ and the assignment $s'$ which is the same as $s$ except that $s'(x) = u$, for each object $u$ in the universe $U$. If all calls return true, we return true; otherwise, we return false. ::: ::::: tcolorbox []{#alg:model-checking label="alg:model-checking"} :::: algorithm ::: algorithmic **Input:** A first-order formula $\phi$, a structure $\mathcal{M} = (U, \{R_i\}, \{c_j\})$, and an assignment $s$. **Output:** True if $\mathcal{M}, s \models \phi$, False otherwise. $R^{\mathcal{M}} \gets$ the relation corresponding to $R$ in $\mathcal{M}$ $(s(x_1), \dots, s(x_k)) \in R^{\mathcal{M}}$ not and or $s' \gets s[x \mapsto u]$ True False $s' \gets s[x \mapsto u]$ False True ::: :::: ::::: ### Challenges with Infinite Universes Algorithm [\[alg:model-checking\]](#alg:model-checking){reference-type="ref" reference="alg:model-checking"} faces challenges when the universe $U$ is infinite. For instance, if $U = \mathbb{N}$, the set of natural numbers, iterating over all elements (lines 12 and 19) is impossible, leading to non-termination. - **Issue**: The algorithm assumes a finite universe. An infinite universe leads to non-termination. - **Possible Solution**: If the structure is provided explicitly, it must be finite by definition. The problem arises when the structure is given implicitly, such as through a set of axioms or a generative process. ### Handling Infinite Strings ::: tcolorbox Consider the infinite string $AAB, AAB, AAB, \dots$. We can represent it implicitly as $(AAB)^\omega$. For such periodic strings, we can use heuristics to avoid checking all positions. For instance, we might check only the first period and then infer the truth value for the entire string based on its periodicity. ::: ### Complexity of Model Checking - **Propositional Logic**: Model checking is in **P** (polynomial time). - **QBF**: Model checking is **PSPACE**-complete (polynomial space complete). - **First-Order Logic**: Model checking is **PSPACE**-complete. ::: tcolorbox The model checking algorithm for first-order logic (Algorithm [\[alg:model-checking\]](#alg:model-checking){reference-type="ref" reference="alg:model-checking"}) runs in polynomial space. Each recursive call expands the structure by a constant amount (binding one variable), and the number of these expansions is at most the number of quantifiers in the formula, which is linear in the size of the formula. Thus, the space used by the expanded structure is polynomial in the size of the formula. The depth of the recursion is also linear in the size of the formula. Therefore, the total space used is polynomial. Moreover, the problem is PSPACE-hard because QBF, a PSPACE-complete problem, can be reduced to first-order logic model checking. Hence, first-order logic model checking is PSPACE-complete. ::: ## Satisfiability Problem The satisfiability problem for first-order logic is significantly harder than for QBF. It involves finding not just the variable assignments but also the universe and relations that make the formula true. In other words, given a formula $\phi$, we need to find a structure $\mathcal{M}$ such that $\mathcal{M} \models \phi$. ::: tcolorbox Consider the formula $\phi(x, y) = \forall z (A(x, z) \implies \exists t (B(t, y) \land C(x)))$. The satisfiability problem asks if there exists a structure $\mathcal{M} = (U, A^{\mathcal{M}}, B^{\mathcal{M}}, C^{\mathcal{M}})$ and an assignment $s$ such that $\mathcal{M}, s \models \phi$. This requires specifying the universe $U$ and the interpretations of the predicates $A$, $B$, and $C$. ::: ### Undecidability of Satisfiability ::: tcolorbox **(Trakhtenbrot, 1950)** The satisfiability problem for first-order logic is undecidable. This means there is no algorithm that can solve the satisfiability problem for all first-order formulas. ::: ### Proof Idea: Reduction from the Halting Problem To prove undecidability, we can reduce the halting problem to the satisfiability problem. - **Halting Problem**: Given a Turing machine $M$ and an input $w$, does $M$ halt on $w$? (Here we consider the case where $w$ is the empty string) - **Reduction**: Map a Turing machine $M$ to a first-order formula $\phi_M$ such that $M$ halts on an empty tape if and only if $\phi_M$ is satisfiable. If such a reduction exists, and since the halting problem is undecidable, it follows that the satisfiability problem for first-order logic is also undecidable. # The Domino Problem (Tiling Problem) The domino problem, also known as the tiling problem, is a classic decision problem in computer science and mathematics. It asks, given a finite set of tile types, whether it is possible to tile an infinite plane or a rectangle of unknown size using these tiles, subject to certain constraints. ## Problem Definition - **Input**: A finite set $T$ of **tiles**, where each tile is a square with colored edges. Formally, each tile $t \in T$ can be represented as a tuple $t = (c_1, c_2, c_3, c_4)$, where $c_1, c_2, c_3, c_4$ are the colors of the top, right, bottom, and left edges, respectively. - **Rules**: 1. Tiles **cannot be rotated**. They must be placed in the orientation they are given. 2. Adjacent edges of neighboring tiles must have **matching colors**. 3. We have an infinite number of copies of each tile type. 4. The borders of the rectangle must be a specific color (e.g. color 0) - **Question**: Does there exist a rectangle of **any** size (with borders of color 0) that can be completely tiled with the given tiles, adhering to the specified rules? Formally, does there exist a positive integers $m, n$ and a function $f: \{1, \dots, m\} \times \{1, \dots, n\} \to T$ such that the tiling is valid according to the rules? :::: tcolorbox Suppose we are given the following set of tiles, where the colors are represented by numbers: ::: center ::: The question is: can we tile a rectangle of unknown size such that adjacent edges match in color, and the border is color 0? :::: ## Undecidability of the Domino Problem The domino problem is **undecidable**. This means that there is no algorithm that can correctly determine, for any given set of tiles, whether a valid tiling exists. We will sketch a proof of this by reducing the halting problem to the domino problem. ### Reduction from the Halting Problem to the Domino Problem We will outline a two-step reduction strategy: 1. Reduce the **halting problem** to the **domino problem**. 2. Reduce the **domino problem** to the **satisfiability problem for first-order logic**. The first step is the core of the argument, while the second step is a more general connection between computability and logic. - **Reduction Idea**: Map a Turing machine $M$ to a set of tiles $T_M$ such that $M$ halts on an empty tape if and only if there exists a tiling of a rectangle of unknown size (with borders of color 0) with tiles from $T_M$. ### Intuition for the Reduction {#sec:intuition-reduction} The tiles in $T_M$ are constructed such that any valid tiling of a rectangle corresponds to a computation history of the Turing machine $M$. Each row in the tiling represents a configuration of the Turing machine at a specific time step. The colors and symbols on the tiles encode the state of the Turing machine, the contents of its tape, and the position of the tape head. The transition rules of the Turing machine are encoded in the color-matching rules of the tiles. - **Missing Detail**: The specific construction of tiles $T_M$ from the Turing machine $M$ is not detailed in this lecture. This is a crucial part of the reduction and will be elaborated on in the next lecture. - **Suggestion**: The tiles should be designed to meticulously encode the transition rules of the Turing machine. This ensures that adjacent tiles in a valid tiling represent valid transitions of the Turing machine. For example, if the machine in state $q$ reads symbol $a$ and transitions to state $q'$, writing symbol $b$ and moving right, there should be a tile that enforces this transition in the tiling. <figure id="fig:turing-tiling"> <figcaption>Illustration of how a tiling can represent the computation of a Turing machine. Each row represents a configuration of the machine at a given time step. The colored squares represent the state of the machine and the head position. The symbols represent the tape contents. The halting state is <span class="math inline">$q_H$</span>.</figcaption> </figure> # Conclusion In this lecture, we delved into the intricacies of the **model checking** and **satisfiability** problems within the realm of first-order logic. We navigated the challenges posed by **infinite universes** and established that the model checking problem is **PSPACE**-complete. We also examined Trakhtenbrot's seminal result, which states that the satisfiability problem for first-order logic is **undecidable**. To further illuminate the concept of undecidability, we introduced the **domino problem** and outlined a strategy for proving its undecidability by means of a reduction from the **halting problem**. ## Key Takeaways ::: tcolorbox - Model checking for first-order logic is **PSPACE**-complete. - Satisfiability for first-order logic is **undecidable**. - The domino problem is **undecidable** and serves as a powerful tool for proving the undecidability of other problems. ::: ## Follow-up Questions ::: tcolorbox - How can we systematically construct tiles from a given Turing machine to execute the reduction from the halting problem to the domino problem? (This will be a central focus of the next lecture.) - What are the practical implications of the undecidability of the satisfiability problem for first-order logic in real-world applications, such as program verification and automated reasoning? - Can we explore other variants of the domino problem, such as those with different boundary conditions or tiling regions, and analyze their respective computational complexities? ::: For the next lecture, we will delve deeper into the reduction from the halting problem to the domino problem, providing a detailed explanation of the tile construction process, as mentioned in Section [4.2.2](#sec:intuition-reduction){reference-type="ref" reference="sec:intuition-reduction"}. We will also discuss the broader implications of these undecidability results in more detail, connecting them to practical concerns in computer science and logic.