User talk:Wvbailey/Explication of Godel's incompleteness theorems

Kleene 1952: Development of a "formal system"

This form of number theory extends for all the real numbers: -∞, 0, +∞. Kleene 1952 starts at chapter IV A FORMAL SYSTEM then skips to Chapter VIII FORMAL NUMBER THEORY.

To develop this theory he immediately defines what he calls three "function symbols" + (plus), * (times), ' (successor). But the development is worth repeating to see what is going on. In summary:

Symbols:

His entire collection of symbols is Logical symbols: ⊃ (implies), & (and), V (or), ￢(not), ∀ (for all), ∃ (there exists). Predicate symbols: = (equals). Function symbols: + (plus), * (times), ' (successor). Individual symbols: 0 (zero). Variables: a, b, c, .... Parentheses: (, ).

Juxtaposition (concatenation):

Term: From these symbols and the notion of juxtaposition (concatenation) of these symbols he defines term.

Formula: From term he defines formula.

Scope of a variable, free variable: He develops the notions of "scope of a variable" and "free variable".

Substitution: Then he introduces the notion of substitution.

Transformation rules: in particular the three deductive schema. Here the symbol ⇒ is being used in place of a long line under the expression, and indicates "yields" in the tautological or derivational sense. The symbols A, B are formulas, A(x), A(t) indicate a formula with a free variable:

A & (A ⊃ B )⇒ B
C ⊃ A(x)⇒ C ⊃ ∀xA(x)
A(x) ⊃ A(t)⇒ ∃xA(x) ⊃ C

Postulates: These transformation rules are three of 21 postulates that he divides into three categories:

GROUP A1: Postulates for the propositional calculus (formulas with no free variables)
GROUP A2: (Additional) Postulates for the predicate calculus (incorporating formulas A(x) with a free variable x)
GROUP B: (Additional) Postulates for number theory

It is in the last group B that we see the "function symbols" + and * appear. As these are axioms, they are worth repeating:

13. A(0) & ∀x(A(x)⊃A(x') ⊃ A(x). (axiom of induction, cf Peano axioms)
14. a'=b' ⊃ a=b. (Peano axiom)
15. ￢a' = 0. (Peano axiom)
16. a=b ⊃ (a=c ⊃ b=c). (Peano axiom)
17. a=b ⊃ a'=b' (Peano axiom)
18. a+0=a (additive identity defined)
19. a+b'=(a+b)' (addition function-symbol defined in a recursive sense, cf Kleene 1952:186)
20. a*0=0 (multiplicative identity defined, an axiom)
21. a*b'=a*b+a (multiplication function-symbol defined in a recursive sense, cf Kleene 1952:186)

Finally, he defines the notion of immediate consequence of the premise(s) by the rules.

In the final chapter he introduces the INDUCTION RULE over formulas with variables i.e. A(x). From all of this he deduces (proves) the familiar "arithmetic laws", including "association", "distribution", and "commutation" for + and *, the notions of additive identity and multiplicative identity, and the notions of multiplicative and additive inverses, the order properties (<, ≤, >, ≥), other more unusual properties such as "connexity, irreflexiveness, asymmetry, inequalities under addition and multiplication), but in particular interest the existence and uniqueness of quotient and remainder.

From this follows the notion of formally provable and we have, in a nutshell the same development used by Kurt Gödel in his Incompleteness theorems (1931) (which is fact where Kleene's development stops until he introduces the notion of primitive recursive functions. —Preceding unsigned comment added by Wvbailey (talk • contribs) 14:55, 9 November 2007 (UTC)[reply]