🤔Proof Theory Unit 6 – Completeness and Compactness Theorems

Key Concepts and Definitions

• Completeness refers to the property of a formal system where every logically valid formula is provable within the system
• Compactness states that if every finite subset of a set of formulas is satisfiable, then the entire set is satisfiable
• A formal system consists of a language, axioms, and inference rules used to derive theorems
• Soundness ensures that every provable formula in a formal system is logically valid
  • Complementary to completeness
• Satisfiability means a formula can be made true under some interpretation or model
• Logical consequence $\Gamma \vDash \varphi$ holds if every model of $\Gamma$ is also a model of $\varphi$
• Provability $\Gamma \vdash \varphi$ means $\varphi$ can be derived from $\Gamma$ using the system's inference rules
• A theory $T$ is a set of formulas closed under logical consequence

Completeness Theorem: Statement and Significance

• States that for a sound formal system, every logically valid formula is provable within the system
  • If $\Gamma \vDash \varphi$, then $\Gamma \vdash \varphi$
• Establishes a strong connection between semantic and syntactic notions of logical consequence
• Guarantees that a formal system captures all logically valid inferences
• Fundamental result in mathematical logic with implications for automated theorem proving
• Applies to various logics, including propositional and first-order logic
• Allows for the systematic derivation of all logical truths within a system
• Provides a basis for completeness proofs of specific theories (Peano arithmetic)

Proof Strategies for Completeness

• Henkin's proof is a common approach for proving completeness in first-order logic
• Involves constructing a maximal consistent set of formulas that includes the original set
  • Maximal consistent set contains every formula or its negation, but not both
• Extends the language with new constant symbols to ensure the existence of witnesses
• Builds a canonical model using equivalence classes of terms in the extended language
• Shows that the canonical model satisfies the maximal consistent set
• Concludes that if a formula is not provable, then its negation is satisfiable
• Alternatively, completeness can be proven using the compactness theorem and Löwenheim-Skolem theorems

Compactness Theorem: Overview and Importance

• States that a set of formulas is satisfiable if and only if every finite subset is satisfiable
• Equivalent to the statement that a set of formulas is unsatisfiable if and only if some finite subset is unsatisfiable
• Fundamental result in model theory with wide-ranging applications
• Allows for reasoning about infinite sets of formulas using finite means
• Implies the existence of non-standard models of arithmetic and analysis
• Enables the construction of models with specific properties using the compactness argument
• Plays a crucial role in the proof of Gödel's completeness theorem for first-order logic
• Used to establish the decidability and undecidability of various theories

Proving the Compactness Theorem

• One approach is to use the completeness theorem and the finiteness of proofs
• Assume every finite subset of a set $\Sigma$ is satisfiable
• By completeness, every finite subset is consistent (no contradiction can be derived)
• If $\Sigma$ were unsatisfiable, then by completeness, $\Sigma \vdash \bot$ (a contradiction)
• Any proof of $\bot$ from $\Sigma$ would use only finitely many formulas from $\Sigma$
• This finite subset would be unsatisfiable, contradicting the assumption
• Therefore, $\Sigma$ must be satisfiable
• Another proof uses ultraproducts to construct a model of $\Sigma$ from models of its finite subsets

Applications in Logic and Mathematics

• Compactness is used to prove the upward and downward Löwenheim-Skolem theorems
  • Every satisfiable theory has models of arbitrary infinite cardinality
• Allows for the construction of non-standard models of arithmetic and analysis
  • Models that contain "infinite" natural numbers or "infinitesimal" real numbers
• Employed in the study of large cardinals and set-theoretic independence proofs
• Used to establish the completeness and decidability of various theories (real-closed fields)
• Applies to propositional and first-order logic, but fails for second-order logic and beyond
• Compactness arguments are common in model theory, algebra, and topology
• Helps analyze the expressive power and limitations of formal systems

Connections to Other Theorems

• Completeness and compactness are closely related to Gödel's incompleteness theorems
  • Incompleteness shows limitations of completeness for sufficiently strong theories
• Compactness is equivalent to the Boolean prime ideal theorem in the presence of the axiom of choice
• Compactness for propositional logic is related to Tychonoff's theorem in topology
• The Löwenheim-Skolem theorems are direct consequences of compactness
• Omitting types theorem in model theory relies on compactness
• Completeness and compactness play a role in the foundations of mathematics
  • Consistency and independence proofs for axiom systems (ZFC set theory)

Common Pitfalls and Misconceptions

• Completeness does not imply that every true statement in a theory is provable
  • Gödel's incompleteness theorems show this is impossible for sufficiently strong theories
• Compactness does not hold for logics stronger than first-order, such as second-order logic
• The existence of non-standard models may seem counterintuitive
  • But they are a natural consequence of compactness
• Completeness and compactness do not eliminate the need for semantic arguments
  • They provide a bridge between syntax and semantics
• Compactness arguments often involve non-constructive proofs
  • The existence of a model is shown without explicitly constructing it
• The relationship between completeness, compactness, and the axiom of choice can be subtle
  • Some forms of compactness are equivalent to choice principles