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

Metamathematics: 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.

Machine-based formal system

All the authors agree on certain requirements that must be present in the "system", however it is designed:

1 A specification of the notions of "proof" and "theorem"
2 Specification of what constitutes a wff
3 A specification of what the notion "provable" means
4 Logic must contain the connective NOT (Negation) so a proof [?] theorem [?] can be negated
5 Logic must contain the connective → for implication
6 Consistency of the system itself: thus the system must be free of contradiction and a proof of A and ~A is not possible: ~(A & ~A)
7 Ability to Godelize propositions expressed in the system
8 Every natural number must be expressible in the system
9 A notion of "for all"
10 Ability to diagonalize within the system

H determines: "This proof-sequence results in a Theorem" & "It is NOT the case that "This proof-seqeuence results in a Theorem".

1 A specification of the notions of "proof" and "theorem":

We are free to specify that every theorem ends in HALT. this rules out a huge category

A proof will be, by definition, a string of symbols { 1, 0 }. The alphabet will be defined as a string of 1's followed by a 0.

10

110

1110

etc.

A word (line of code) will be two of these concatenated. The first one will be chosen from a library of 16 [?] OPCODES. In the metalanguage these have the following definitions:

halt: 10

110

1110

11110

111110

1111110

11111110

111111110

The second will be a similar string considered to be written in unary code and will represent the OPERAND -- either a register or an address.

Each line of code: that start at line 1 and progress sequentially through lines 2, 3, ... . These notions of "lines of code" as symbolized by "1", "2", "3" is in the metalanguage. The actual implementation can be in binary, unary, unary single-select (CASE), odd-ball symbols, etc.

1 clear C 2 2
2 jz A 4 3
3 dcr A 4 4
4 inc C 2 2
5 halt

Each line will have 5 parts to it [or possibly three?] the "pipe" | here is a visual separator and has no other purpose

1 clear C 2 2 | 2 jz A 4 3 | 3 dcr A 4 4 | 4 inc C 2 2 | 5 halt

This is good because it lends itself to an easy discovery of whether the proof is well formed or not.

Another more primitive coding as two-variable lines to be concatenated:

1 clear
2 C
3 test
4 A
5 jZ
6 13
7 dcr
8 A
9 inc
10 C
11 ju
12 3
13 halt

clear C test A jZ 13 dcr A inc C ju 3 halt

The spaces here are intentional; they act as the separators.

A theorem will be the last line in the sequence.

5: Logic must contain the connective → for implication:

If a machine TABLE is drawn as a sequence of "states" every state can be written as 1 or two transition-arrows leaving the state are to be written as the following, where a and b are the identifiers of the next states, and c is the contents of place Z compared to 0. SR is the "program counter" or "state register"

((c → b) & (~c → a)) = ((c & b) V (~c & a)) => SR

[ ([Z]=0) → b) & (~([Z]=0) → a) ] = [ ([Z]=0) & b) V (~([Z]=0) & a) ]

The single-exit case occurs when b = a, and in this case:

[ (c → a) & (~c → a) ] = [ (c & a) V (~c & a) ] = [ a ] => SR

4 Logic must contain the connective NOT (Negation) so a proof [?] theorem [?] can be negated:

Theorem will be the last line of a sequence

Example of machine

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- versus unary-encoding: Unary decrementing is a simple matter of shifing 'down' (shift toward the "open" left end.

_u1110... in unary is "3". "3"-1= "2" = 1100.... But this is not the same as binary ₂1110... = "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... = wff

Unpacking strategy for a wff: by shifting from e.g. register N into any register pointed to by index-register X (decimals are just for visualizations):

110.11110.111111111111110.111101111110.00000000...etc

load "X" with the address of the first free register
put 110 into the first "unpacking" register,
increment X, i.e. [X] +1 => X
11110 into the 2nd unpacking register,
increment X
111111111111110 into the 3rd
increment "X"
DO until [N]=0, then escape:

unpack into X
increment X