Propositional Logic · Quantifiers

Lesson 3

Nikolai Chukhin · Alexander S. Kulikov

For the curious 🤓
In 1936, Alonzo Church proved that there is no algorithm that would take as input a statement about positive integers, including quantifiers, equality signs, addition, and multiplication, and would answer whether this statement is true or false. This result can be proven as follows: given a Turing machine \(M\) and its input \(w\), one can construct a formula \(\phi_{M,w}\) in the language \((\mathbb{Z}_{\ge 0}, +, \times)\) with a single free variable \(x\) such that the statement \(\exists x \colon \phi_{M,w}\) is true if and only if \(M\) halts on \(w\). To do this, the protocol of the operation of machine \(M\) on input \(w\), which ends in an accepting state, is encoded (using addition and multiplication) as a huge integer.