Thiel I 227 ff
Incompleteness Theorem/Goedel/Thiel: ... this metamathematical statement corresponds in F to a one-digit statement form G(x) which then must occur somewhere in the counting sequence. If G(x) takes the h'th place, it is therefore identical with the propositional form called Ah(x) there.
Goedel's result will be, that in F neither the proposition G(h) arising from G(x) by the insertion of h nor its negative ~G(h) is derivable.
"Undecidable in F".
Suppose G(h) is derivable in F, then only the derivation of true statements would be allowed, so G(h) would also be true.
Thus, since G(x) was introduced as an image of $Ax(x) in F, $Ah(h) would be valid. But that would mean, since Ah(x) is identical with G(x), $G(h). G(h) would therefore be non-derivable in F - this is a contradiction.
>Derivation, >Derivability.
This derivation first only proves the validity of the "if-then-statement" S G(h)>$ G(h). This must now be inserted:
(S G(h)>$ G(h))> $ G(h).
This follows from the general scheme (A>~A)>~A.
On the other hand, if we then assume that the negative ~G(h) is derivable, then ~G(h) would also be true. This would be equivalent to the validity of ~$ Ah(h) thus with S Ah(h).
Thiel I 228
This in turn agrees with S G(h), so that both assertion and negative would be derivable, and we would have a formal contradiction. If F is contradiction-free at all, our second assumption S ~G(h) is not valid either. This is an undecidable assertion.
Cf. >Decidability, >Indecidability.
Thiel I 228
This proof sketch establishes a program. Important roles in the execution of this program are played by the "Goedelization" and the so-called "negative representability" of certain relations in F.
Def Goedelization: Goedelization is first of all only a reversibly definite assignment of basic numbers to character sequences. We want to put the expressions of F into bracket-free form.
>Goedel numbers.
For this we write the logical connective signs not between, but in front of the expressions. We write the logical operators as "indices" to the order functor G.
Terminology order functor G.
Quantifiers: we treat quantifiers as two-digit functors whose first argument is the index, the second the quantified propositional form.
>Quantifiers, >Quantification.
Thiel I 229
Then the statement (x)(y)(z) ((x=y)>(zx = zy) gets the form
(x)(y)(z)G > G = xyG = G times zxG times zy.
We can represent the members of the infinite variable sequences in each case by a standard letter signaling the sort and e.g. prefixed points: thus for instance x,y,z,...by x,°x,°°x,...As counting character we take instead of |,||,|||,... zeros with a corresponding number of preceding dashes 0,'0,''0,...
>Sequences.
With this convention, each character in F is either a 0 or one of the one-digit functors G1 (the first order functor!), ', ~.
Two-digit is G2, three-digit is G4, etc.
Thiel I 229
E.g. Goedelization, Goedel number, Goedel number:
Prime numbers are assigned in each case:....
Primes.
Thiel I 230
In this way, each character string of F can be uniquely assigned a Goedel number and told how to compute it. Since every basic number has a unique representation as a product of prime numbers, it can be said of any given number whether it is a Goedel number of a character string of F at all.
Metamathematical and arithmetical relations correspond to each other: example:
Thiel I 230
We replace the x by 0 in ~G=x'x and obtain ~G = 0'0.
The Goedel number of the first row is:
2
23 x 3
13 x 5
37 x 7
29 x 11
37, the Goedel number of the second row of characters is:
2
23 x 3
13 x 5
31 x 7
29 x 11
31.
The transition from the Goedel number of the first row to that of the second row is made by division by 5
6 x 11
6 and this relation (of product and factor) is the arithmetic relation between their Goedel numbers corresponding to the metamathematical relation of the character rows.
Thiel I 231
These relations are even effective, since one can effectively (Goedel says "recursively") compute the Goedel number of each member of the relation from those of its remaining members.
>Recursion.
The most important case is of course the relation Bxy between the Goedel number x, a proof figure Gz1...zk and the Goedel number y of its final sequence...
Thiel I 233
"Negation-faithful representability": Goedel shows that for every recursive k-digit relation R there exists a k-digit propositional form A in F of the kind that A is derivable if R is valid, and ~A if R does not (..+..).
We say that the propositional form A represents the relation R in F negation-faithfully.
Thiel I 234
After all this, it follows that if F is ω-contradiction-free, then neither G nor ~G is derivable in F. G is an "undecidable statement in F".
The occurrence of undecidable statements in this sense is not the same as the undecidability of F in the sense that there is no, as it were, mechanical procedure.
>Decidability.
Thiel I 236
It is true that there is no such decision procedure for F, but this is not the same as the shown "incompleteness", which can be seen from the fact that in 1930 Goedel had proved the classical quantifier logic as complete, but there is no decision procedure here, too.
Def Incomplete/Thiel: a theory would only be incomplete if a true proposition about objects of the theory could be stated, which demonstrably could not be derived from the axiom system underlying the theory. ((s) Then the system would not be maximally consistent.)
Whether this was done in the case of arithmetic by the construction of Goedel's statement G was for a long time answered in the negative, on the grounds that G was not a "true" arithmetic statement.
This was settled about 20 years ago by the fact that combinatorial propositions were found, which are also not derivable in the full formalism.
Goedel/Thiel: thus incompleteness can no longer be doubted. This is not a proof of the limits of human cognition, but only a proof of an intrinsic limit of the axiomatic method.
Thiel I 238 ff
One of the points of the proof of Goedel's "Underivability Theorem" was that the effectiveness of the metamathematical derivability relation corresponding to the self-evident effectiveness of all proofs in the full formalism F, has its exact counterpart in the recursivity of the arithmetic relations between the Goedel numbers of the proof figures and final formulas, and that this parallelism can be secured for all effectively decidable metamathematical relations and their arithmetic counterparts at all.
>Derivation, >Derivability.
