6.2 Proof of the completeness theorem

Henkin's proof is a powerful method for showing completeness in formal systems. It builds a maximal consistent set of sentences and uses it to construct a model that satisfies all sentences in the set.

This approach is crucial for understanding completeness theorems. By demonstrating that every consistent set of sentences has a model, Henkin's proof establishes the link between syntax and semantics in logical systems.

Henkin's Proof and Consistency

Proving Completeness Using Henkin's Method

• Henkin's proof provides a method for demonstrating the completeness of a formal system
• Involves constructing a maximal consistent set of sentences from a given consistent set
• Utilizes Lindenbaum's lemma to extend the consistent set to a maximal consistent set
• The maximal consistent set serves as the basis for constructing a model that satisfies all sentences in the set

Properties of Consistent Sets

• A consistent set of sentences is a set that does not contain any contradictions
• No sentence and its negation can be derived simultaneously from a consistent set
• Consistency is a fundamental requirement for constructing a model that satisfies the sentences
• Maximal consistent sets play a crucial role in Henkin's proof by ensuring completeness

Lindenbaum's Lemma and Maximal Consistency

• Lindenbaum's lemma states that any consistent set of sentences can be extended to a maximal consistent set
• A maximal consistent set is a consistent set that cannot be further extended without introducing inconsistency
• The lemma guarantees the existence of a maximal consistent set for any given consistent set
• Maximal consistent sets have the property that for every sentence, either the sentence or its negation is included in the set ($\forall \varphi, \varphi \in \Gamma \lor \neg \varphi \in \Gamma$)

Model Construction

Witnesses and Term Models

• A witness is a constant symbol that is used to represent an element in the domain of a model
• Witnesses are introduced for each existential sentence in the maximal consistent set to ensure its satisfaction
• A term model is constructed using the maximal consistent set and the introduced witnesses
• In a term model, the domain consists of equivalence classes of terms, where terms are equivalent if their equality is provable from the maximal consistent set

Canonical Models and Completeness

• The canonical model is a model constructed from the maximal consistent set and the term model
• The canonical model satisfies all sentences in the maximal consistent set by construction
• The truth value of a sentence in the canonical model is determined by its membership in the maximal consistent set
• The existence of the canonical model for any consistent set of sentences proves the completeness of the formal system
• Completeness means that every valid sentence is provable within the system ($\Gamma \vDash \varphi \implies \Gamma \vdash \varphi$)

Constructing the Canonical Model

• The domain of the canonical model is the set of equivalence classes of terms in the term model
• Function symbols are interpreted as functions on the equivalence classes, preserving the equality relations
• Predicate symbols are interpreted based on their occurrence in the maximal consistent set
• Constants and variables are assigned to their corresponding equivalence classes in the term model
• The canonical model satisfies all sentences in the maximal consistent set, establishing completeness