Applications of First-Order Logic and First-Order Theories

Author

Your Name

Published

February 5, 2025

Introduction

This lecture explores the practical applications of first-order logic, focusing on the concept of first-order theories. We will shift our perspective from examining various structures for a fixed formula to analyzing formulas that hold true within a specific, fixed structure. This approach is crucial for understanding the properties of systems and computational devices, as it allows us to fix a system and reason about its properties. We will delve into several examples of first-order theories, including Presburger arithmetic, Peano arithmetic, and Tarski arithmetic, highlighting their applications in constraint solving, distributed systems, computer graphics, robotics, formal languages, and cryptography. Additionally, we will discuss the Rado graph and its implications for probabilistic reasoning in first-order logic, particularly the surprising zero-one law. The main objectives are to understand how first-order theories are defined, how they are used in practice, and the theoretical implications of these concepts, particularly in terms of decidability and complexity. We will see that while some theories are decidable and can be used in practice, others are undecidable, highlighting the trade-off between expressiveness and computational feasibility.

First-Order Theories

A first-order theory is a set of formulas that are true in a given fixed structure. The structure is defined by a signature (a set of symbols), a universe (a set of elements), and an interpretation of the relational symbols.

Formally, let $\Sigma$ be a signature, $U$ be a universe, and $I$ be an interpretation of the relational symbols in $\Sigma$ over $U$. The structure $S$ is defined as $S = (U, I)$. The first-order theory $Th(S)$ is the set of all formulas $\phi$ in the signature $\Sigma$ such that $S \models \phi$. In other words, $Th(S) = \{\phi \in \text{Formulas}(\Sigma) \mid S \models \phi\}$.

The key idea behind first-order theories is to fix a structure, which can represent a mathematical object or a computational device, and then explore the properties that hold true within that structure. This is a shift from the usual approach where we fix a formula and search for structures that satisfy it. By fixing the structure, we can focus on the inherent properties of a specific system or object.

Examples of First-Order Theories

Ordering of Natural Numbers: The structure is $(\mathbb{N}, <)$, where $\mathbb{N}$ is the set of natural numbers and $<$ is the usual ordering. Example formulas:
- $\exists x \forall y (x \leq y)$ (there exists a minimal element, which is 0).
- $\forall x \exists y (y > x)$ (there are infinitely many elements).
- $\forall x \forall y (x < y \lor x = y \lor y < x)$ (the order is total).
This theory is relatively simple, but the model checking problem (determining if a formula belongs to the theory) is still non-trivial.
Presburger Arithmetic: Named after Mojżesz Presburger, this theory has the structure $(\mathbb{N}, +)$, where $+$ is the addition operation (represented as a ternary relation). Example formulas:
- $\exists z \forall x (x + z = x)$ (existence of zero).
- $\forall x \forall y \forall z (x + y = z \leftrightarrow y + x = z)$ (commutativity of addition).
This theory is used in constraint solving, reasoning about arithmetic properties of natural numbers, and formalizing distributed systems.
Peano Arithmetic: Named after Giuseppe Peano, this theory has the structure $(\mathbb{N}, +, \times)$, where $\times$ is the multiplication operation (represented as a ternary relation). Example formulas:
- $\forall x (x \times 1 = x)$ (definition of 1 as the multiplicative identity).
- $\forall x (x \neq 0 \rightarrow \exists y (x = y + 1))$ (every non-zero number has a predecessor).
- Prime Numbers: A number $p$ is prime if it is not 1 and its only divisors are 1 and itself. This can be expressed as: \[\forall p (p \neq 1 \land (\forall a \forall b (p = a \times b \rightarrow (a = 1 \lor b = 1))))\]
- Infinitely Many Primes: \[\forall x \exists p (p > x \land \text{Prime}(p))\]
This theory is significantly more expressive than Presburger arithmetic and can describe many interesting properties, including those of prime numbers. However, this expressiveness comes at a cost: Peano arithmetic is undecidable.
Tarski Arithmetic: Named after Alfred Tarski, this theory has the structure $(\mathbb{R}, +, \times)$, where $\mathbb{R}$ is the set of real numbers. Example formulas:
- $\forall x \exists y (x = y \times y \lor -x = y \times y)$ (every non-negative real number has a square root).
- $\forall x \forall y (x < y \rightarrow \exists z (x < z \land z < y))$ (density of real numbers).
Surprisingly, despite the richer universe, Tarski arithmetic is decidable. It has applications in various areas, including computer graphics, robotics, and cryptography.
Rado Graph: Also known as the random graph, the Rado graph is an infinite graph with specific properties that make it appear random. It is constructed in a way that for any two disjoint finite sets of vertices $U$ and $V$, there exists a vertex $z$ connected to all vertices in $U$ and to no vertex in $V$.
The Rado graph can be constructed as follows:
1. The vertices are the natural numbers $\mathbb{N}$.
2. For any two vertices $m$ and $n$ with $m < n$, there is an edge between $m$ and $n$ if and only if the $m$-th bit of the binary representation of $n$ is 1.
The Rado graph is used to study the probability that a first-order formula is true in a random graph, and it plays a crucial role in the proof of the zero-one law.

