Introduction
First-order theorem proving is the art and science of using computers to automatically prove mathematical theorems and verify logical statements. It combines logic, algorithms, and search strategies to derive conclusions from axioms and inference rules.
This guide introduces the foundational concepts you need to understand to work with first-order theorem proving.
What is First-Order Logic?
First-order logic (FOL) is a formal system that extends propositional logic with two key features:
┌─────────────────────────────────────────────────────────────┐
│ Key Extensions in First-Order Logic │
├─────────────────────────────────────────────────────────────┤
│ 1. Quantifiers: ∀ (for all), ∃ (exists) │
│ 2. Predicates: Statements about objects │
│ 3. Variables: Refer to objects in the domain │
│ 4. Functions: Map objects to objects │
└─────────────────────────────────────────────────────────────┘
Simple Examples
-- Propositional: It is raining
is_raining
-- First-order: Socrates is human
Human(Socrates)
-- First-order: All humans are mortal
∀x (Human(x) → Mortal(x))
-- First-order: Some bird can fly
∃x (Bird(x) ∧ CanFly(x))
The Language of First-Order Logic
Building Blocks
% Constants (specific objects)
Socrates, Alice, 5, PlanetEarth
% Variables (placeholder for any object)
x, y, z, person, number
% Function symbols (map inputs to outputs)
Father(x) -- unary function
Plus(x, y) -- binary function
FatherOf(x, y) -- could be predicate or function
% Predicate symbols (true/false statements)
Human(x)
Loves(x, y)
GreaterThan(x, y)
Formulas
-- Atomic formulas (predicates applied to terms)
Human(Socrates)
Loves(Alice, Bob)
GreaterThan(5, 3)
-- Compound formulas (using connectives)
Human(x) ∧ Mortal(x) -- conjunction
¬Human(x) -- negation
Human(x) → CanDie(x) -- implication
∀x (Human(x) → Mortal(x)) -- universal quantifier
∃x (Bird(x) ∧ CanFly(x)) -- existential quantifier
Key Concepts in Theorem Proving
1. Axioms
Axioms are statements accepted as true without proof. They form the foundation of a theory:
% Axioms of equality
∀x (x = x) -- reflexivity
∀x ∀y (x = y → y = x) -- symmetry
∀x ∀y ∀z ((x = y ∧ y = z) → x = z) -- transitivity
% Axioms of arithmetic
∀x (x + 0 = x)
∀x ∀y (x + S(y) = S(x + y))
% Domain-specific axioms
∀x (Human(x) → Mortal(x))
∀x (Parent(x) → Human(x))
2. Theorems
A theorem is a statement that can be proven from axioms using inference rules:
-- If these are axioms:
∀x (Human(x) → Mortal(x))
Human(Socrates)
-- Then this is a theorem:
Mortal(Socrates)
3. Inference Rules
Inference rules define how to derive new truths from existing ones:
% Modus Ponens (most fundamental)
P → Q P
──────────────
Q
% Modus Tollens
P → Q ¬Q
──────────────
¬P
% Universal Instantiation
∀x P(x)
──────────────
P(c) -- for any constant c
% Existential Generalization
P(c)
──────────────
∃x P(x)
The Proof Process
What is a Proof?
A proof is a sequence of formulas where each formula is either:
- An axiom, or
- Derived from previous formulas using inference rules
% Example proof that Socrates is mortal
1. ∀x (Human(x) → Mortal(x)) -- Axiom
2. Human(Socrates) -- Given
3. Human(Socrates) → Mortal(Socrates) -- Universal Instantiation (1)
4. Mortal(Socrates) -- Modus Ponens (2, 3)
QED
Types of Proofs
┌─────────────────────────────────────────────────────────────┐
│ Proof Techniques │
├─────────────────────────────────────────────────────────────┤
│ • Direct Proof: Start from premises, reach conclusion │
│ • Proof by Contradiction: Assume negation, derive conflict │
│ • Proof by Induction: Base case + inductive step │
│ • Proof by Cases: Cover all possible scenarios │
└─────────────────────────────────────────────────────────────┘
Semantics: What Do Formulas Mean?
Interpretations
An interpretation assigns meaning to the symbols:
% Consider: ∀x (Human(x) → Mortal(x))
-- Interpretation 1 (standard):
Domain = all humans
Human(x) = "x is a human"
Mortal(x) = "x is mortal"
-- Formula is TRUE
-- Interpretation 2 (alternative):
Domain = all creatures
Human(x) = "x is a robot"
Mortal(x) = "x runs on electricity"
-- Formula may be TRUE or FALSE depending on interpretation
Models
A model is an interpretation that makes all axioms true:
% If axioms are:
-- All humans are mortal
-- Socrates is human
% Then interpretation with:
-- Socrates is human
-- No immortal humans
-- Is a MODEL (makes all axioms true)
Validity and Satisfiability
┌─────────────────────────────────────────────────────────────┐
│ Key Semantic Concepts │
├─────────────────────────────────────────────────────────────┤
│ Valid (Tautology): True in EVERY interpretation │
│ ⊨ P → P │
├─────────────────────────────────────────────────────────────┤
│ Satisfiable: True in SOME interpretation │
│ ∃x P(x) is satisfiable │
├─────────────────────────────────────────────────────────────┤
│ Unsatisfiable: False in EVERY interpretation │
│ P ∧ ¬P is unsatisfiable │
├─────────────────────────────────────────────────────────────┤
│ Falsifiable: False in SOME interpretation │
│ ∃x ¬P(x) is falsifiable │
└─────────────────────────────────────────────────────────────┘
Soundness and Completeness
Soundness
A proof system is sound if everything it proves is actually true:
Soundness: If ⊢ φ (provable), then ⊨ φ (valid)
-- If the prover says "P is proved"
-- Then P must be true in all models
Completeness
A proof system is complete if everything that’s true can be proved:
Completeness: If ⊨ φ (valid), then ⊢ φ (provable)
-- If P is true in all models
-- Then there exists a proof of P
Gödel’s Incompleteness
┌─────────────────────────────────────────────────────────────┐
│ Important Limitation │
├─────────────────────────────────────────────────────────────┤
│ Gödel's First Incompleteness Theorem: │
│ │
│ Any sufficiently expressive theory cannot be both │
│ complete and consistent. │
│ │
│ This means: There will always be true statements │
│ that cannot be proved within the theory. │
└─────────────────────────────────────────────────────────────┘
Basic Proof Strategies
1. Forward Chaining
Start from known facts, apply rules, work toward goal:
% Known:
% 1. All mammals are warm-blooded
% 2. All warm-blooded animals have hearts
% 3. whales are mammals
% Forward chain:
% From 1 and 3: Whales are warm-blooded
% From 2 and above: Whales have hearts
2. Backward Chaining
Start from goal, work backward to find supporting facts:
% Goal: Prove "Socrates is mortal"
% Step 1: To prove Mortal(x), need Human(x)
% Step 2: To prove Human(Socrates), check axioms
% Step 3: Found: Human(Socrates) in axioms
% Step 4: Use ∀x (Human(x) → Mortal(x)) to complete proof
3. Resolution
Convert to clauses, resolve contradictions:
-- To prove P:
-- 1. Assume ¬P
-- 2. Add axioms
-- 3. Derive contradiction (empty clause)
-- 4. Therefore P is proved
Common Techniques
Universal Instantiation
% From ∀x P(x), conclude P(c) for any constant c
∀x (Human(x) → Mortal(x))
───────────────────────────────
Human(Socrates) → Mortal(Socrates)
Existential Instantiation
-- From ∃x P(x), introduce a NEW constant (Skolem constant)
-- The constant must be fresh (not used elsewhere)
∃x (King(x) ∧ Just(x))
───────────────────────────────
King(a) ∧ Just(a) -- a is a NEW constant symbol
Chaining Quantifiers
-- Order matters!
∀x ∃y (Loves(x, y))
-- For everyone, there is someone they love
-- (possibly different for each person)
∃y ∀x (Loves(x, y))
-- There is someone who loves everyone
-- (the same person loves everyone)
Why Theorem Proving Matters
Applications
┌─────────────────────────────────────────────────────────────┐
│ Where Theorem Proving is Used │
├─────────────────────────────────────────────────────────────┤
│ • Software Verification: Proving program correctness │
│ • Hardware Design: Verifying circuit properties │
│ • Formal Methods: Safety-critical systems │
│ • Knowledge Representation: Automated reasoning │
│ • Mathematics: Proving new theorems │
│ • AI: Logic-based learning and inference │
└─────────────────────────────────────────────────────────────┘
Example: Program Verification
% Prove: This swap function is correct
% Specification:
% ∀a ∀b { swap(a,b) returns (b,a) }
% Implementation:
swap(x, y):
temp = x
x = y
y = temp
return (x, y)
% Proof shows implementation meets specification
Summary
First-order theorem proving rests on several foundational concepts:
- First-order logic uses quantifiers and predicates to express statements about objects
- Axioms are accepted truths; theorems are derived truths
- Inference rules like modus ponens enable mechanical reasoning
- Soundness ensures proofs are valid; completeness ensures all truths are provable
- Proof strategies like forward/backward chaining guide the search for proofs
Understanding these basics prepares you for more advanced topics in automated reasoning and formal verification.
Related Articles
- Introduction to Predicate Logic
- Resolution and Refutation
- Unification and Pattern Matching
- Natural Deduction Systems
- First-Order Logic Calculus of Computation
Comments