## Thursday, November 8, 2018

### Provability from finite and infinite theories

Let #s be the Goedel number of s. The following fact is useful for thinking about the foundations of mathematics:

Proposition. There is a finite fragment A of Peano Arithmetic such that if T is a recursively axiomatizable theory, then there is an arithmetical formula PT(n) such that for all arithmetical sentences s, A → PT(#s) is a theorem of FOL if and only if T proves s.

The Proposition allows us to replace the provability of a sentence from an infinite recursive theory by the provability of a sentence from a finite theory.

Sketch of Proof of Proposition. Let M be a Turing machine that given a sentence as an input goes through all possible proofs from T and halts if it arrives at one that is a proof of the given sentence.

We can encode a history of a halting (and hence finite) run of M as a natural number such that there will be a predicate HM(m, n) and a finite fragment A of Peano Arithmetic independent of M (I expect that Robinson arithmetic will suffice) such that (a) m is a history of a halting run of M with input m if and only if HM(m, n) and (b) for all m and n, A proves whether HM(m, n).

Now, let PT(n) be ∃mHM(m, n). Then A proves PT(#s) if and only if there is an m0 such that A proves HM(m0, n). (If A proves PT(#s), then because A is true, there is an m such that HM(m, #s), and then A will prove HM(m0, #s). Conversely, if A proves HM(m0, #s), then it proves ∃mHM(m, #s).) And so A proves PT(#s) if and only if T proves s.