Peano Arithmetic & Gödel — Part 5: Formalization & Gödel Numbering

graph TD RefPA["Ref: PA (Charts 1–3)"] DefLPA["Def: Language L_PA (0, S, +, ·)"] DefAxPA["Def: Axioms of PA (induction schema)"] DefGodelNum["Def: Gödel numbering: #(term), #(formula), #(proof)"] DefPrimRec["Def: Primitive recursive functions"] LemPrimRec["Lem: Gödel numbering is primitive recursive"] DefNum["Def: Numeral n̄ for n ∈ ℕ"] DefSubst["Def: Substitution sub(φ, x, t) = φ(t/x)"] LemSubstPR["Lem: sub is primitive recursive"] DefRep["Def: Strong representability: R(n) ↔ PA ⊢ ρ(n̄)"] LemRep["Lem: Recursive relations are representable in PA"] DefProof["Def: Proof predicate Prf(m,n): m codes proof of formula #n"] LemProofRep["Lem: Prf is representable in PA"] RefPA --> DefLPA RefPA --> DefAxPA DefLPA --> DefGodelNum DefAxPA --> DefGodelNum DefAxPA --> DefRep DefPrimRec --> LemPrimRec DefGodelNum --> LemPrimRec DefNum --> DefSubst DefSubst --> LemSubstPR LemPrimRec --> LemSubstPR LemPrimRec --> LemRep LemRep --> LemProofRep DefSubst --> LemProofRep DefRep --> LemProofRep classDef definition fill:#b197fc,color:#fff,stroke:#9775fa classDef lemma fill:#74c0fc,color:#fff,stroke:#4dabf7 classDef ref fill:#bdc3c7,color:#333,stroke:#95a5a6 class RefPA ref class DefLPA,DefAxPA,DefGodelNum,DefPrimRec,DefNum,DefSubst,DefRep,DefProof definition class LemPrimRec,LemSubstPR,LemRep,LemProofRep lemma