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 & 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 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":

(1) The symbols and formulas of L must be "Godelizable" as numbers AND

(2) The class of axioms and relation of immediate consequence" is [primitive-] recursive

II. Every natural number n can be expressed 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.

If "3" = sss0, where sign 0 has the equivalent symbol "clr_A" = 00010001₂ = 17₁₀ and s has the symbol "inc_A" = 00100001₂ = 33₁₀ and the string is formed by concatenation 0001.0001.00100001.00100001.00100001 and parsed as a string of conventional binary written left to right i.e.:

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

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

The individual formulas for the terms can be recovered by e.g. =INT(555,819,281₁₀,2^24), and MOD=555,819,281₁₀-INT(555,819,281₁₀,2^24); use MOD in the next formula, 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 ~("R(zp, zq) 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(z0) & F(z1) &F(z2), ... 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 _zn in S: [z_n is Godel's usage]

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.