Extensions of the system A I
S. W. P. Steen · Cambridge University Press eBooks · 1972
The system A′ We have seen that the system A I is incomplete and that any extension of it which remains a formal system will also be incomplete. We could add, as extra axioms, some A-true but A I -unprovable statements so as to obtain more A-true statements as theorems in the resulting extended system. But as long as we have a formal system it will still be incomplete and an irresolvable statement can be constructed on the same lines as before. We can do this programme in a systematic manner as follows: We have an effective method for constructing an irresolvable ℒ-true ℒ-statement in a formal system ℒ which contains recursive number theory and negation. Call this ℒ-statement G {ℒ}. We first form G {A I } and then the system G ′ which consists of the system A I with the extra axiom G {A I }; having formed G (λ) we construct G ( S λ) by adding the extra axiom G { G (λ) }. Having formed the systems A I , G ′,…, G (λ) ,… we then form the system G * as the union of all the systems A I , G ′,…, i.e. the system A I with all the extra axioms we added in forming the systems G ′,…; this system again will be formal, hence we can form G { G * } and the system G *′ which is the system G * plus the extra axiom G { G * }. So we can proceed through the constructive ordinals . But we shall have to stop before we come to the end of the constructive ordinals, otherwise we shall cease to have a formal system.