Model Checking Problem for First-Order Theories

Given a fixed structure $S$ (as defined in Definition [def:first_order_theory]) and a formula $\phi$, the model checking problem asks whether $S \models \phi$, i.e., whether the formula $\phi$ is true in the structure $S$. This is equivalent to asking whether $\phi$ belongs to the first-order theory $Th(S)$. Since the structure $S$ is often infinite, traditional model checking algorithms that rely on exhaustive enumeration of the universe cannot be used. New algorithms are needed to address this problem, and these algorithms often have high computational complexity.

Example: Ordering of Natural Numbers

For the structure $(\mathbb{N}, <)$, consider the formula $\forall x \exists y (y > x)$. This formula states that there are infinitely many elements in the domain. Determining whether this formula belongs to the theory $Th(\mathbb{N}, <)$ is a non-trivial computational problem. Although the formula is intuitively true, a model checking algorithm would need to reason about the properties of the ordering relation without being able to iterate through all natural numbers.

Example: Presburger Arithmetic

Presburger arithmetic, with the structure $(\mathbb{N}, +)$, is used in constraint solving and reasoning about arithmetic properties of natural numbers. It is also applied in the formalization of distributed systems, where properties of distributed algorithms can be expressed and verified using this theory.

For example, linear inequalities, which are commonly used in constraint satisfaction problems, can be expressed using only addition in Presburger arithmetic. Let’s see how this is done:

$x < y$ can be written as $\exists z (x + z + 1 = y)$, where $z$ is a natural number. We add 1 to $z$ because we want $z$ to be at least 1, ensuring that $y$ is strictly greater than $x$.
$2x < y$ can be written as $\exists z (x + x + z + 1 = y)$.
$5y < 2x - 1$ can be transformed as follows:
1. First, we rewrite the inequality to avoid subtraction: $5y + 1 < 2x$.
2. Then, we express the multiplication by constants as repeated addition: $y + y + y + y + y + 1 < x + x$.
3. Finally, we use the technique from the first example to express the inequality using only addition: $\exists z (y + y + y + y + y + 1 + z + 1 = x + x)$.

In general, any linear inequality with integer coefficients can be expressed in Presburger arithmetic using the following steps:

Rewrite the inequality to have only positive coefficients by moving terms with negative coefficients to the other side of the inequality.
Express multiplication by constants as repeated addition.
Introduce an existentially quantified variable and add 1 to it to represent the strict inequality using only addition.

Graphical representation of the inequality (5y < 2x - 1) in the natural numbers. The shaded region represents the solutions to the inequality.

Furthermore, we can use existential quantification to project the solution space onto a single axis. For instance, $\exists y (5y + 2 = 2x)$ defines a set of points on the x-axis that satisfy the inequality for some natural number $y$. The resulting set will have a finite number of exceptions and then follow a periodic pattern.

These transformations allow us to use decision procedures for Presburger arithmetic to solve problems involving linear inequalities, which have applications in areas such as program analysis, compiler optimization, and operations research.

Peano Arithmetic and Undecidability

Peano arithmetic, with the structure $(\mathbb{N}, +, \times)$, is powerful enough to express properties of prime numbers and many other complex mathematical concepts. For instance, we can define the number 1 as the unique element such that $\forall x (x \times 1 = x)$, and we can define prime numbers as numbers greater than 1 that are only divisible by 1 and themselves: \[\text{Prime}(p) \equiv p > 1 \land \forall a \forall b (p = a \times b \rightarrow (a = 1 \lor b = 1))\] We can even express the statement that there are infinitely many prime numbers: \[\forall x \exists p (p > x \land \text{Prime}(p))\] However, this expressiveness comes at a significant cost: undecidability.

The first-order theory of Peano arithmetic is undecidable. That is, there is no algorithm that can take as input an arbitrary first-order formula $\phi$ in the signature of Peano arithmetic and determine, in finite time, whether $\phi$ is true in the standard model of natural numbers $(\mathbb{N}, +, \times)$.

The undecidability of Peano arithmetic has profound implications. It means that there are statements within the theory that are true but cannot be proven within the system, and there are statements that are false but cannot be disproven. This is a fundamental limitation of formal systems that are expressive enough to include basic arithmetic.

This undecidability result is closely related to the undecidability of the Diophantine equations problem, also known as Hilbert’s 10th problem.

A Diophantine equation is a polynomial equation with integer coefficients for which we seek integer solutions. A system of Diophantine equations is a set of such equations, and we seek integer values for the variables that satisfy all equations in the system simultaneously.

There is no algorithm that can take as input an arbitrary system of Diophantine equations and determine, in finite time, whether the system has a solution in the integers.

The connection between Peano arithmetic and Hilbert’s 10th problem is established through a reduction. We can encode any system of Diophantine equations as a first-order formula in Peano arithmetic such that the formula is true if and only if the system of equations has a solution in the natural numbers.

