Logical Theories and Reductions

Author

Your Name

Published

February 5, 2025

Introduction

This lecture delves into the realm of logical theories, with a particular focus on first-order theories. We introduce the concept of logical reductions as a powerful tool for comparing the expressive power of these theories.

Recall that a theory is defined as a set of formulas that are true within a fixed structure. This perspective gives rise to a decision problem: given a formula and a predefined structure, we seek to determine the truth value of the formula within that structure. Unlike traditional model checking, where the structure is part of the input, fixing the structure beforehand allows us to reason about infinite structures, significantly enriching the problem’s complexity and interest.

The primary goal is to establish a framework, analogous to algorithmic reductions in computability theory, that enables us to determine the relative complexity of different logical theories. By doing so, we can gain a deeper understanding of their expressive capabilities and limitations.

Algorithmic Reductions

In the realm of computability theory, many-to-one reductions serve as a cornerstone for comparing the difficulty of computational problems. Suppose we have two problems, $P$ and $Q$, where $P$ is intuitively considered "easier" and $Q$ is considered "harder". A reduction from $P$ to $Q$ is established through a computable function $F$. This function takes any input $X$ for problem $P$ and transforms it into a corresponding input $X'$ for problem $Q$.

The crucial property of this transformation is that it preserves the truth value of the problem instances. Formally, the answer to problem $P$ for input $X$ is true if and only if the answer to problem $Q$ for input $X'$ is true. This can be expressed as: \[P(X) \iff Q(F(X))\] where $P(X)$ denotes the answer to problem $P$ with input $X$, and $Q(F(X))$ denotes the answer to problem $Q$ with input $F(X)$.

Example: Consider problem $P$ as determining if a number is even, and problem $Q$ as determining if a number is divisible by 4. We can reduce $P$ to $Q$ by defining $F(X) = 2X$. If $X$ is even (i.e., $P(X)$ is true), then $2X$ is divisible by 4 (i.e., $Q(F(X))$ is true). Conversely, if $2X$ is divisible by 4, then $X$ must be even.

This implies that if we have an algorithm to solve $Q$, we can use it to solve $P$ by first applying the reduction function $F$. Consequently, if $P$ is undecidable, then $Q$ must also be undecidable.

Logical Reductions

The concept of reduction, powerful in comparing computational problems, can be elegantly extended to the realm of logical theories. Let $S$ and $T$ be two structures, and our goal is to demonstrate that the logical theory of $S$ is "easier" than that of $T$.

