Abstract

We’ve now proved our key version of the First Theorem, Theorem 42. If T is the right kind of ω-consistent theory including enough arithmetic, then there will be an arithmetic sentence GT such that T ￿ GT and T ￿ ¬GT. Moreover, GT is constructed so that it is true if and only if unprovable-in T (so it is true). Now recall that, for a p.r. axiomatized theory T , Prf T(m, n) is the relation which holds just if m is the super g.n. of a sequence of wffs that is a T proof of a sentence with g.n. n. This relation is p.r. decidable (see §25.4). Assuming T extends Q, it can capture any p.r. decidable relation, including Prf T (§22). So we can define..