🤔Mathematical Logic Unit 5 – Formal Proofs in First–Order Logic

Key Concepts and Definitions

• First-order logic extends propositional logic by introducing quantifiers, variables, and predicates to represent and reason about complex mathematical statements and structures
• Syntax defines the formal rules and symbols used to construct well-formed formulas (wffs) in first-order logic
  • Includes logical connectives (∧, ∨, ¬, →, ↔), quantifiers (∀, ∃), variables, constants, functions, and predicates
• Semantics assigns meaning to the formulas by defining truth values, interpretations, and models
• Validity refers to a formula that is true under all possible interpretations, while satisfiability means a formula is true under at least one interpretation
• Soundness ensures that the inference rules and axioms of a logical system only produce valid conclusions from valid premises
• Completeness guarantees that all valid formulas can be derived using the inference rules and axioms of the logical system
• Consistency means that a logical system cannot derive both a formula and its negation, avoiding contradictions

Syntax and Formation Rules

• The alphabet of first-order logic consists of variables (x, y, z, ...), constants (a, b, c, ...), function symbols (f, g, h, ...), predicate symbols (P, Q, R, ...), and logical connectives (∧, ∨, ¬, →, ↔)
• Terms are the basic building blocks of formulas and can be variables, constants, or function applications
  • Function applications are formed by applying a function symbol to a tuple of terms, e.g., f(x, g(y))
• Atomic formulas are the simplest well-formed formulas, formed by applying a predicate symbol to a tuple of terms, e.g., P(x, f(y))
• Complex formulas are built from atomic formulas using logical connectives and quantifiers
  • Negation (¬A), conjunction (A ∧ B), disjunction (A ∨ B), implication (A → B), and equivalence (A ↔ B)
  • Universal quantification (∀x A(x)) and existential quantification (∃x A(x))
• The scope of a quantifier is the formula it binds, and free variables are those not bound by any quantifier
• Formulas with no free variables are called sentences or closed formulas

Inference Rules and Axioms

• Inference rules allow the derivation of new formulas from existing ones, preserving truth and validity
• Modus Ponens (MP): From A and A → B, infer B
• Universal Instantiation (UI): From ∀x A(x), infer A(t) for any term t
• Existential Generalization (EG): From A(t) for some term t, infer ∃x A(x)
• Axioms are fundamental truths accepted without proof and serve as the foundation for deriving other formulas
• First-order logic often includes axioms for equality, such as reflexivity (∀x (x = x)), symmetry (∀x ∀y (x = y → y = x)), and transitivity (∀x ∀y ∀z ((x = y ∧ y = z) → x = z))
• Other axioms may be specific to the mathematical theory being studied, such as the Peano axioms for arithmetic or the Zermelo-Fraenkel axioms for set theory

Proof Techniques and Strategies

• Direct proof derives the conclusion from the premises using a sequence of inference rules and axioms
• Indirect proof (proof by contradiction) assumes the negation of the conclusion and derives a contradiction, thereby proving the original conclusion
  • Reductio ad absurdum (RAA): From ¬A → (B ∧ ¬B), infer A
• Proof by cases considers all possible cases and proves the conclusion holds in each case
• Existential proof demonstrates the existence of an object satisfying a given property without explicitly constructing it
• Universal proof shows that a property holds for all objects in a given domain
• Induction proves a property for all natural numbers by proving a base case and an inductive step
  • Base case: Prove the property holds for the first natural number (usually 0 or 1)
  • Inductive step: Assume the property holds for an arbitrary natural number k (inductive hypothesis) and prove it holds for k+1

Common Proof Structures

• Proof by induction: Base case, inductive hypothesis, inductive step
• Proof by contradiction: Assume the negation of the conclusion, derive a contradiction, conclude the original statement
• Proof by cases: Divide the problem into exhaustive and mutually exclusive cases, prove the conclusion for each case
• Existential proof: Prove the existence of an object satisfying a property, often using a constructive method or a non-constructive argument (e.g., the pigeonhole principle)
• Uniqueness proof: Prove the existence of an object satisfying a property and then prove that any two such objects are equal
• Proof by contrapositive: Prove the equivalent contrapositive statement (¬B → ¬A instead of A → B)
• Proof by biconditional: Prove both directions of an "if and only if" (↔) statement

Applications in Mathematics

• First-order logic is used to formalize and reason about various branches of mathematics, such as arithmetic, analysis, geometry, and set theory
• Peano arithmetic is a first-order theory that axiomatizes the natural numbers and their properties, enabling proofs of arithmetic statements
• Real analysis can be formalized in first-order logic, allowing rigorous proofs of theorems about limits, continuity, differentiation, and integration
• Geometry can be axiomatized using first-order logic, as in Hilbert's axiomatization of Euclidean geometry or Tarski's axiomatization of Euclidean and non-Euclidean geometries
• Set theory, such as Zermelo-Fraenkel set theory (ZF) or ZFC (ZF with the Axiom of Choice), is formalized in first-order logic, providing a foundation for mathematics

Limitations and Extensions

• Gödel's First Incompleteness Theorem shows that any consistent first-order theory containing arithmetic is incomplete, meaning there are true statements that cannot be proved within the theory
• Gödel's Second Incompleteness Theorem demonstrates that a consistent first-order theory containing arithmetic cannot prove its own consistency within the theory itself
• The Löwenheim-Skolem Theorem implies that first-order theories with infinite models have models of every infinite cardinality, leading to non-standard models of arithmetic and set theory
• Higher-order logic extends first-order logic by allowing quantification over predicates and functions, increasing expressive power but sacrificing some desirable properties like completeness
• Modal logic adds operators for necessity and possibility, enabling reasoning about modalities such as knowledge, belief, time, and obligation
• Other extensions include second-order logic, intuitionistic logic, and many-valued logics, each with its own strengths and limitations

Practice Problems and Examples

• Prove that the sum of two even numbers is always even
  • Formalize the statement using first-order logic and prove it using induction or direct proof
• Prove that there are infinitely many prime numbers
  • Use proof by contradiction and Euclid's classical argument
• Prove that the square root of 2 is irrational
  • Employ proof by contradiction and arithmetic properties
• Prove that in a group of 6 people, there are always 3 people who know each other or 3 people who do not know each other
  • Apply the pigeonhole principle and proof by cases
• Formalize and prove basic properties of set operations, such as commutativity, associativity, and distributivity
  • Use first-order logic and set theory axioms
• Prove the fundamental theorem of arithmetic (unique prime factorization) using first-order logic and Peano arithmetic
• Formalize and prove the Intermediate Value Theorem from real analysis using first-order logic and the axioms of the real number system