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).

Background notions

Metamathematics -- "a program ... in which they [formalist mathematicians e.g. Hilbert, Bernays etc] aim in particular to establish the consistence of classical mathematics" (Kleene 1952:59) study of a formal mathematical system by use of the system itself

"metamathematics includes the description or definition of formal systems as well as the investigation of properties of formal systems. In dealing with a particular formal system, we may call the system the object theory, and the metamathematics relating to it its metatheory.... sthe object theory is not properly a theory at all as we formerly understood the term, but a system of meaningless objects like the positions in a game of chesss, subject to maechanical manipulations like the moves in chess. The object theory is described ans studied as a sytem of symbols and of objects built up oout of symbols. The symbols are regarded simply as various kinds of recognizable objects. To fix our ideas we may think of them concretely as marks on paper..." (p. 62)

"a program which makes a mathematical theory itself the object of exact mathematical study. In a mathematical theory, we study a system of mathematical objects (Kleene 1952:59)... all the meanings of all the words are left out of account, and all the conditions which govern their use in the theory are stated explicitly" (Kleene 1952:60)

"objects" here are "propositions" written down in "symbols"

axiomatization: cf p. 59 -- "the propositions of the theory arranged deductively, some of them from which the others are logically deducible, ... axioms (or postulates)" (p. ("formal axiomatics" §8) ... state the logical princples for our axioms... [??]

logical principles ... will now be given effectin part perhaps by new axioms, and in some part at least by rules fpermitting the inference of one sentence from another or others. Since we have abstracted eintirely from the content or matter, leaving only the form, we say that the original theory has been formalized." (p. 60)

Symbolization: "to build a new a symbolic language specially for the purpose of expressing the theory ... (The symobls in a symbolic language will usually correspond to whole words instead of to letters; and sequences of symbols which correspond to sentences will be called "formulas" ... sympole symbolic notations which lend themselves to manipulation by formal rules...p. 51)

Rosser 1939

Rosser's description of "a suitable logic L"

I. Notion of "two logics" -- (1) "logic of ordinary discourse", (2) formal logic

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

"For the considerations which follow, the meaning of the symbols is immaterial, and it is desirable that they be forgotten.... the undefined terms (hence the formulas and proofs) are countable... [does he mean here by implication that the formulas a proofs are thus undefined?]..."(Godel 1934:53)

II. Logic must contain the connective NOT (NEGATION): "Amongst the symbols of L must be one, ~, which is interpreted as "not", the 'contradictory' when the symbol is applied before a sentence.

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

Necessary for the "fixpoint" or fix point lemma -- where a function A is converted to a Godel number G_A, and the Godel number G_A is in turn converted to a numeral #g = 0^...' such that A(#g):

For any formula B(y) there is a sentence A such that ⊢f A ↔ B(#A) [B-B-J 2002:222)

Notions of formula, variable, substitution or replacement,

VI. Logic must contain a symbol ⊃ defined as IMPLICATION (as defined the formal sentential-connective sense): If formula A expresses sentence S and formula B expresses sentence T and A ⊃ B expresses "IF S THEN T" (IMPLICATION in the formal sense).

IV. A process whereby certain of the propostions of L are specified as "provable".

VI.1 "Provable" defined to mean that if A is provable & A⊃B is provable then so is B.

V. The notion of simple consistency and ω-consistency in L:

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.

VIII. The notion of diagonalization of a function φ(x,y) (yielding "z=φ(x,x)" ) must be expressible in L:

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 [sic ??] y.

x is a NUMBER that represents formula f_x(v)
y is a NUMBER that represents formula f_y
f_y is a formula to be plugged into f_x(v)
z = φ is the NUMBER of formula f_x( f_y )

VII. A system for arithmetizating of formulas must be defined in L:

"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 repalaced 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

Flawed example

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.