For example, consider the Diophantine equation $x^2 - y^2 = 0$. We can express this in Peano arithmetic as: \[\exists x \exists y (x \times x = y \times y)\] This formula is true in $(\mathbb{N}, +, \times)$ if and only if there exist natural numbers $x$ and $y$ that satisfy the equation $x^2 = y^2$.

Since we can reduce the problem of solving Diophantine equations to the problem of determining the truth of a formula in Peano arithmetic, and since Hilbert’s 10th problem is undecidable, it follows that Peano arithmetic is also undecidable.

The undecidability of Peano arithmetic is a fundamental result in mathematical logic and computer science. It demonstrates that there are inherent limitations to what can be computed and proven within formal systems that are powerful enough to encompass basic arithmetic.

Tarski Arithmetic and Decidability

Tarski arithmetic, named after Alfred Tarski, is the first-order theory of the structure $(\mathbb{R}, +, \times)$, where $\mathbb{R}$ represents the set of real numbers, and $+$ and $\times$ are the usual addition and multiplication operations. This theory allows us to express statements about real numbers, including polynomial equations and inequalities.

Surprisingly, despite the richer universe of real numbers compared to the natural numbers in Peano arithmetic, Tarski arithmetic is decidable. This is a highly non-trivial result.

The first-order theory of Tarski arithmetic is decidable. That is, there exists an algorithm that can take as input an arbitrary first-order formula $\phi$ in the signature of Tarski arithmetic and determine, in finite time, whether $\phi$ is true in the structure $(\mathbb{R}, +, \times)$.

The decidability of Tarski arithmetic is a remarkable result because it shows that despite the complexity and infinite nature of the real numbers, there is a systematic way to determine the truth of any statement expressible in this theory. This is in stark contrast to Peano arithmetic, which is undecidable.

The original decision procedure provided by Tarski was based on quantifier elimination, a technique that transforms a formula with quantifiers into an equivalent formula without quantifiers. However, this algorithm had a non-elementary complexity, making it impractical for real-world applications. Later, more efficient algorithms were developed, such as the cylindrical algebraic decomposition (CAD) algorithm, which has a doubly exponential time complexity. While still complex, these algorithms are practical for many problems.

This theory has numerous applications in various areas, including:

Computer Graphics: Tarski arithmetic can be used to model and solve problems related to geometric shapes, intersections, and transformations, which are fundamental in computer graphics. For example, determining whether two curves intersect can be expressed as a formula in Tarski arithmetic.

Intersection of two parabolas, which can be determined using Tarski arithmetic.
Robotics: Kinematics and motion planning for robots often involve solving systems of polynomial equations, which can be tackled using Tarski arithmetic. For instance, determining the possible configurations of a robot arm can be formulated as a decision problem in this theory.
Cryptography: Some modern cryptographic primitives rely on the properties of real numbers and polynomial equations, making Tarski arithmetic relevant for their analysis and security proofs.
Formal Verification: Tarski arithmetic can be used to verify properties of hybrid systems, which combine continuous dynamics (modeled using real numbers) with discrete control.
Theorem Proving: Automated theorem provers can use decision procedures for Tarski arithmetic to prove or disprove conjectures involving real numbers.

The decidability of Tarski arithmetic, combined with its wide range of applications, makes it a powerful tool for solving problems in various domains involving real numbers and polynomial relationships.

Rado Graph and the Zero-One Law

The Rado graph, also known as the random graph or the infinite random graph, is a specific infinite graph that embodies many properties of finite random graphs. It is constructed in a deterministic way (as described in Section 2.1), but it exhibits characteristics that make it appear random. The Rado graph is used to study the probabilistic behavior of first-order formulas in the context of finite random graphs.

Let’s first define what we mean by a random graph.

A random graph $G(n, p)$ is a graph with $n$ vertices where each edge is included independently with probability $p$. In this context, we consider the case where $p = 1/2$, meaning each edge is present with probability $1/2$.

Let $\phi$ be any first-order formula in the language of graphs (i.e., using only the edge relation $E(x, y)$). Let $G(n, 1/2)$ denote a random graph on $n$ vertices with edge probability $1/2$. Then, \[\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi] \in \{0, 1\}\] That is, as the number of vertices $n$ goes to infinity, the probability that a random graph with $n$ vertices satisfies $\phi$ approaches either 0 or 1.

The Zero-One Law is a surprising result. It states that for any property expressible in first-order logic, a large random graph either almost surely has that property or almost surely does not have that property. There are no intermediate probabilities.

Here are some examples to illustrate the Zero-One Law:

