Hilbert Proof Systems and Herbrand Logic: Foundations of Automated Theorem Proving

12 min read
logic computer-science

An in-depth exploration of Hilbert proof systems and the Tableaux method for predicate logic, with detailed examples on quantifier manipulation and step-by-step proof construction.

Hilbert Proof Systems and Herbrand Logic: Foundations of Automated Theorem Proving

The Hilbert proof system represents one of the most elegant and rigorous approaches to formal logic. By reducing complex logical reasoning to a minimal set of axioms and a single rule of inference, it provides a foundational bedrock for mathematical logic.

In this lecture, we explore the structure of Hilbert systems, examine critical examples of quantifier manipulation, and apply the Tableaux method—a powerful algorithmic technique used in modern automated theorem provers—to construct formal proofs.

The Hilbert Proof System

The defining characteristic of a Hilbert system is its minimalism. Unlike systems with many inference rules (like Natural Deduction), a Hilbert system typically uses implication as the primary connective and relies on a small set of logical axioms combined with Modus Ponens as the sole rule of derivation.

The Five Axioms of First-Order Logic

Our system consists of five schema axioms. Let $A$, $B$, and $C$ be arbitrary well-formed formulas:

Axiom 1: Basic Implication Identity A→(B→A)A \to (B \to A)

Intuition: This axiom asserts that if a proposition $A$ is true, it remains true even if we assume some other condition $B$. This reflects the monotonicity of classical logic—adding premises cannot invalidate a true conclusion.

Axiom 2: Implication Distribution [A→(B→C)]→[(A→B)→(A→C)][A \to (B \to C)] \to [(A \to B) \to (A \to C)]

Intuition: This is the logical analog of function distribution. If $A$ implies that “$B$ implies $C$”, and $A$ also implies $B$, then $A$ must imply $C$. It allows us to distribute an assumption $A$ across an implication $B \to C$.

Axiom 3: The Contrapositive Principle (¬B→¬A)→(A→B)(\neg B \to \neg A) \to (A \to B)

Intuition: This captures the essence of proof by contrapositive. If the falsity of $B$ guarantees the falsity of $A$, then the truth of $A$ guarantees the truth of $B$.

Axiom 4: Universal Instantiation ∀xA(x)→A(t)\forall x A(x) \to A(t)

Condition: $t$ is any term free for $x$ in $A(x)$. Intuition: If a property holds for everything, it must hold for any specific thing $t$. This allows us to move from general laws to specific instances.

Axiom 5: Universal Distribution ∀x(A→B(x))→(A→∀xB(x))\forall x(A \to B(x)) \to (A \to \forall x B(x))

Condition: The variable $x$ must not occur free in $A$. Intuition: If $A$ implies $B(x)$ for every possible $x$, and $A$ itself does not depend on $x$, then $A$ implies that $B(x)$ is universally true.

Modus Ponens: The Single Rule of Inference

The engine of the Hilbert system is Modus Ponens (MP):

A,A→BB\frac{A, \quad A \to B}{B}

Meaning: If we have proven $A$, and we have proven that $A$ implies $B$, we can logically conclude $B$.

This single rule, combined with the five axioms above, forms a sound and complete proof system for first-order logic. Every valid mathematical theorem can, in principle, be derived from this compact foundation.

Quantifier Manipulation: Subtleties and Pitfalls

One of the most common sources of error in logic is the improper manipulation of quantifiers. The order of quantifiers ($\forall \exists$ vs $\exists \forall$) fundamentally changes the meaning of a statement.

Case Study 1: The Invalid Commutation

Claim: Is the following implication valid? ∃x∀yA(x,y)→∀x∃yA(x,y)\exists x \forall y A(x,y) \to \forall x \exists y A(x,y)

Analysis: Let’s attempt a proof to see where it breaks down.

  1. Assume $\exists x \forall y A(x,y)$.
  2. By Existential Elimination, we introduce a specific constant (a witness), say $a$, such that $\forall y A(a,y)$.
  3. By Universal Instantiation, we can pick any arbitrary term $b$ and say $A(a,b)$.
  4. By Existential Introduction, we can say $\exists y A(a,y)$.

