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, objects, axiomatizaton, logical principles, symbolization

Derived from Kleene 1952 (italics added here and there for emphasis):

Metamathematic: The mathematical study of a formal mathematical system by use of the system itself

Metamathematics is "a program ... in which they [formalist mathematicians e.g. Hilbert, Bernays etc] aim in particular to establish the consistency of classical mathematics" (Kleene 1952:59).

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

"The 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 chess, subject to mechanical manipulations like the moves in chess. The object theory is described and studied as a system of symbols and of objects built up out 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)

"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" (p. 60)

Criteria for a formal system

Axiomatization: cf p. 59 -- "the propositions of the theory arranged deductively, some of them from which the others are logically deducible "

Logical principles ... will now be given effect in part perhaps by new axioms, and in some part at least by rules permitting the inference of one sentence from another or others. Since we have abstracted entirely 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" ... 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

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

Notions of formula, variable, substitution or replacement,

VI. Logic must contain a symbol ⊃ standing for IMPLICATION:

IF formula A expresses sentence S and formula B expresses sentence T THEN 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":

"Provable" is defined to mean that IF A is provable, AND A⊃B is provable, THEN so is B (i.e. modus ponens)

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 for system 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

Godel 1934: 5 requirements for formal logic L

I. Ability to Godelize formulas written in logic L":

The symbols and formulas of L must be "Godelizable" as numbers AND
The class of axioms and relation of immediate consequence" is [primitive-] recursive

II. An expression in L for every natural number n can be expressed as a sequence of formulas z_n:

Every natural number n must be expressable as a sequence of formulas z_n, AND
The relationship between n and Godel number G(z_n) of formula-sequence zz_n is recursive.

Example: If "3" = sss0, where sign 0 has the equivalent symbol "clear_A" = 00010001₂ = 17₁₀ and s has the symbol "increment_A" = 00100001₂ = 33₁₀ and the string sss0 is formed by concatenation (the dots are just visual separators and have no other significance):

0.s.s.s = 17₁₀.33₁₀.33₁₀.33₁₀ = 00010001₂.00100001₂.00100001₂.00100001₂

This string is parsed as blocks of 8-bit bytes, each block a conventional binary byte, but written where the least significant byte (LSB) is on the left and the most signficant byte (MSB) is on the right i.e.:

0.s.s.s = 17₁₀*(2⁸)⁰ + 33₁₀*(2⁸)¹ + 33₁₀*(2⁸)² + 33₁₀*(2⁸)³ = 555,819,281₁₀

The individual formulas for the terms can be recovered by successive applications of N = Q*D + R,

Right-most byte: 33₁₀ = INT(555819281₁₀,2²⁴),

Next byte: 33₁₀ = INT(MOD(555819281,²⁴),2¹⁶), etc, etc.

III. The symbol for NOT: This needs work

A symbol that stands for NOT (i.e. NEGATION) must exist in the system L, AND
There must exist two variables v, w, AND
For all relations R of two variables, i.e. R(v,w) THEN there exists a formula "R(z_p, z_q) is provable" if the relation holds of p, q [p, q are formulas ...].

DITTO for NOT-R(z_p, z_q).

IV. A symbol ∀ (for all)

V. The system must be free of contradiction: Requirements for simple-consistency and ω-consistency:

Simple consistency: IF R(v,w) THEN by the law of contradiction NOT-("R(z_p, z_q) is provable" & ~"R(z_p, z_q) is provable")

ω-consistency: IF F(v) is a recursive function of one variable v THEN the NOT( "formulas NOT-∀vF(v) & F(z₀) & F(z₁) &F(z₂), ... are provable" )

Charlesworth 1981 requirements for L (he calls it "S")

I. Guidelines for what constitues a proof, precise notions of "statement" and "logical way". Concrete use of Truth tables for NOT, OR, AND, IMPLIES but not ∀ and ∃ because these cannot be defined by means such as truth tables. So therefore a formal system of symbols and rules of manipulation are required.

"...a finite list of statments linked together in alogical way." (p. 112)

II. Two levels of system: English language (metalanguage), formal system

PROOF: "Each statement in the proof must be an axiom or must follow from preceding statements in the proof by one of the rules of the system, which are called "rules of inference""

III. Requirement for well-formed wff [statements?, formulas?]:

"Whenever the symbols of S₀ are given their intended meaning, a formal statement and its negation correspond to assertions in English which are so well formed and unambiguous that one of them is true." (p. 112) AND

"It would be necessary to speicify, in terms of form alone, which expressions are formal statements. ... all that is required is an algorithm α₂for checking whether or not a particular expression is a formal statement." (p. 112-113)

Condition 1: The system specifies only a finite number of symbols AND there exists an algorithm α₁ that checks any symbol-string for "well-formed" :

Condition 2: Definition of theorem and proof :

A theorem in S is a formal statement at the last line of a proof, AND

A proof is a finite list of [wff?] [statements? formulas?], AND

There exists an algorithm α₂ to check whether or not any particular finite list of [wff ? expressions?] is a proof in S