To achieve this, we need a computable function that maps a formula $\phi$, expressed in the signature of $S$, into a corresponding formula $\phi'$, expressed in the signature of $T$. This mapping must satisfy a crucial property: $\phi$ holds true over structure $S$ if and only if $\phi'$ holds true over structure $T$. Formally: \[S \models \phi \iff T \models \phi'\]

This establishes a logical reduction from the theory of $S$ to the theory of $T$. In essence, it means that if we can decide the truth of formulas in the theory of $T$, we can also decide the truth of formulas in the theory of $S$ by using the aforementioned computable function to translate between the two.

This theorem describes the implication of a logical reduction between two theories in terms of decidability.

Theorem 1. If there exists a logical reduction from the theory of structure $S$ to the theory of structure $T$, and the theory of $T$ is decidable, then the theory of $S$ is also decidable. Conversely, if the theory of $S$ is undecidable, then the theory of $T$ must also be undecidable.

Logical Interpretations

A logical interpretation is a specific and powerful type of logical reduction. It provides a systematic way to construct the transformation function $F$, not arbitrarily, but by directly leveraging a well-defined relationship between the structures $S$ and $T$. The core idea is to describe the "easier" structure $S$ as a logical transformation of the "harder" structure $T$.

This definition formally introduces the concept of a logical interpretation between two structures.

Definition 1. A logical interpretation of structure $S$ in structure $T$, denoted as $S \leq_L T$, is defined by a set of formulas in the signature of $T$ that effectively "encode" the relations of $S$ within $T$. Specifically, for each relation $R$ in $S$ (including the universe, which can be seen as a unary relation), we associate a formula $\alpha_R$ in the signature of $T$. This formula $\alpha_R$ has the same number of free variables as the arity of $R$.

The interpretation must ensure that the set of tuples from the universe of $T$ that satisfy $\alpha_R$ is isomorphic* to the relation $R$ in $S$. In other words, there exists a bijection between the elements of the universe of $S$ and a subset of the universe of $T$ (defined by $\alpha_U$ where $U$ is the universe of $S$) that preserves the structure defined by the relations in $S$.*

This remark highlights the core concept behind logical interpretations. Remark: We are essentially "simulating" the structure $S$ within the structure $T$ using the logical language of $T$. Each relation in $S$ is "translated" into a logical definition within $T$.

The significance of this definition lies in its constructive nature. Once we have a logical interpretation, we can automatically derive the reduction function $F$ that maps formulas from $S$ to $T$, as we will see in subsequent examples.

Example: Reduction from Natural Numbers with Order to Presburger Arithmetic

We will now illustrate the concept of logical interpretation with a concrete example. We aim to show that the first-order theory of natural numbers with order, denoted as $FO(\mathbb{N}, <)$, is reducible to Presburger arithmetic, which is the first-order theory of natural numbers with addition, denoted as $FO(\mathbb{N}, +)$.

Structure $S$: Natural numbers with the total order relation ($<$), represented as $(\mathbb{N}, <)$.
Structure $T$: Natural numbers with addition ($+$), represented as $(\mathbb{N}, +)$.

Our task is to define a logical interpretation of $S$ in $T$. According to Definition 1, we need to find a formula $\alpha_<$ in the signature of $T$ (which only allows the use of $+$) that captures the meaning of the $<$ relation in $S$.

We can achieve this with the following formula:

$\alpha_<(X, Y) := \exists Z (X + Z = Y \land \neg (X = Y))$

This remark explains the meaning of the formula $\alpha_<(X, Y)$. Remark: This formula states that $X < Y$ if and only if there exists a natural number $Z$ such that $X + Z = Y$ and $X$ is not equal to $Y$. This effectively defines the order relation in terms of addition.

Constructing the Reduction

The logical interpretation provides us with a mechanical way to translate any formula $\phi$ in the signature of $S$ into a corresponding formula $\phi'$ in the signature of $T$. We simply replace each occurrence of the $<$ relation in $\phi$ with its definition $\alpha_<(X, Y)$.

Let’s consider a specific example: \[\phi := \forall X \exists Y (X < Y)\] This formula $\phi$ expresses the property that for every natural number $X$, there exists a larger natural number $Y$ (which is a true statement in the structure $S$).

To construct the corresponding formula $\phi'$ in the signature of $T$, we replace $X < Y$ with $\alpha_<(X, Y)$: \[\phi' := \forall X \exists Y (\exists Z (X + Z = Y \land \neg (X = Y)))\]

Now, $\phi'$ is a formula in the language of Presburger arithmetic. Crucially, by the definition of our logical interpretation, we have: \[(\mathbb{N}, <) \models \phi \iff (\mathbb{N}, +) \models \phi'\] This means $\phi$ is true in the structure $S$ if and only if $\phi'$ is true in the structure $T$.

This theorem describes the implication of the reduction from the theory of natural numbers with order to Presburger arithmetic.

Theorem 2. Since Presburger arithmetic is decidable, this reduction implies that the first-order theory of natural numbers with order is also decidable.

Example: Adding the Even Predicate

Let’s enhance the previous example by introducing a unary relation "even" to our structure $S$. This relation will contain all even natural numbers. Our new structure $S$ becomes $(\mathbb{N}, <, \text{even})$, and we will still reduce it to Presburger arithmetic, $T = (\mathbb{N}, +)$.

To define a logical interpretation, we need to provide formulas in the signature of $T$ for all relations in $S$. We already have $\alpha_<$ from the previous example, and now we need to define $\alpha_{\text{even}}$:

$\alpha_<(X, Y) := \exists Z (X + Z = Y \land \neg (X = Y))$ (as before)
$\alpha_{\text{even}}(X) := \exists Z (X = Z + Z)$

This remark explains the meaning of the formula $\alpha_{\text{even}}(X)$. Remark: The formula $\alpha_{\text{even}}(X)$ asserts that $X$ is an even number if and only if there exists a natural number $Z$ such that $X$ is the sum of $Z$ with itself. This correctly captures the notion of evenness using only addition.