Example 1: Consider the formula $\phi_1$ stating the existence of a triangle: \[\phi_1 \equiv \exists x \exists y \exists z (E(x, y) \land E(y, z) \land E(x, z))\] As $n$ increases, the probability that a random graph $G(n, 1/2)$ contains a triangle approaches 1. Thus, $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi_1] = 1$.
Example 2: Consider the formula $\phi_2$ stating that every vertex is connected to at least one other vertex: \[\phi_2 \equiv \forall x \exists y (x \neq y \land E(x, y))\] As $n$ increases, the probability that every vertex has a neighbor approaches 1. Thus, $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi_2] = 1$.
Example 3: Consider the formula $\phi_3$ stating that there is no isolated vertex: \[\phi_3 \equiv \forall x \exists y E(x,y)\] As $n$ goes to infinity, the probability that there is no isolated vertex tends to 1. Thus, $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi_3] = 1$.
Example 4: Consider the formula $\phi_4$ stating that there is no clique of size 5. As $n$ goes to infinity, the probability that there is no clique of size 5 tends to 0. Thus, $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi_4] = 0$.

The Rado graph $R$ plays a crucial role in understanding the Zero-One Law. It turns out that the behavior of a first-order formula on large random graphs is directly connected to its truth value on the Rado graph.

Let $\phi$ be a first-order formula in the language of graphs. Then the following are equivalent:

$R \models \phi$ (The Rado graph satisfies $\phi$)
$\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi] = 1$

This theorem provides a bridge between the infinite Rado graph and the probabilistic behavior of finite random graphs. Moreover, it leads to a surprising decidability result.

The first-order theory of the Rado graph, $Th(R)$, is decidable. In fact, there is an algorithm that can decide whether $R \models \phi$ for any first-order formula $\phi$ in PSPACE.

The decidability of $Th(R)$, combined with the connection between the Rado graph and the Zero-One Law, implies that we can effectively determine whether a first-order property holds almost surely in large random graphs. This has applications in areas such as network analysis, where random graphs are used to model complex networks.

The Zero-One Law and the properties of the Rado graph provide deep insights into the behavior of first-order logic on random structures. They demonstrate a fascinating interplay between the infinite and the finite, and between deterministic constructions and probabilistic outcomes.

Conclusion

This lecture introduced the concept of first-order theories, which provide a powerful framework for reasoning about systems and their properties by fixing a structure and examining the formulas true within that structure. We explored several important examples of first-order theories, including Presburger arithmetic, Peano arithmetic, Tarski arithmetic, and the theory of the Rado graph.

These theories have a wide range of practical applications:

Presburger arithmetic finds applications in constraint solving, reasoning about arithmetic properties of natural numbers, and formal verification of distributed systems.
Peano arithmetic, while undecidable, is crucial for understanding the foundations of mathematics and the limits of formal systems.
Tarski arithmetic is used in computer graphics, robotics, cryptography, formal verification of hybrid systems, and automated theorem proving.
The Rado graph and the Zero-One Law provide insights into the behavior of large random graphs and have applications in network analysis.

We also discussed the theoretical implications of these theories, particularly in terms of decidability and complexity. Key takeaways include:

Fixing a structure and examining the formulas true in that structure offers a valuable perspective for analyzing systems and their properties.
The undecidability of Peano arithmetic (Theorem [thm:undecidability_peano]) highlights the trade-off between expressiveness and decidability. It demonstrates the inherent limitations of formal systems that are powerful enough to encompass basic arithmetic.
The decidability of Tarski arithmetic (Theorem [thm:decidability_tarski]), despite the infinite nature of the real numbers, showcases that even rich theories can be computationally manageable, enabling practical applications in various domains.
The Zero-One Law for random graphs (Theorem [thm:zero_one_law]) reveals surprising insights into the probabilistic behavior of first-order formulas, showing that properties expressed in first-order logic either hold almost surely or almost surely do not hold in large random graphs.

Follow-up Questions:

How can we formally compare the expressiveness of different first-order theories? For instance, how can we show that Peano arithmetic is more expressive than Presburger arithmetic?
What are the specific techniques used in the algorithms for deciding Tarski arithmetic, such as quantifier elimination and cylindrical algebraic decomposition? How do these algorithms work in practice?
How is the Rado graph constructed in detail, and what are its key properties that make it suitable for studying the probabilistic behavior of first-order formulas?
Can we extend the Zero-One Law to other types of structures or logics, such as monadic second-order logic or random graphs with different edge probabilities? What are the limitations of such extensions?
What are other examples of decidable and undecidable theories, and what are their practical implications?

For the next lecture, we will explore methods for comparing the expressiveness of different first-order theories, such as the concept of interpretability. We will also delve deeper into the algorithmic aspects of deciding these theories, focusing on techniques like quantifier elimination and their complexity. Furthermore, we will discuss other examples of decidable and undecidable theories and their impact on various fields of computer science and mathematics.

