6.1 Gödel's completeness theorem for first-order logic

Gödel's completeness theorem is a cornerstone of first-order logic. It shows that if a sentence is logically valid, it can be proved using first-order logic rules. This powerful result connects the semantic notion of truth with the syntactic concept of provability.

The theorem has far-reaching implications for mathematical logic and foundations. It establishes that first-order logic is complete, meaning all valid statements can be derived within the system. This provides a solid basis for formal reasoning in mathematics and computer science.

Completeness and Soundness

Gödel's Completeness Theorem and First-Order Logic

• Gödel's completeness theorem states that if a sentence is logically valid in first-order logic, then it can be proved using the rules of first-order logic
  • This means that the proof system of first-order logic is complete
  • For example, if a sentence like $\forall x (P(x) \rightarrow Q(x))$ is true in every model, then it can be proved using the rules of first-order logic
• First-order logic is a formal system that includes predicates, variables, quantifiers, and logical connectives
  • It allows for expressing complex mathematical statements and reasoning about them
  • First-order logic is more expressive than propositional logic, which only deals with simple propositions and connectives

Soundness and Consistency

• Soundness is a property of a logical system where every provable sentence is logically valid
  • In other words, if a sentence can be proved using the rules of the system, then it must be true in every model
  • Soundness ensures that the proof system does not allow for proving false statements
• Consistency is a property of a logical system where no contradiction can be derived
  • A contradiction is a sentence of the form $A \land \lnot A$, where both a sentence and its negation are provable
  • If a system is consistent, it means that it is impossible to prove both a sentence and its negation using the rules of the system

Models and Satisfiability

Models and Satisfiability

• A model is an interpretation of a first-order language that assigns meanings to the symbols in the language
  • A model consists of a non-empty domain (or universe) and an interpretation function that maps the symbols to elements, subsets, or relations on the domain
  • For example, a model for the language of arithmetic might have the natural numbers as its domain and interpret the symbol $+$ as the addition function
• A sentence is satisfiable if there exists a model in which the sentence is true
  • For instance, the sentence $\exists x (P(x) \land Q(x))$ is satisfiable if there is a model with an element in the domain that satisfies both predicates $P$ and $Q$
• A sentence is valid if it is true in every model
  • For example, the sentence $\forall x (P(x) \rightarrow P(x))$ is valid because it is true in every model, regardless of the interpretation of the predicate $P$

Validity and Logical Consequence

• Validity is a stronger notion than satisfiability, as a valid sentence is true in all models, while a satisfiable sentence is true in at least one model
  • Valid sentences are also called tautologies
  • If a sentence is valid, then its negation is unsatisfiable
• A sentence $\phi$ is a logical consequence of a set of sentences $\Gamma$ if every model that makes all the sentences in $\Gamma$ true also makes $\phi$ true
  • We write this as $\Gamma \models \phi$
  • Logical consequence is a semantic notion, based on the truth values of sentences in models

Proof Techniques

Henkin Construction

• The Henkin construction is a method for building a model of a consistent set of sentences in first-order logic
  • It is used in the proof of Gödel's completeness theorem to show that every consistent set of sentences has a model
• The construction proceeds by extending the original language with new constant symbols and adding sentences that specify the properties of these new constants
  • The new constants are used to ensure that every existential sentence in the set has a witness in the model
• The Henkin construction builds a model step by step, ensuring that the resulting model satisfies all the sentences in the original set
  • This is done by creating a complete consistent set of sentences that includes the original set and the new sentences added during the construction
• The Henkin construction demonstrates the close connection between consistency and satisfiability in first-order logic
  • If a set of sentences is consistent, then the Henkin construction can be used to build a model that satisfies the set
  • Conversely, if a set of sentences has a model, then it must be consistent, as an inconsistent set cannot have a model