propositions Q0, Q1, Q2, Q3,, . . . of the formal system will actually have proofs within the system. These ‘provable’ propositions will have numbers which constitute some set in ℕ in fact the set P of ‘theorems’ considered above. We have, in effect, already seen that there is an algorithm for generating, one after the other, all the propositions with proofs in some given formal system. (As outlined earlier, the ‘nth proof’ Πn is obtained algorithmically from n. All we have to do is look at the last line of the nth proof to find the ‘nth proposition provable within the system’, i.e. the nth
...more
