The Gödel theorem.
Norwood Russell Hanson · Notre Dame Journal of Formal Logic · 1961
Gόdel demonstrates that any logical system which includes Arithmetic must be incomplete.For within such a system there will always be (wellformed, meaningful) formulae % , which are 'undecidable',-such that neither % nor ~ % is a theorem.Thus no decision procedure exists for Arithmetic; indeed if one did exist Arithmetic would be contradictory, -this is the crux of Gόdel's proof.Hence, if Arithmetic is consistent it must be incomplete.The original proof of this is very difficult.Most informal expositions, however, convey too little of the power and ingenuity of GodeΓs argument.Perhaps we can steer a middle course.Our aim will be intelligibility without undue sacrifice of rigour.The actual deduction (IV) presupposes a prior discussion of I. Decision Procedure, II.Recursive Functions and III.The Arithmetization of Logical Syntax. I. DECISION PROCEDURE General Notions:A formal mathematical system consists of symbols, and rules for their manipulation.Primitive (undefined) terms are the individual symbols.Formulae are finite sequences of primitive terms.Meaningful formulae are symbol-sequences constructed according to the rules of the system.Axioms (primitive formulae) are a sub-class of all the meaningful formulae. A rule of inference (R) defines the relation of 'immediate consequencesby R' between a set of meaningful formulae (premises) and a further meaningful formula (conclusion).This R may be 'from 21 and 21D58 infer 33 '.A finite procedure must be available for determining whether a formula is meaningful, or whether a conclusion is an immediate consequence of a set of premises.