Example Formula Transformation

Consider the following formula $\phi$ in the signature of $S$: \[\phi := \forall X \exists Y (X < Y \land \text{even}(Y))\] This formula expresses the statement that there are infinitely many even numbers.

To transform $\phi$ into a formula $\phi'$ in the signature of $T$, we replace $X < Y$ with $\alpha_<(X, Y)$ and $\text{even}(Y)$ with $\alpha_{\text{even}}(Y)$: \[\phi' := \forall X \exists Y (\exists Z (X + Z = Y \land \neg (X = Y)) \land \exists Z' (Y = Z' + Z'))\] Here, $Z'$ is used to avoid variable name clashes, although both $Z$ and $Z'$ are existentially quantified.

This transformed formula $\phi'$ is now a valid formula in Presburger arithmetic. It demonstrates how we can express properties involving both order and evenness within the language of addition.

This theorem describes the implication of the reduction when adding the even predicate.

Theorem 3. This reduction further reinforces that the first-order theory of $(\mathbb{N}, <, \text{even})$ is decidable, as it can be reduced to the decidable theory of Presburger arithmetic.

Example: Reduction from Integers with Order to Natural Numbers with Order and Even Predicate

This example demonstrates a more intricate reduction, where the universe of the structures is different. We aim to reduce the first-order theory of integers with order, $FO(\mathbb{Z}, <)$, to the first-order theory of natural numbers with order and the even predicate, $FO(\mathbb{N}, <, \text{even})$.

Structure $S$: Integers with the total order relation ($<$), represented as $(\mathbb{Z}, <)$.
Structure $T$: Natural numbers with the total order relation ($<$) and the even predicate, represented as $(\mathbb{N}, <, \text{even})$.

To establish the reduction, we will define an isomorphism between the integers and a structure derived from the natural numbers. We can visualize the integers as an infinite line extending in both directions. We "fold" this line onto the natural numbers, mapping non-negative integers to even natural numbers and negative integers to odd natural numbers. This mapping can be expressed as follows:

$0 \in \mathbb{Z} \mapsto 0 \in \mathbb{N}$
$1 \in \mathbb{Z} \mapsto 2 \in \mathbb{N}$
$-1 \in \mathbb{Z} \mapsto 1 \in \mathbb{N}$
$2 \in \mathbb{Z} \mapsto 4 \in \mathbb{N}$
$-2 \in \mathbb{Z} \mapsto 3 \in \mathbb{N}$
and so on...

Now we need to define the formula $\alpha_<$ that captures the order relation $\prec$ on integers using the order relation $<$ and the even predicate on natural numbers. We use $\prec$ to denote the order on integers and $<$ for the order on natural numbers to avoid confusion.

\[\begin{aligned}\alpha_\prec(X, Y) := &(\text{even}(X) \land \text{even}(Y) \land X < Y) \\&\lor (\neg \text{even}(X) \land \neg \text{even}(Y) \land Y < X) \\&\lor (\text{even}(X) \land \neg \text{even}(Y)) \\&\lor (\neg \text{even}(X) \land \text{even}(Y) \land X < Y)\end{aligned}\]

This remark provides a detailed explanation of the formula $\alpha_\prec(X, Y)$. Remark: This formula covers all possible cases for comparing two integers $X$ and $Y$ based on their corresponding natural numbers:

Both $X$ and $Y$ are non-negative: They are mapped to even natural numbers, and their order is the same as in $\mathbb{N}$.
Both $X$ and $Y$ are negative: They are mapped to odd natural numbers, and their order is reversed.
$X$ is non-negative and $Y$ is negative: $X \prec Y$ is always false, and $X$ is mapped to an even number while $Y$ is mapped to an odd number, so the disjunct is always true.
$X$ is negative and $Y$ is non-negative: $X \prec Y$ is always true. $X$ is mapped to an odd number and $Y$ to an even number. The order in $\mathbb{N}$ doesn’t matter since the disjunct will always be true.

This logical interpretation demonstrates that the theory of integers with order can be "simulated" within the theory of natural numbers with order and the even predicate.

This theorem describes the implication of the reduction from the theory of integers with order.

Theorem 4. Since $FO(\mathbb{N}, <, \text{even})$ is decidable (as shown in the previous example), this reduction implies that the first-order theory of integers with order, $FO(\mathbb{Z}, <)$, is also decidable.

Conclusion

In this lecture, we have explored the powerful concepts of logical reductions and interpretations. These tools provide a rigorous framework for comparing the expressive power of different logical theories. We began with a simple reduction from the theory of natural numbers with order to Presburger arithmetic, demonstrating how to define the order relation using addition. We then extended this reduction to include the even predicate, showcasing the versatility of logical interpretations.

Furthermore, we tackled a more complex scenario, reducing the theory of integers with order to the theory of natural numbers with order and the even predicate. This reduction involved a change of universe and highlighted the importance of establishing isomorphisms between structures.

These examples illustrate how logical reductions can be used to determine the relative complexity of theories. By reducing a theory to another theory with known decidability properties, we can establish the decidability or undecidability of the original theory.

Follow-up Questions:

Can we define addition using only the order relation in first-order logic? No, it is not possible to define addition using only the order relation in first-order logic. This is because the order relation alone cannot express the recursive nature of addition.
What other theories can we compare using logical reductions? Logical reductions can be applied to a wide range of theories, including theories of strings, trees, graphs, and various arithmetic theories. The possibilities are vast and depend on finding suitable interpretations between the theories.
How can we extend this framework to other logical formalisms, such as second-order logic? The concept of logical interpretations can be extended to higher-order logics. In second-order logic, for example, we would quantify over sets of elements, and the interpretations would involve defining relations between sets. This opens up avenues for comparing the expressive power of different logical systems.

This remark suggests further avenues for studying logical reductions and interpretations. Remark: The study of logical reductions and interpretations is a rich and active area of research in logic and theoretical computer science. It provides valuable insights into the foundations of mathematics and computation, and it has deep connections to areas such as model theory, automata theory, and complexity theory.

--- title: "Logical Theories and Reductions" 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 realm of logical theories, with a particular focus on first-order theories. We introduce the concept of *logical reductions* as a powerful tool for comparing the expressive power of these theories. Recall that a *theory* is defined as a set of formulas that are true within a *fixed structure*. This perspective gives rise to a decision problem: given a formula and a predefined structure, we seek to determine the truth value of the formula within that structure. Unlike traditional model checking, where the structure is part of the input, fixing the structure beforehand allows us to reason about *infinite structures*, significantly enriching the problem's complexity and interest. The primary goal is to establish a framework, analogous to algorithmic reductions in computability theory, that enables us to determine the relative complexity of different logical theories. By doing so, we can gain a deeper understanding of their expressive capabilities and limitations. # Algorithmic Reductions In the realm of computability theory, *many-to-one reductions* serve as a cornerstone for comparing the difficulty of computational problems. Suppose we have two problems, $P$ and $Q$, where $P$ is intuitively considered \"easier\" and $Q$ is considered \"harder\". A reduction from $P$ to $Q$ is established through a *computable function* $F$. This function takes any input $X$ for problem $P$ and transforms it into a corresponding input $X'$ for problem $Q$. The crucial property of this transformation is that it preserves the truth value of the problem instances. Formally, the answer to problem $P$ for input $X$ is true if and only if the answer to problem $Q$ for input $X'$ is true. This can be expressed as: $$P(X) \iff Q(F(X))$$ where $P(X)$ denotes the answer to problem $P$ with input $X$, and $Q(F(X))$ denotes the answer to problem $Q$ with input $F(X)$. ::: tcolorbox **Example:** Consider problem $P$ as determining if a number is even, and problem $Q$ as determining if a number is divisible by 4. We can reduce $P$ to $Q$ by defining $F(X) = 2X$. If $X$ is even (i.e., $P(X)$ is true), then $2X$ is divisible by 4 (i.e., $Q(F(X))$ is true). Conversely, if $2X$ is divisible by 4, then $X$ must be even. ::: This implies that if we have an algorithm to solve $Q$, we can use it to solve $P$ by first applying the reduction function $F$. Consequently, if $P$ is undecidable, then $Q$ must also be undecidable. # Logical Reductions The concept of reduction, powerful in comparing computational problems, can be elegantly extended to the realm of logical theories. Let $S$ and $T$ be two structures, and our goal is to demonstrate that the logical theory of $S$ is \"easier\" than that of $T$. To achieve this, we need a *computable function* that maps a formula $\phi$, expressed in the signature of $S$, into a corresponding formula $\phi'$, expressed in the signature of $T$. This mapping must satisfy a crucial property: $\phi$ holds true over structure $S$ if and only if $\phi'$ holds true over structure $T$. Formally: $$S \models \phi \iff T \models \phi'$$ This establishes a logical reduction from the theory of $S$ to the theory of $T$. In essence, it means that if we can decide the truth of formulas in the theory of $T$, we can also decide the truth of formulas in the theory of $S$ by using the aforementioned computable function to translate between the two. :::: tcolorbox This theorem describes the implication of a logical reduction between two theories in terms of decidability. ::: theorem **Theorem 1**. *If there exists a logical reduction from the theory of structure $S$ to the theory of structure $T$, and the theory of $T$ is decidable, then the theory of $S$ is also decidable. Conversely, if the theory of $S$ is undecidable, then the theory of $T$ must also be undecidable.* ::: :::: # Logical Interpretations A *logical interpretation* is a specific and powerful type of logical reduction. It provides a systematic way to construct the transformation function $F$, not arbitrarily, but by directly leveraging a well-defined relationship between the structures $S$ and $T$. The core idea is to describe the \"easier\" structure $S$ as a logical transformation of the \"harder\" structure $T$. :::: tcolorbox This definition formally introduces the concept of a logical interpretation between two structures. ::: {.def:logical_interpretation .definition} **Definition 1**. *A logical interpretation of structure $S$ in structure $T$, denoted as $S \leq_L T$, is defined by a set of formulas in the signature of $T$ that effectively \"encode\" the relations of $S$ within $T$. Specifically, for each relation $R$ in $S$ (including the universe, which can be seen as a unary relation), we associate a formula $\alpha_R$ in the signature of $T$. This formula $\alpha_R$ has the same number of free variables as the arity of $R$.* *The interpretation must ensure that the set of tuples from the universe of $T$ that satisfy $\alpha_R$ is *isomorphic* to the relation $R$ in $S$. In other words, there exists a bijection between the elements of the universe of $S$ and a subset of the universe of $T$ (defined by $\alpha_U$ where $U$ is the universe of $S$) that preserves the structure defined by the relations in $S$.* ::: :::: ::: tcolorbox This remark highlights the core concept behind logical interpretations. **Remark:** We are essentially \"simulating\" the structure $S$ within the structure $T$ using the logical language of $T$. Each relation in $S$ is \"translated\" into a logical definition within $T$. ::: The significance of this definition lies in its constructive nature. Once we have a logical interpretation, we can automatically derive the reduction function $F$ that maps formulas from $S$ to $T$, as we will see in subsequent examples. # Example: Reduction from Natural Numbers with Order to Presburger Arithmetic We will now illustrate the concept of logical interpretation with a concrete example. We aim to show that the first-order theory of natural numbers with order, denoted as $FO(\mathbb{N}, <)$, is reducible to Presburger arithmetic, which is the first-order theory of natural numbers with addition, denoted as $FO(\mathbb{N}, +)$. - Structure $S$: Natural numbers with the total order relation ($<$), represented as $(\mathbb{N}, <)$. - Structure $T$: Natural numbers with addition ($+$), represented as $(\mathbb{N}, +)$. Our task is to define a logical interpretation of $S$ in $T$. According to Definition [1](#def:logical_interpretation){reference-type="ref" reference="def:logical_interpretation"}, we need to find a formula $\alpha_<$ in the signature of $T$ (which only allows the use of $+$) that captures the meaning of the $<$ relation in $S$. We can achieve this with the following formula: - $\alpha_<(X, Y) := \exists Z (X + Z = Y \land \neg (X = Y))$ ::: tcolorbox This remark explains the meaning of the formula $\alpha_<(X, Y)$. **Remark:** This formula states that $X < Y$ if and only if there exists a natural number $Z$ such that $X + Z = Y$ and $X$ is not equal to $Y$. This effectively defines the order relation in terms of addition. ::: ## Constructing the Reduction The logical interpretation provides us with a mechanical way to translate any formula $\phi$ in the signature of $S$ into a corresponding formula $\phi'$ in the signature of $T$. We simply replace each occurrence of the $<$ relation in $\phi$ with its definition $\alpha_<(X, Y)$. Let's consider a specific example: $$\phi := \forall X \exists Y (X < Y)$$ This formula $\phi$ expresses the property that for every natural number $X$, there exists a larger natural number $Y$ (which is a true statement in the structure $S$). To construct the corresponding formula $\phi'$ in the signature of $T$, we replace $X < Y$ with $\alpha_<(X, Y)$: $$\phi' := \forall X \exists Y (\exists Z (X + Z = Y \land \neg (X = Y)))$$ Now, $\phi'$ is a formula in the language of Presburger arithmetic. Crucially, by the definition of our logical interpretation, we have: $$(\mathbb{N}, <) \models \phi \iff (\mathbb{N}, +) \models \phi'$$ This means $\phi$ is true in the structure $S$ if and only if $\phi'$ is true in the structure $T$. :::: tcolorbox This theorem describes the implication of the reduction from the theory of natural numbers with order to Presburger arithmetic. ::: theorem **Theorem 2**. *Since Presburger arithmetic is decidable, this reduction implies that the first-order theory of natural numbers with order is also decidable.* ::: :::: # Example: Adding the Even Predicate Let's enhance the previous example by introducing a unary relation \"even\" to our structure $S$. This relation will contain all even natural numbers. Our new structure $S$ becomes $(\mathbb{N}, <, \text{even})$, and we will still reduce it to Presburger arithmetic, $T = (\mathbb{N}, +)$. To define a logical interpretation, we need to provide formulas in the signature of $T$ for all relations in $S$. We already have $\alpha_<$ from the previous example, and now we need to define $\alpha_{\text{even}}$: - $\alpha_<(X, Y) := \exists Z (X + Z = Y \land \neg (X = Y))$ (as before) - $\alpha_{\text{even}}(X) := \exists Z (X = Z + Z)$ ::: tcolorbox This remark explains the meaning of the formula $\alpha_{\text{even}}(X)$. **Remark:** The formula $\alpha_{\text{even}}(X)$ asserts that $X$ is an even number if and only if there exists a natural number $Z$ such that $X$ is the sum of $Z$ with itself. This correctly captures the notion of evenness using only addition. ::: ## Example Formula Transformation Consider the following formula $\phi$ in the signature of $S$: $$\phi := \forall X \exists Y (X < Y \land \text{even}(Y))$$ This formula expresses the statement that there are infinitely many even numbers. To transform $\phi$ into a formula $\phi'$ in the signature of $T$, we replace $X < Y$ with $\alpha_<(X, Y)$ and $\text{even}(Y)$ with $\alpha_{\text{even}}(Y)$: $$\phi' := \forall X \exists Y (\exists Z (X + Z = Y \land \neg (X = Y)) \land \exists Z' (Y = Z' + Z'))$$ Here, $Z'$ is used to avoid variable name clashes, although both $Z$ and $Z'$ are existentially quantified. This transformed formula $\phi'$ is now a valid formula in Presburger arithmetic. It demonstrates how we can express properties involving both order and evenness within the language of addition. :::: tcolorbox This theorem describes the implication of the reduction when adding the even predicate. ::: theorem **Theorem 3**. *This reduction further reinforces that the first-order theory of $(\mathbb{N}, <, \text{even})$ is decidable, as it can be reduced to the decidable theory of Presburger arithmetic.* ::: :::: # Example: Reduction from Integers with Order to Natural Numbers with Order and Even Predicate This example demonstrates a more intricate reduction, where the universe of the structures is different. We aim to reduce the first-order theory of integers with order, $FO(\mathbb{Z}, <)$, to the first-order theory of natural numbers with order and the even predicate, $FO(\mathbb{N}, <, \text{even})$. - Structure $S$: Integers with the total order relation ($<$), represented as $(\mathbb{Z}, <)$. - Structure $T$: Natural numbers with the total order relation ($<$) and the even predicate, represented as $(\mathbb{N}, <, \text{even})$. ::: center ::: To establish the reduction, we will define an isomorphism between the integers and a structure derived from the natural numbers. We can visualize the integers as an infinite line extending in both directions. We \"fold\" this line onto the natural numbers, mapping non-negative integers to even natural numbers and negative integers to odd natural numbers. This mapping can be expressed as follows: - $0 \in \mathbb{Z} \mapsto 0 \in \mathbb{N}$ - $1 \in \mathbb{Z} \mapsto 2 \in \mathbb{N}$ - $-1 \in \mathbb{Z} \mapsto 1 \in \mathbb{N}$ - $2 \in \mathbb{Z} \mapsto 4 \in \mathbb{N}$ - $-2 \in \mathbb{Z} \mapsto 3 \in \mathbb{N}$ - and so on\... Now we need to define the formula $\alpha_<$ that captures the order relation $\prec$ on integers using the order relation $<$ and the even predicate on natural numbers. We use $\prec$ to denote the order on integers and $<$ for the order on natural numbers to avoid confusion. $$\begin{aligned}\alpha_\prec(X, Y) := &(\text{even}(X) \land \text{even}(Y) \land X < Y) \\&\lor (\neg \text{even}(X) \land \neg \text{even}(Y) \land Y < X) \\&\lor (\text{even}(X) \land \neg \text{even}(Y)) \\&\lor (\neg \text{even}(X) \land \text{even}(Y) \land X < Y)\end{aligned}$$ ::: tcolorbox This remark provides a detailed explanation of the formula $\alpha_\prec(X, Y)$. **Remark:** This formula covers all possible cases for comparing two integers $X$ and $Y$ based on their corresponding natural numbers: 1. Both $X$ and $Y$ are non-negative: They are mapped to even natural numbers, and their order is the same as in $\mathbb{N}$. 2. Both $X$ and $Y$ are negative: They are mapped to odd natural numbers, and their order is reversed. 3. $X$ is non-negative and $Y$ is negative: $X \prec Y$ is always false, and $X$ is mapped to an even number while $Y$ is mapped to an odd number, so the disjunct is always true. 4. $X$ is negative and $Y$ is non-negative: $X \prec Y$ is always true. $X$ is mapped to an odd number and $Y$ to an even number. The order in $\mathbb{N}$ doesn't matter since the disjunct will always be true. ::: This logical interpretation demonstrates that the theory of integers with order can be \"simulated\" within the theory of natural numbers with order and the even predicate. :::: tcolorbox This theorem describes the implication of the reduction from the theory of integers with order. ::: theorem **Theorem 4**. *Since $FO(\mathbb{N}, <, \text{even})$ is decidable (as shown in the previous example), this reduction implies that the first-order theory of integers with order, $FO(\mathbb{Z}, <)$, is also decidable.* ::: :::: # Conclusion In this lecture, we have explored the powerful concepts of logical reductions and interpretations. These tools provide a rigorous framework for comparing the expressive power of different logical theories. We began with a simple reduction from the theory of natural numbers with order to Presburger arithmetic, demonstrating how to define the order relation using addition. We then extended this reduction to include the even predicate, showcasing the versatility of logical interpretations. Furthermore, we tackled a more complex scenario, reducing the theory of integers with order to the theory of natural numbers with order and the even predicate. This reduction involved a change of universe and highlighted the importance of establishing isomorphisms between structures. These examples illustrate how logical reductions can be used to determine the relative complexity of theories. By reducing a theory to another theory with known decidability properties, we can establish the decidability or undecidability of the original theory. **Follow-up Questions:** - Can we define addition using only the order relation in first-order logic? *No, it is not possible to define addition using only the order relation in first-order logic. This is because the order relation alone cannot express the recursive nature of addition.* - What other theories can we compare using logical reductions? *Logical reductions can be applied to a wide range of theories, including theories of strings, trees, graphs, and various arithmetic theories. The possibilities are vast and depend on finding suitable interpretations between the theories.* - How can we extend this framework to other logical formalisms, such as second-order logic? *The concept of logical interpretations can be extended to higher-order logics. In second-order logic, for example, we would quantify over sets of elements, and the interpretations would involve defining relations between sets. This opens up avenues for comparing the expressive power of different logical systems.* ::: tcolorbox This remark suggests further avenues for studying logical reductions and interpretations. **Remark:** The study of logical reductions and interpretations is a rich and active area of research in logic and theoretical computer science. It provides valuable insights into the foundations of mathematics and computation, and it has deep connections to areas such as model theory, automata theory, and complexity theory. :::