|
4 From the conclusions of Section 2 there follows a remarkable result with regard to a consistency proof of the system P (and its extensions), which is expressed in the following proposition: Proposition XI: If c be a given recursive, consistent class63 of formulae, then the propositional formula which states that c is consistent is not c-provable; in particular, the consistency of P is unprovable in P,64 it being assumed that P is consistent (if not, of course, every statement is provable). The proof (sketched in outline) is as follows: Let c be any given recursive class of formulae, selected once and for all for purposes of the following argument (in the simplest case it may be the null class). For proof of the fact that 17 Gen r is not c-provable,65 only the consistency of c was made use of, as appears from 1, page 59; i.e. Wid(c) ® ~Bewc(17 Gen r) (23) i.e. by (6.1): Wid(c) ® (x) ~[x Bc (17 Gen r)] By (13), 17 Gen r = Sb(p 19|Z(p)) and hence: Wid(c) ® (x) ~[x Bc Sb(p 19|Z(p))] [197] i.e. by (8.1): Wid(c) ® (x) Q(x,p) (24) We now establish the following: All the concepts defined (or assertions proved) in Sections 266 and 4 are also expressible (or provable) in P. For we have employed throughout only the normal methods of definition and proof accepted in classical mathematics, as formalized in the system P. In particular c (like any recursive class) is definable in P. Let w be the propositional formula expressing Wid(c) in P. The relation Q(x,y) is expressed, in accordance with (8.1), (9) and (10), by the relation-sign q, and Q(x,p), therefore, by r [since by (12) r = Sb(q 19|Z(p))] and the proposition (x) Q(x,p) by 17 Gen r. In virtue of (24) w Imp (17 Gen r) is therefore provable in P67 (and a fortiori c-provable). Now if w were c-provable, 17 Gen r would also be c-provable and hence it would follow, by (23), that c is not consistent. It may be noted that this proof is also constructive, i.e. it permits, if a proof from c is produced for w, the effective derivation from c of a contradiction. The whole proof of Proposition XI can also be carried over word for word to the axiom-system of set theory M, and to that of classical mathematics A,68 and here too it yields the result that there is no consistency proof for M or for A which could be formalized in M or A respectively, it being assumed that M and A are consistent. It must be expressly noted that Proposition XI (and the corresponding results for M and A) represent no contradiction of the formalistic standpoint of Hilbert. For this standpoint presupposes only the existence of a consistency proof effected by finite means, and there might conceivably be finite proofs which cannot be stated in P (or in M or in A). Since, for every consistent class c, w is not c-provable, there will always be propositions which are undecidable (from c), namely w, so long as Neg(w) is not c-provable; in [198] other words, one can replace the assumption of w-consistency in Proposition VI by the following: The statement "c is inconsistent" is not c-provable. (Note that there are consistent c's for which this statement is c-provable.) Throughout this work we have virtually confined ourselves to the system P, and have merely indicated the applications to other systems. The results will be stated and proved in fuller generality in a forthcoming sequel. There too, the mere outline proof we have given of Proposition XI will be presented in detail. 63 C is consistent (abbreviated as Wid(c)) is defined as follows: Wid(c) = ($x) [Form(x) & ~Bewc(x)]. 64 This follows if c is replaced by the null class of formulae. 65 r naturally depends on c (just as p does). 66 From the definition of "recursive" on [179] up to the proof of Proposition VI inclusive. 67 That the correctness of w Imp (17 Gen r) can be concluded from (23), is simply based on the fact that–as was remarked at the outset–the undecidable proposition 17 Gen r asserts its own unprovability. 68 Cf. J. v. Neumann, 'Zur Hilbertschen Beweistheorie', Math. Zeitschr. 26, 1927.
Revista Matemáticas,
Educación e Internetâ |