User:Wvbailey/Explication of Godel's incompleteness theorems

The following is an exploration of how to explain the first Gödel incompleteness theorem (Theorem VI, 1931).

Rosser 1939

I. Notion of "two logics" --

(1) "logic of ordinary discourse"
"formal logic L"

"propositions of L" are formulas built per "certain rules of structure"

symbols, interpretations, rules of structure interpretations will be declarative sentences (not necessarily true) of "ordinary discourse" -- "expressions in L".

II. "Amonst the symbols of L must be one, ~, which is interpreted as "not", the 'contradictory' when the symbol is applied before a sentence.

III.1. For each integer, there must be a formula in L which denotes that integer.

III.2 notion of "variables"

III.3 notion of "substitution" or "replacement"

IV. A process whereby certain of the propostions of L are specied as "provable". [notion of simple consistency and ω-consistency]

V. If F and ~F are provable in L, then all propositions of L are provable. The non-provability of any formula whatever of L implies the simple consistency of L. ω-consistency implies simple consistency; but if L is not simply constent then not ω-consistent.

VI. Modus ponens: Symbol ⊃ of L such that if formula A expresses sentence S and formula B expresses sentence T and A ⊃ B expresses "IF S THEN T".

VI.1 "Provable means that if A & A⊃B are provable then so is B.

VII. Notion of arithmetization of formulas: "For every formula, a number is assigned. However, not all numbers are assigned to formulas. If a number is assigned to a formula, the formula can always be found...". (p. 226). Thus, when numbers have been assigned to formulas, statements about formulas can be repalced by statements about numbers. That is, if P is a property of formulas,we can find a property of numbers, Q, such that the formula A has the property P if and only if the number of A has the property Q.

"LEMMA 1. Let "x has the property Q [a property of numbers] " be expressible in L. then for suitable L, there can be found a formula F of L, with a number n, such that F expresses "n has the property Q." That is, F expresses "F has the property P [a property of formulas]." p. 227

VIII. "We now call attention to an extra assumption implicit in the "for suitable L" of Lemma 1, namely that "z=φ(x,x)" be expressible in L, where φ(x,y) is the function [with the following] DEFINITION: φ(x,y) is the number of the formula got by taking the formula with the number x and replacing all occurrences of v in it by the formula of L which denotes the number of y.

φ is a NUMBER.
x is a NUMBER.

Registers holding individual numbers of arbitrary size::

010EJZ[E]; 020EJ[E]; 03CLR_P; 04DCR_P; 05INC_P; 06CLRi; 07DCRi; 08INCi; H }. Each instruction is considered to be tally marks, and a zero (blank) separates them. Thus "

or if we had 16 total instructions

0|nop; ~~1.E|movek_J,~~ 2.E.|JFZi; 3.E.|JF,E; 4.E.|JBZi; 5.E.|JB; ~~6|clrJ, 7|dcrJ, 8|incJ,~~ 9|clr_P; A|dcr_P; B|inc_P; C|clri; D|dcri; E|inci; F|halt }.

MOVE("3",5): clrP.inc_P.inc_P.inc_P.inc_P.inc_P.clri.inci.inci.inci = 8AAAAABDDD₁₆

JZ(5,*+q): movek_J.5.clrP.inc_P.inc_P.inc_P.inc_P.inc_P.JFZi

DCR(5): dcri.

J (*-r): movek_12.JB = 1+m+1

i.e. clear register 5 can be written without the use of the "clri" command: what would be this "godel" number? the need for absolute numbers screws this up a bit (doesn't allow for just simple fixed-place e.g. 4 bit encoding -- these numbers signify tally marks): 9.B.B.B.B.B.2.4.D.5.10. = 0|||||||||0|||||||||||0|||||||||||0|||||||||||0|||||||||||0|||||||||||0||0||||0||||||||||||||0|||||0||||||||||

clrP

incP

JFZi

4

dcri

JB

10

Example: INC(2) is expressible by x) = 0111011 (in binary written backwards), 14+32+64 = 110₁₀

Formula "x" = INC(v) = 011101^v

Formula "y" = INC^v number in y is CLR(y).INC(y).INC(y)....INC(y) = i.e. the concatenation of these:

[Y]=y =

Formula "x(y=v)" = 01110

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.