The Block: We are stuck. We have shown that for the specific constant $a$, there exists a $y$. However, the consequent $\forall x \exists y A(x,y)$ requires this to hold for every $x$, not just our witness $a$. Since $a$ is a specific constant fixed by the premise, we cannot generalize it to $\forall x$.

Counterexample: Let $A(x,y)$ be the relation “$x = y$”.

  • $\exists x \forall y (x=y)$ means “There is a number equal to every number.” (False)
  • $\forall x \exists y (x=y)$ means “Every number is equal to some number” (e.g., itself). (True) The implication False $\to$ True is technically valid truth-functionally, but the logical derivation fails because the structure doesn’t hold for all interpretations.

Case Study 2: Swapping Quantifiers

Claim: Is the following valid? ∃x∀yA(x,y)→∀y∃xA(y,x)\exists x \forall y A(x,y) \to \forall y \exists x A(y,x)

Analysis:

  1. Assume $\exists x \forall y A(x,y)$.
  2. Eliminate $\exists x$: We get $\forall y A(a,y)$ for some witness $a$.
  3. Eliminate $\forall y$: We get $A(a,b)$ for any arbitrary $b$.

The Block: We need to prove $\forall y \exists x A(y,x)$. This would require deriving $A(b, \text{something})$. We have $A(a,b)$. Unless the relation $A$ is symmetric (i.e., $A(x,y) \to A(y,x)$), we cannot derive $A(b,a)$ from $A(a,b)$.

Counterexample: Let $A(x,y)$ be “$x > y$”.

  • Premise: “There is a number larger than all numbers.” (False)
  • Conclusion: “For every number, there is a number smaller than it.” (True) Again, the logical form does not support the derivation. $A(a,b)$ does not imply $A(b,a)$.

The Tableaux Method for Predicate Logic

While Hilbert systems are elegant, they are difficult to use for finding proofs manually. The Tableaux Method (or Truth Tree method) is a refutation-based procedure ideal for automated reasoning.

Algorithm: To prove a formula $F$, we assume $\neg F$ and try to show this leads to a contradiction in all branches of the logic tree.

Problem 1: Proving Satisfiability

Formula: $\exists y [\neg R(y,y) \lor P(y,y)] \land \forall x R(x,x)$

We construct the tree by decomposing the formula:

  1. Root: $\exists y [\neg R(y,y) \lor P(y,y)] \land \forall x R(x,x)$
  2. Decompose AND:
    • (1) $\exists y [\neg R(y,y) \lor P(y,y)]$
    • (2) $\forall x R(x,x)$
  3. Eliminate $\exists y$ (from 1): Introduce witness constant $a$.
    • (3) $\neg R(a,a) \lor P(a,a)$
  4. Branch on OR (from 3):
    • Left Branch: $\neg R(a,a)$
      • Apply (2) $\forall x R(x,x)$ to $a$: $R(a,a)$.
      • Contradiction! ($R(a,a)$ and $\neg R(a,a)$). Branch Closed.
    • Right Branch: $P(a,a)$
      • Apply (2) to $a$: $R(a,a)$.
      • No contradiction. We have $P(a,a)$ true and $R(a,a)$ true.

Result: The tree has an open branch. Therefore, the formula is satisfiable (true in at least one model) but not a tautology (not true in all models).

Problem 2: Proving Validity

Formula: $\forall x[P(x) \to Q(x)] \to (\forall x P(x) \to \forall x Q(x))$

Proof: Assume the negation is true.

  1. False: $\forall x[P(x) \to Q(x)] \to (\forall x P(x) \to \forall x Q(x))$
  2. True: $\forall x[P(x) \to Q(x)]$ (Antecedent)
  3. False: $\forall x P(x) \to \forall x Q(x)$ (Consequent)
  4. True: $\forall x P(x)$ (from 3)
  5. False: $\forall x Q(x)$ (from 3)
  6. True: $\exists x \neg Q(x)$ (Negation of 5)
  7. Witness: $\neg Q(a)$ (from 6, constant $a$)
  8. Instantiate (2) with $a$: $P(a) \to Q(a)$
  9. Instantiate (4) with $a$: $P(a)$
  10. Modus Ponens (on 8, 9): Therefore $Q(a)$
  11. Contradiction: We have derived $Q(a)$ (step 10) and we have $\neg Q(a)$ (step 7).