--- title: "Applications of First-Order Logic and First-Order Theories" 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 explores the practical applications of first-order logic, focusing on the concept of first-order theories. We will shift our perspective from examining various structures for a fixed formula to analyzing formulas that hold true within a specific, fixed structure. This approach is crucial for understanding the properties of systems and computational devices, as it allows us to fix a system and reason about its properties. We will delve into several examples of first-order theories, including Presburger arithmetic, Peano arithmetic, and Tarski arithmetic, highlighting their applications in constraint solving, distributed systems, computer graphics, robotics, formal languages, and cryptography. Additionally, we will discuss the Rado graph and its implications for probabilistic reasoning in first-order logic, particularly the surprising zero-one law. The main objectives are to understand how first-order theories are defined, how they are used in practice, and the theoretical implications of these concepts, particularly in terms of decidability and complexity. We will see that while some theories are decidable and can be used in practice, others are undecidable, highlighting the trade-off between expressiveness and computational feasibility. # First-Order Theories ::: tcolorbox []{#def:first_order_theory label="def:first_order_theory"} A first-order theory is a set of formulas that are true in a given fixed structure. The structure is defined by a signature (a set of symbols), a universe (a set of elements), and an interpretation of the relational symbols. ::: Formally, let $\Sigma$ be a signature, $U$ be a universe, and $I$ be an interpretation of the relational symbols in $\Sigma$ over $U$. The structure $S$ is defined as $S = (U, I)$. The first-order theory $Th(S)$ is the set of all formulas $\phi$ in the signature $\Sigma$ such that $S \models \phi$. In other words, $Th(S) = \{\phi \in \text{Formulas}(\Sigma) \mid S \models \phi\}$. ::: tcolorbox The key idea behind first-order theories is to fix a structure, which can represent a mathematical object or a computational device, and then explore the properties that hold true within that structure. This is a shift from the usual approach where we fix a formula and search for structures that satisfy it. By fixing the structure, we can focus on the inherent properties of a specific system or object. ::: ## Examples of First-Order Theories - **Ordering of Natural Numbers**: The structure is $(\mathbb{N}, <)$, where $\mathbb{N}$ is the set of natural numbers and $<$ is the usual ordering. Example formulas: - $\exists x \forall y (x \leq y)$ (there exists a minimal element, which is 0). - $\forall x \exists y (y > x)$ (there are infinitely many elements). - $\forall x \forall y (x < y \lor x = y \lor y < x)$ (the order is total). This theory is relatively simple, but the model checking problem (determining if a formula belongs to the theory) is still non-trivial. - **Presburger Arithmetic**: Named after Mojżesz Presburger, this theory has the structure $(\mathbb{N}, +)$, where $+$ is the addition operation (represented as a ternary relation). Example formulas: - $\exists z \forall x (x + z = x)$ (existence of zero). - $\forall x \forall y \forall z (x + y = z \leftrightarrow y + x = z)$ (commutativity of addition). This theory is used in constraint solving, reasoning about arithmetic properties of natural numbers, and formalizing distributed systems. - **Peano Arithmetic**: Named after Giuseppe Peano, this theory has the structure $(\mathbb{N}, +, \times)$, where $\times$ is the multiplication operation (represented as a ternary relation). Example formulas: - $\forall x (x \times 1 = x)$ (definition of 1 as the multiplicative identity). - $\forall x (x \neq 0 \rightarrow \exists y (x = y + 1))$ (every non-zero number has a predecessor). - **Prime Numbers**: A number $p$ is prime if it is not 1 and its only divisors are 1 and itself. This can be expressed as: $$\forall p (p \neq 1 \land (\forall a \forall b (p = a \times b \rightarrow (a = 1 \lor b = 1))))$$ - **Infinitely Many Primes**: $$\forall x \exists p (p > x \land \text{Prime}(p))$$ This theory is significantly more expressive than Presburger arithmetic and can describe many interesting properties, including those of prime numbers. However, this expressiveness comes at a cost: Peano arithmetic is undecidable. - **Tarski Arithmetic**: Named after Alfred Tarski, this theory has the structure $(\mathbb{R}, +, \times)$, where $\mathbb{R}$ is the set of real numbers. Example formulas: - $\forall x \exists y (x = y \times y \lor -x = y \times y)$ (every non-negative real number has a square root). - $\forall x \forall y (x < y \rightarrow \exists z (x < z \land z < y))$ (density of real numbers). Surprisingly, despite the richer universe, Tarski arithmetic is decidable. It has applications in various areas, including computer graphics, robotics, and cryptography. - **Rado Graph**: Also known as the random graph, the Rado graph is an infinite graph with specific properties that make it appear random. It is constructed in a way that for any two disjoint finite sets of vertices $U$ and $V$, there exists a vertex $z$ connected to all vertices in $U$ and to no vertex in $V$. ::: tcolorbox The Rado graph can be constructed as follows: 1. The vertices are the natural numbers $\mathbb{N}$. 2. For any two vertices $m$ and $n$ with $m < n$, there is an edge between $m$ and $n$ if and only if the $m$-th bit of the binary representation of $n$ is 1. ::: The Rado graph is used to study the probability that a first-order formula is true in a random graph, and it plays a crucial role in the proof of the zero-one law. # Model Checking Problem for First-Order Theories Given a fixed structure $S$ (as defined in Definition [\[def:first_order_theory\]](#def:first_order_theory){reference-type="ref" reference="def:first_order_theory"}) and a formula $\phi$, the model checking problem asks whether $S \models \phi$, i.e., whether the formula $\phi$ is true in the structure $S$. This is equivalent to asking whether $\phi$ belongs to the first-order theory $Th(S)$. Since the structure $S$ is often infinite, traditional model checking algorithms that rely on exhaustive enumeration of the universe cannot be used. New algorithms are needed to address this problem, and these algorithms often have high computational complexity. ## Example: Ordering of Natural Numbers For the structure $(\mathbb{N}, <)$, consider the formula $\forall x \exists y (y > x)$. This formula states that there are infinitely many elements in the domain. Determining whether this formula belongs to the theory $Th(\mathbb{N}, <)$ is a non-trivial computational problem. Although the formula is intuitively true, a model checking algorithm would need to reason about the properties of the ordering relation without being able to iterate through all natural numbers. ## Example: Presburger Arithmetic Presburger arithmetic, with the structure $(\mathbb{N}, +)$, is used in constraint solving and reasoning about arithmetic properties of natural numbers. It is also applied in the formalization of distributed systems, where properties of distributed algorithms can be expressed and verified using this theory. For example, linear inequalities, which are commonly used in constraint satisfaction problems, can be expressed using only addition in Presburger arithmetic. Let's see how this is done: - $x < y$ can be written as $\exists z (x + z + 1 = y)$, where $z$ is a natural number. We add 1 to $z$ because we want $z$ to be at least 1, ensuring that $y$ is strictly greater than $x$. - $2x < y$ can be written as $\exists z (x + x + z + 1 = y)$. - $5y < 2x - 1$ can be transformed as follows: 1. First, we rewrite the inequality to avoid subtraction: $5y + 1 < 2x$. 2. Then, we express the multiplication by constants as repeated addition: $y + y + y + y + y + 1 < x + x$. 3. Finally, we use the technique from the first example to express the inequality using only addition: $\exists z (y + y + y + y + y + 1 + z + 1 = x + x)$. ::: tcolorbox In general, any linear inequality with integer coefficients can be expressed in Presburger arithmetic using the following steps: 1. Rewrite the inequality to have only positive coefficients by moving terms with negative coefficients to the other side of the inequality. 2. Express multiplication by constants as repeated addition. 3. Introduce an existentially quantified variable and add 1 to it to represent the strict inequality using only addition. ::: <figure id="fig:linear_inequality"> <figcaption>Graphical representation of the inequality <span class="math inline">$5y < 2x - 1$</span> in the natural numbers. The shaded region represents the solutions to the inequality.</figcaption> </figure> Furthermore, we can use existential quantification to project the solution space onto a single axis. For instance, $\exists y (5y + 2 = 2x)$ defines a set of points on the x-axis that satisfy the inequality for some natural number $y$. The resulting set will have a finite number of exceptions and then follow a periodic pattern. These transformations allow us to use decision procedures for Presburger arithmetic to solve problems involving linear inequalities, which have applications in areas such as program analysis, compiler optimization, and operations research. # Peano Arithmetic and Undecidability Peano arithmetic, with the structure $(\mathbb{N}, +, \times)$, is powerful enough to express properties of prime numbers and many other complex mathematical concepts. For instance, we can define the number 1 as the unique element such that $\forall x (x \times 1 = x)$, and we can define prime numbers as numbers greater than 1 that are only divisible by 1 and themselves: $$\text{Prime}(p) \equiv p > 1 \land \forall a \forall b (p = a \times b \rightarrow (a = 1 \lor b = 1))$$ We can even express the statement that there are infinitely many prime numbers: $$\forall x \exists p (p > x \land \text{Prime}(p))$$ However, this expressiveness comes at a significant cost: undecidability. ::: tcolorbox []{#thm:undecidability_peano label="thm:undecidability_peano"} The first-order theory of Peano arithmetic is undecidable. That is, there is no algorithm that can take as input an arbitrary first-order formula $\phi$ in the signature of Peano arithmetic and determine, in finite time, whether $\phi$ is true in the standard model of natural numbers $(\mathbb{N}, +, \times)$. ::: ::: tcolorbox The undecidability of Peano arithmetic has profound implications. It means that there are statements within the theory that are true but cannot be proven within the system, and there are statements that are false but cannot be disproven. This is a fundamental limitation of formal systems that are expressive enough to include basic arithmetic. ::: This undecidability result is closely related to the undecidability of the Diophantine equations problem, also known as Hilbert's 10th problem. ::: tcolorbox A Diophantine equation is a polynomial equation with integer coefficients for which we seek integer solutions. A system of Diophantine equations is a set of such equations, and we seek integer values for the variables that satisfy all equations in the system simultaneously. ::: ::: tcolorbox There is no algorithm that can take as input an arbitrary system of Diophantine equations and determine, in finite time, whether the system has a solution in the integers. ::: The connection between Peano arithmetic and Hilbert's 10th problem is established through a reduction. We can encode any system of Diophantine equations as a first-order formula in Peano arithmetic such that the formula is true if and only if the system of equations has a solution in the natural numbers. For example, consider the Diophantine equation $x^2 - y^2 = 0$. We can express this in Peano arithmetic as: $$\exists x \exists y (x \times x = y \times y)$$ This formula is true in $(\mathbb{N}, +, \times)$ if and only if there exist natural numbers $x$ and $y$ that satisfy the equation $x^2 = y^2$. Since we can reduce the problem of solving Diophantine equations to the problem of determining the truth of a formula in Peano arithmetic, and since Hilbert's 10th problem is undecidable, it follows that Peano arithmetic is also undecidable. The undecidability of Peano arithmetic is a fundamental result in mathematical logic and computer science. It demonstrates that there are inherent limitations to what can be computed and proven within formal systems that are powerful enough to encompass basic arithmetic. # Tarski Arithmetic and Decidability Tarski arithmetic, named after Alfred Tarski, is the first-order theory of the structure $(\mathbb{R}, +, \times)$, where $\mathbb{R}$ represents the set of real numbers, and $+$ and $\times$ are the usual addition and multiplication operations. This theory allows us to express statements about real numbers, including polynomial equations and inequalities. Surprisingly, despite the richer universe of real numbers compared to the natural numbers in Peano arithmetic, Tarski arithmetic is decidable. This is a highly non-trivial result. ::: tcolorbox []{#thm:decidability_tarski label="thm:decidability_tarski"} The first-order theory of Tarski arithmetic is decidable. That is, there exists an algorithm that can take as input an arbitrary first-order formula $\phi$ in the signature of Tarski arithmetic and determine, in finite time, whether $\phi$ is true in the structure $(\mathbb{R}, +, \times)$. ::: ::: tcolorbox The decidability of Tarski arithmetic is a remarkable result because it shows that despite the complexity and infinite nature of the real numbers, there is a systematic way to determine the truth of any statement expressible in this theory. This is in stark contrast to Peano arithmetic, which is undecidable. ::: The original decision procedure provided by Tarski was based on quantifier elimination, a technique that transforms a formula with quantifiers into an equivalent formula without quantifiers. However, this algorithm had a non-elementary complexity, making it impractical for real-world applications. Later, more efficient algorithms were developed, such as the cylindrical algebraic decomposition (CAD) algorithm, which has a doubly exponential time complexity. While still complex, these algorithms are practical for many problems. This theory has numerous applications in various areas, including: - **Computer Graphics**: Tarski arithmetic can be used to model and solve problems related to geometric shapes, intersections, and transformations, which are fundamental in computer graphics. For example, determining whether two curves intersect can be expressed as a formula in Tarski arithmetic. <figure id="fig:parabola_intersection"> <figcaption>Intersection of two parabolas, which can be determined using Tarski arithmetic.</figcaption> </figure> - **Robotics**: Kinematics and motion planning for robots often involve solving systems of polynomial equations, which can be tackled using Tarski arithmetic. For instance, determining the possible configurations of a robot arm can be formulated as a decision problem in this theory. - **Cryptography**: Some modern cryptographic primitives rely on the properties of real numbers and polynomial equations, making Tarski arithmetic relevant for their analysis and security proofs. - **Formal Verification**: Tarski arithmetic can be used to verify properties of hybrid systems, which combine continuous dynamics (modeled using real numbers) with discrete control. - **Theorem Proving**: Automated theorem provers can use decision procedures for Tarski arithmetic to prove or disprove conjectures involving real numbers. The decidability of Tarski arithmetic, combined with its wide range of applications, makes it a powerful tool for solving problems in various domains involving real numbers and polynomial relationships. # Rado Graph and the Zero-One Law The Rado graph, also known as the random graph or the infinite random graph, is a specific infinite graph that embodies many properties of finite random graphs. It is constructed in a deterministic way (as described in Section 2.1), but it exhibits characteristics that make it appear random. The Rado graph is used to study the probabilistic behavior of first-order formulas in the context of finite random graphs. Let's first define what we mean by a random graph. ::: tcolorbox A random graph $G(n, p)$ is a graph with $n$ vertices where each edge is included independently with probability $p$. In this context, we consider the case where $p = 1/2$, meaning each edge is present with probability $1/2$. ::: ::: tcolorbox []{#thm:zero_one_law label="thm:zero_one_law"} Let $\phi$ be any first-order formula in the language of graphs (i.e., using only the edge relation $E(x, y)$). Let $G(n, 1/2)$ denote a random graph on $n$ vertices with edge probability $1/2$. Then, $$\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi] \in \{0, 1\}$$ That is, as the number of vertices $n$ goes to infinity, the probability that a random graph with $n$ vertices satisfies $\phi$ approaches either 0 or 1. ::: ::: tcolorbox The Zero-One Law is a surprising result. It states that for any property expressible in first-order logic, a large random graph either almost surely has that property or almost surely does not have that property. There are no intermediate probabilities. ::: Here are some examples to illustrate the Zero-One Law: - **Example 1**: Consider the formula $\phi_1$ stating the existence of a triangle: $$\phi_1 \equiv \exists x \exists y \exists z (E(x, y) \land E(y, z) \land E(x, z))$$ As $n$ increases, the probability that a random graph $G(n, 1/2)$ contains a triangle approaches 1. Thus, $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi_1] = 1$. - **Example 2**: Consider the formula $\phi_2$ stating that every vertex is connected to at least one other vertex: $$\phi_2 \equiv \forall x \exists y (x \neq y \land E(x, y))$$ As $n$ increases, the probability that every vertex has a neighbor approaches 1. Thus, $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi_2] = 1$. - **Example 3**: Consider the formula $\phi_3$ stating that there is no isolated vertex: $$\phi_3 \equiv \forall x \exists y E(x,y)$$ As $n$ goes to infinity, the probability that there is no isolated vertex tends to 1. Thus, $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi_3] = 1$. - **Example 4**: Consider the formula $\phi_4$ stating that there is no clique of size 5. As $n$ goes to infinity, the probability that there is no clique of size 5 tends to 0. Thus, $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi_4] = 0$. The Rado graph $R$ plays a crucial role in understanding the Zero-One Law. It turns out that the behavior of a first-order formula on large random graphs is directly connected to its truth value on the Rado graph. ::: tcolorbox Let $\phi$ be a first-order formula in the language of graphs. Then the following are equivalent: 1. $R \models \phi$ (The Rado graph satisfies $\phi$) 2. $\lim_{n \to \infty} \text{Prob}[G(n, 1/2) \models \phi] = 1$ ::: This theorem provides a bridge between the infinite Rado graph and the probabilistic behavior of finite random graphs. Moreover, it leads to a surprising decidability result. ::: tcolorbox The first-order theory of the Rado graph, $Th(R)$, is decidable. In fact, there is an algorithm that can decide whether $R \models \phi$ for any first-order formula $\phi$ in PSPACE. ::: ::: tcolorbox The decidability of $Th(R)$, combined with the connection between the Rado graph and the Zero-One Law, implies that we can effectively determine whether a first-order property holds almost surely in large random graphs. This has applications in areas such as network analysis, where random graphs are used to model complex networks. ::: The Zero-One Law and the properties of the Rado graph provide deep insights into the behavior of first-order logic on random structures. They demonstrate a fascinating interplay between the infinite and the finite, and between deterministic constructions and probabilistic outcomes. # Conclusion This lecture introduced the concept of first-order theories, which provide a powerful framework for reasoning about systems and their properties by fixing a structure and examining the formulas true within that structure. We explored several important examples of first-order theories, including Presburger arithmetic, Peano arithmetic, Tarski arithmetic, and the theory of the Rado graph. These theories have a wide range of practical applications: - **Presburger arithmetic** finds applications in constraint solving, reasoning about arithmetic properties of natural numbers, and formal verification of distributed systems. - **Peano arithmetic**, while undecidable, is crucial for understanding the foundations of mathematics and the limits of formal systems. - **Tarski arithmetic** is used in computer graphics, robotics, cryptography, formal verification of hybrid systems, and automated theorem proving. - **The Rado graph** and the Zero-One Law provide insights into the behavior of large random graphs and have applications in network analysis. We also discussed the theoretical implications of these theories, particularly in terms of decidability and complexity. Key takeaways include: - Fixing a structure and examining the formulas true in that structure offers a valuable perspective for analyzing systems and their properties. - The undecidability of Peano arithmetic (Theorem [\[thm:undecidability_peano\]](#thm:undecidability_peano){reference-type="ref" reference="thm:undecidability_peano"}) highlights the trade-off between expressiveness and decidability. It demonstrates the inherent limitations of formal systems that are powerful enough to encompass basic arithmetic. - The decidability of Tarski arithmetic (Theorem [\[thm:decidability_tarski\]](#thm:decidability_tarski){reference-type="ref" reference="thm:decidability_tarski"}), despite the infinite nature of the real numbers, showcases that even rich theories can be computationally manageable, enabling practical applications in various domains. - The Zero-One Law for random graphs (Theorem [\[thm:zero_one_law\]](#thm:zero_one_law){reference-type="ref" reference="thm:zero_one_law"}) reveals surprising insights into the probabilistic behavior of first-order formulas, showing that properties expressed in first-order logic either hold almost surely or almost surely do not hold in large random graphs. **Follow-up Questions**: - How can we formally compare the expressiveness of different first-order theories? For instance, how can we show that Peano arithmetic is more expressive than Presburger arithmetic? - What are the specific techniques used in the algorithms for deciding Tarski arithmetic, such as quantifier elimination and cylindrical algebraic decomposition? How do these algorithms work in practice? - How is the Rado graph constructed in detail, and what are its key properties that make it suitable for studying the probabilistic behavior of first-order formulas? - Can we extend the Zero-One Law to other types of structures or logics, such as monadic second-order logic or random graphs with different edge probabilities? What are the limitations of such extensions? - What are other examples of decidable and undecidable theories, and what are their practical implications? For the next lecture, we will explore methods for comparing the expressiveness of different first-order theories, such as the concept of interpretability. We will also delve deeper into the algorithmic aspects of deciding these theories, focusing on techniques like quantifier elimination and their complexity. Furthermore, we will discuss other examples of decidable and undecidable theories and their impact on various fields of computer science and mathematics.