Godel numbering
Summary
One can define a system ("Godel numbering") for encoding expressions and derivations (in some logical system) as numbers. All the syntactic operations needed to verify derivations are recursive and can be represented in arithmetic. This shows that any logical theory which includes arithmetic is powerful enough to talk about itself. This idea is used to construct self-referential sentences in Godel's Incompleteness Theorem and related results.
Context
This concept has the prerequisites:
- first-order logic (One wants to arithmetize expressions in first order logic.)
- proofs in first-order logic (One needs to show a deductive calculus for a logical system can be arithmetized.)
- representability in arithmetic (Arithmetization requires showing that things are representable in arithmetic.)
Goals
- Define a system for assigning numbers ("Godel numbers") to expressions and derivations in a first-order language
- Be aware that all the syntactic manipulations needed to verify a proof are representable in arithmetic
- Work through the details of the above
Core resources (read/watch one of the following)
-Paid-
→ A Mathematical Introduction to Logic
An undergraduate textbook in mathematical logic, with proofs.
Location:
Section 3.4, "Arithmetization of syntax," pages 224-234
Other notes:
- The definition of recursive functions (i.e. those representable in axiomatic number theory) is different from (but equivalent to) the usual one.
Supplemental resources (the following are optional, but you may find them useful)
-Free-
→ Wikipedia
See also
-No Additional Notes-