Condition 3: Any wff can be NEGATED:

An algorithm α₃ can turn any wff into its negation, AND

The negation is a wff in S, AND

Within the interpretation of the symbols of S, either "wff" evaluates to "truth" or "~wff" evaluates to "truth", but not both

Condition 4: Representation of any natural number n as a formal formula z_n in S: [z_n is Godel's usage, i.e. z_n = sss0 for n="3"]

Given any natural number, there exists an algorithm α₄ that can provide the z_n ["notation", formula?] in S for the number n, AND

If, given a formal statement [formula?] F(x)|_zn the notation z_m [formula?] for a number m replaces the notation z_n for a number n then the new expression F(x)|_zn is a formal statement [formula?] in S.

Condition 5:

For each machine-program P there exists a number predicate F_P in S, AND

For each natural number n, program P (process?) with input n prints YES iff F_P(n) is a theorem, AND

Then P halts.

LEMMA 1: Diagonalization requirement:

Given that system S satisfies conditions 1-5, then there exists an algorithm φ that generates the theroems in S, AND there is an algorithm ψ that generates [?] F₁(1), F₂(2), F₃(3), ... where the list F₁, F₂, F₃, ... are all the number predicates in S.

LEMMA 2:

Assume that system S satisfies conditions 1-5. If S is complete AND given a formal statement F is S, then an algorithm exists to determine BOTH " F is a theorem " AND " F is NOT a theorem ".

Charlesworth's proof

Given the above, if S is complete then both following are possible outcomes:

P with input n prints "YES" iff F_n(n) is NOT a theorem of S.
P with input n prints "YES" iff F_m(n) is a theorem of S.

Assign number m => n:

P with input m prints "YES" iff F_m(m) is NOT a theorem of S.
P with input m prints "YES" iff F_m(m) is a theorem of S.

As both cannot happen by the law of contradiction, (NOT_A & A) is a FALSEHOOD, then the assumption that S is complete is flawed.

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.

Machine-based formal system

H = hypothetical machine that attempts to prove the consistency of ["the system"? What is "the system"?]. H has its own number k that could be run by U if present in place N, i.e. if [N] = k then U would be running program k = program that is H.

Thus we seem to need two U's, (1) U to the whole shebang and (2) inner U2 as part of H that runs the number n = [N] under test.

U = universal machine that can run any wfn (well-formed number) that is loaded into register N.
R = register that holds count of successful decisions (whatever they may represent)
N = register that holds the number-under-test n, i.e. [N] = n. Number "n" will be investigated by decision-machine D (or algorithms α₁ = α_wff, α₂ = α_proof, α₃ = α_negation) and then "run" by U.

Uber-U runs the whole show.

Encoding

Symbols: {0, 1}

Alphabet: strings of concatenated 1's separated by a single 0, as the following:

10
110
1110
11110
111110

wff Part I: Concatenations of the above alphabet starting a 1 at the left end and ending with the last string of 1's on the far right. Everything to the right beyond this should be 0's because the JUMP_IF_ZERO will be looking at the entire register (actually a tape).

Example: a formula (theorem) will be something like this (written in "backwards" binary):

1101111011111111111111011110111111000000000...etc

The following is not well formed because the sequences of more than qty one 0 are inside the 1's:

1110011111010001110000000000000....etc.

wff Part II: parsing failures: If all the "instructions" were single-parameter (unclear if possible need for a "jump-address) and because of forward jumps) then not all strings would represent legitimate "opcodes". Given that some of the "opcodes" have parameters, not all strings will be wffs. For example, if "jump" were encoded by 1111110 and the jump-to address were encoded by 1111....1110, then if for some reason the unpacking came "out of sync" then 1111....1110 might be assumed to be an "opcode", but it would fail to parse. To avoid double work, the parsing can also act as part of the "wff-checking".

Binary encoding versus unary: Unary decrementing is a simple matter of shifing 'down' (shift toward the "open" left end).

1110... in unary is "3". "3"-1= "2" = 1100.... But this is not the same as 1110... in binary is "7". Shift left results in 1100... = 1/2*N = "3" + a remainder of 1 that falls out the left end. This is not the same as "decrement".

Unary incrementing is a matter of printing the "head" (least-significant bit) and shifting 'up' (binary multiply-by-2 and add 1).

Although the instructions are written in unary, the string shown above is actually binary because it contains 0's between the 1's. So it must be considered binary. Thus (again, arithmetic in backwards binary):

10000... = wff

01000... = NOT-wff

11000... = wff

00100... = NOT-wff

10100... = wff

01100... = NOT-wff

11100... = wff

00010... = NOT-wff

10010... = NOT-wff

01010... = NOT-wff

11010... = wff

00110... = NOT-wff

10110... = wff

01110... = NOT-wff

11110... = wff

00001... = NOT-wff

10001... = NOT-wff

Unpacking strategy for a wff: by shifting

110 into the first "unpacking" register,
11110 into the 2nd unpacking register,
111111111111110 into the 3rd
11110 into the 4th
1111110 into the 5th, etc.