Decidability of Logical Theories

Mathematical logic is the branch of mathematics that investigates mathematics itself, defining concepts like theorems, proofs, and truth

Computability theory is very relevant to some key results of mathematical logic

Our goal in this section is to explain in which domains an algorithm can be given that decides the truth of a theorem

Proving theorems is difficult! Here are three well-known examples using symbolic logic,

1. $\forall q\exists p\forall x,y[p>q\wedge (x,y>1\to xy\ne p)]$, there are infinitely many prime numbers, known to be true since Euclid, 2300 years ago
2. $\forall a,b,c,n[(a,b,c>0\wedge n>2)\to a^n+b^n\ne c^n]$, Fermat’s last theorem, infamously only proved in 1994 by Andrew Wiles
3. $\forall q\exists p\forall x,y[p>q\wedge (x,y>1\to (xy\ne p\wedge xy\ne p+2))]$, twin prime conjecture, unsolved

Can we automate this process? How can we approach this? Intuition from what we’ve learned says no

Formally, let’s treat these statements as strings and define a language consisting of true statements. Is this language decidable?

We define the alphabet as $\{\wedge ,\vee ,\neg ,(,),\forall ,\exists ,x,R_1,\dots ,R_k\}$, where $\wedge ,\vee ,$ and $\neg$ are called Boolean operations, ”(” and ”)” are just parentheses, $\forall$ and $\exists$ are quantifiers, $x$ denotes variables, and $R_1,\dots ,R_k$ are called relations

A string of the form $R_i(x_1,\dots ,x_k)$ is called an atomic formula has a arity $k$, and all occurrences of $R_i$ must have the same arity

A formula is a well-formed string over this alphabet

$\varphi$ is a formula if it

1. Is an atomic formula
2. Has the form ${\varphi }_1\wedge {\varphi }_2$, ${\varphi }_1\vee {\varphi }_2$, or $\neg {\varphi }_1$
3. Has the form $\exists x_i[{\varphi }_1]$ or $\forall x_i[{\varphi }_1]$

A quantifier may appear at any point, and its scope is the fragment of the statement appearing within the matched pair of parentheses or brackets following the quantified variable

All formulas are in prenex normal form, where quantifiers appear in the front of the formula

A variable that isn’t bound is called a free variable
A formula with no free variables is called a sentence or statement

Finally, we specify the universe over which variables may take values and specify the meaning of the relation symbols

A relation is a function from $k$-tuples to $\{\text{TRUE},\text{FALSE}\}$
The arity of a relation symbol must match that of its assigned relation

A universe together with an assignment of relations to relation symbols is called a model, formally we write $\mathcal{M}$ as a tuple $(U,P_1,\dots ,P_k)$ where $U$ is the universe and $P_i$ is the relation assigned to symbol $R_i$

The language of a model is the collection of formulas that use only the relation symbols the model assigns with the correct arity

If $\varphi$ is a sentence in the language of a model, $\varphi$ is either true or false in that model, and if it is true then we say $\mathcal{M}$ is a model of $\varphi$

If $\mathcal{M}$ is a model, we let the theory of M be the collection of true sentences in the language of that model, written as $\text{Th}(\mathcal{M})$

With all this in place, we can move on to our question

Theorem: $\text{Th}(\mathcal{N},+)$ is decidable

Proof:
Write the input as $\varphi =Q_1{x}_1{Q}_2{x}_2\dots Q_l{x}_l[\psi ]$, where $Q_i$ is either $\forall$ or $\exists$, and $\psi$ is a formula without quantifiers with variables $x_1,\dots ,x_l$

Define ${\varphi }_i=Q_{i+1}{x}_{i+1}{Q}_{i+2}{x}_{i+2}\dots Q_l{x}_l[\psi ]$
${\varphi }_i$ has $i$ free variables

For $i>0$, define the alphabet, ${\Sigma }_i=$ all size $i$ columns of $0$s and $1s$, and ${\Sigma }_0=\{[]\}$
A string over ${\Sigma }_i$ represents $i$ binary integers

For each such $i$, we construct a finite automaton $A_i$ that accepts strings ${\Sigma }_i$ corresponding to $i$-tuples $a_1,\dots ,a_i$ whenever ${\varphi }_i(a_1,\dots ,a_i)$ is true

To start with $A_l$, we observe that ${\varphi }_l=\psi$ is a Boolean combination of atomic formulas (single additions) that a DFA can verify straightforwardly

We then construct $A_i$ from $A_{i+1}$
If ${\varphi }_i=\exists x_{i+1}{\varphi }_{i+1}$ then we construct $A_i$ to operate as $A_{i+1}$, except it nondeterministically guesses the value of $a_{i+1}$ instead of receiving it
If ${\varphi }_i=\forall x_{i+1}{\varphi }_{i+1}$, it is equivalent to $\neg \exists x_{i+1}\neg {\varphi }_{i+1}$, thus we can construct the finite automaton that recognizes the complement of $A_{i+1}$ and then apply the same construction

$A_0$ accepts any input if ${\varphi }_0$ is true, so we test whether it accepts $ϵ$ and forward that value

Theorem: $\text{Th}(\mathcal{N},+,\times )$ is undecidable

Lemma: Let $M$ be a Turing machine and $w$ a string. We can construct a formula ${\varphi }_{M,w}$ in the language of $(\mathcal{N},+,\times )$ that contains a single free variable $x$, such that $\exists x{\varphi }_{M,w}$ is true if and only if $M$ accepts $w$

The idea is the formula says $x$ is a suitably encoded accepting computation history of $M$ on $w$, in a form that can be checked by the $+$ and $\times$ operations

The proof of this is mechanically very complicated, but results in reducing $A_{\text{TM}}$ to our problem and proving the theorem

Already, this is a very philosophically interesting theorem, but Kurt Gödel’s incompleteness theorems take it a step farther

A formal proof $\pi$ of a statement $x$ is a sequence of statements, $S_1,S_2,\dots ,S_l$, where $S_l=\varphi$ and each $S_i$ follows from the preceding statements and certain basic axioms about numbers, with the following reasonable (and provable) assumptions,

1. $\{⟨\varphi ,\pi ⟩\mid \pi \text{ is a proof of }\varphi \}$ is decidable
2. If a statement is provable then it is true

Theorem: The collection of provable statements in $\text{Th}(\mathcal{N},+,\times )$ is Turing-recognizable

From our assumption that we can construct a proof-checker, we can make an algorithm $P$ that tests each string as a candidate for a proof $\pi$ of $\varphi$

Theorem: Some true statement in $\text{Th}(\mathcal{N},+,\times )$ is not provable

Assume all true statements are provable, we can then construct a decider $D$, contradicting our earlier theorem,

On input $\varphi$, $D$ runs $P$ given in the proof in parallel on $\varphi$ and $\neg \varphi$
Since one of these is true and therefore provable by assumption, $P$ must halt and $D$ can decide the truth of $\varphi$

Let’s construct an example of a true but unprovable statement

$S=$ “On any input:

1. Obtain $⟨S⟩$ via the recursion theorem
2. Construct $\psi =\neg \exists c[{\varphi }_{S,0}]$
3. Run $P$ on input $\psi$
4. If $P$ accepts then accept”

${\psi }_{\text{unprovable}}$ is the construction we created in this machine

If there’s a proof of $\psi$ then we reach a contradiction in the behavior of $S$, so there must not be a proof, in which case $\psi$ is true as claimed