Result: All branches close. The negation is impossible. Therefore, the original formula is valid.

Conclusion

The Hilbert proof system demonstrates the power of minimal axiomatization: with just five axioms and Modus Ponens, we can derive all valid formulas of first-order logic. However, the examples of quantifier manipulation reveal critical subtleties:

  1. Quantifier order matters: $\exists x \forall y$ is fundamentally different from $\forall x \exists y$.
  2. Independent constants cannot be freely manipulated: Constants from different quantifiers represent potentially distinct values.
  3. Skolemization is sound but introduces constraints: Skolem constants are witnesses, not arbitrary values.

The Tableaux method complements the Hilbert system by providing a semi-decidable proof procedure: if a formula is valid, the Tableaux method will eventually close all branches and confirm validity. If invalid, the method may not terminate, but often reveals counterexamples through open branches.

Together, these techniques form the foundation of automated theorem proving and are essential tools in formal verification, program correctness, and artificial intelligence reasoning systems.

Exercises

To solidify your understanding of Hilbert systems and quantifier manipulation, work through these exercises:

  1. Hilbert Derivation: Using Axiom 1 and Axiom 2, show that $A \rightarrow A$ is a theorem in the Hilbert system.
  2. Quantifier Analysis: Explain why $\forall x \exists y A(x,y)$ does not logically imply $\exists y \forall x A(x,y)$. Provide a counterexample.
  3. Tableaux Proof: Use the Tableaux method to prove that $\forall x P(x) \rightarrow \exists x P(x)$ is valid (assuming a non-empty domain).

Exercise Solutions

Exercise 1: Proving $A \rightarrow A$

  1. $[A \rightarrow ((A \rightarrow A) \rightarrow A)] \rightarrow [(A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)]$ (Axiom 2 with $B = (A \rightarrow A), C = A$)
  2. $A \rightarrow ((A \rightarrow A) \rightarrow A)$ (Axiom 1 with $B = (A \rightarrow A)$)
  3. $(A \rightarrow (A \rightarrow A)) \rightarrow (A \rightarrow A)$ (Modus Ponens on 1 and 2)
  4. $A \rightarrow (A \rightarrow A)$ (Axiom 1 with $B = A$)
  5. $A \rightarrow A$ (Modus Ponens on 3 and 4)

Exercise 2: Quantifier Order

The implication $\forall x \exists y A(x,y) \rightarrow \exists y \forall x A(x,y)$ is invalid because the choice of $y$ can depend on $x$ in the antecedent, but must be the same for all $x$ in the consequent.

  • Counterexample: Let $A(x,y)$ be “$y$ is the mother of $x$”.
  • $\forall x \exists y A(x,y)$ means “Every person has a mother” (True).
  • $\exists y \forall x A(x,y)$ means “There is one person who is the mother of everyone” (False).

Exercise 3: Tableaux Proof

  1. False: $\forall x P(x) \rightarrow \exists x P(x)$ (Assume negation)
  2. True: $\forall x P(x)$ (Antecedent)
  3. False: $\exists x P(x)$ (Consequent)
  4. True: $\neg \exists x P(x)$ (from 3)
  5. True: $\forall x \neg P(x)$ (from 4)
  6. Instantiate (2) with $a$: $P(a)$
  7. Instantiate (5) with $a$: $\neg P(a)$
  8. Contradiction: $P(a)$ and $\neg P(a)$. Branch closed. Original formula is valid.

Further Reading

  • Introduction to Mathematical Logic by Mendelson - Comprehensive coverage of Hilbert systems.
  • Logic for Applications by Anil Nerode and Richard Shore - Practical applications of formal logic.
  • Automated Reasoning by Gallier - Tableaux methods and resolution theorem proving.
  • The Isabelle Theorem Prover - Modern automated proof assistant.

This lecture covered Hilbert proof systems, quantifier manipulation, and the Tableaux method. Next, we will explore Herbrand semantics and how they provide efficient models for first-order logic.

Related Posts