Description:
<jats:p>For the first Gödel incompleteness theorem, the existence in a formal system of arithmetic <jats:italic>L</jats:italic> of a sentence which is neither provable nor refutable, all that is required of the formula Th(<jats:italic>x</jats:italic>) of <jats:italic>L</jats:italic> used to express the notion ‘<jats:italic>x</jats:italic> is the g.n. (gödel number) of a theorem of <jats:italic>L</jats:italic>’ is mere numeralwise correctness, i.e. that for a numeral <jats:italic>n</jats:italic>, Th(<jats:italic>n</jats:italic>) is provable in <jats:italic>L</jats:italic> iff <jats:italic>n</jats:italic> is the g.n. of a theorem of <jats:italic>L</jats:italic>. It is well known that much more is needed for the second Gödel incompleteness theorem, the unprovability in <jats:italic>L</jats:italic> of the formula Con =<jats:sub>df</jats:sub> ¬(∃<jats:italic>y, z</jats:italic>)(Th(<jats:italic>y</jats:italic>) ∧ Th(<jats:italic>z</jats:italic>) ∧ neg(<jats:italic>z, y</jats:italic>)), which (if neg expresses negation) expresses the consistency of <jats:italic>L</jats:italic>. Conditions sufficient for this second theorem, more or less as stated by Hilbert-Bernays [1, p. 286] and elegantly formulated by Löb [2] may with a cavalier disregard for the distinction between use and mention be stated thus: The result of the first incompleteness theorem: there is a sentence <jats:italic>G</jats:italic> such that ⊢<jats:italic>G</jats:italic> ↔ ¬Th <jats:italic>G</jats:italic>), together with, if ⊢<jats:italic>A</jats:italic> then ⊢Th <jats:italic>A</jats:italic>, if ⊢(<jats:italic>A → B</jats:italic>) then ⊢(Th <jats:italic>A</jats:italic> → Th <jats:italic>B</jats:italic>), ⊢(Th <jats:italic>A</jats:italic> → Th Th <jats:italic>A</jats:italic>). On the other hand Feferman [3], Kreisel [4, p. 154] and Jeroslow [9] have given examples of systems and consistency formulae, based on numeralwise correct formulae Th(<jats:italic>x</jats:italic>), which <jats:italic>are</jats:italic> provable within the system.</jats:p>