Peano Arithmetic & Gödel — Part 6: Gödel's Completeness Theorem

graph TD RefSound["Ref: Soundness (Part 4)"] DefConsistent["Def: T consistent iff T ⊬ ⊥"] DefMaxCons["Def: Maximal consistent: T maximal, consistent"] LemLindenbaum["Lem: Lindenbaum: every consistent T extends to maximal consistent Δ"] DefHenkin["Def: Henkin theory: ∃xφ ∈ Δ ⇒ φ(c/x) ∈ Δ for some constant c"] LemHenkinExt["Lem: Every consistent T extends to Henkin theory T' in expanded language"] LemTermModel["Lem: From maximal Henkin T'', build term model M: |M| = closed terms, truth = membership"] ThmCompleteness["Thm: Completeness: T consistent ⇒ T has model"] CorCompact["Cor: Compactness: T ⊨ φ ⇒ finite T₀ ⊆ T with T₀ ⊨ φ"] RefSound --> ThmCompleteness DefConsistent --> DefMaxCons DefMaxCons --> LemLindenbaum LemLindenbaum --> LemHenkinExt DefHenkin --> LemHenkinExt LemHenkinExt --> LemTermModel LemTermModel --> ThmCompleteness ThmCompleteness --> CorCompact classDef definition fill:#b197fc,color:#fff,stroke:#9775fa classDef lemma fill:#74c0fc,color:#fff,stroke:#4dabf7 classDef theorem fill:#51cf66,color:#fff,stroke:#40c057 classDef corollary fill:#1abc9c,color:#fff,stroke:#16a085 classDef ref fill:#bdc3c7,color:#333,stroke:#95a5a6 class RefSound ref class DefConsistent,DefMaxCons,DefHenkin definition class LemLindenbaum,LemHenkinExt,LemTermModel lemma class ThmCompleteness theorem class CorCompact corollary