Proof Techniques in Predicate Logic

Having established both syntax and semantics, we now delve into the essential methods used to formally prove statements in predicate logic. Specifically, we’ll explore Natural Deduction and Hilbert-style systems, illustrating their application to real mathematical reasoning.

Natural Deduction in Predicate Logic

Natural deduction is a formal proof system that extends naturally from propositional logic, incorporating quantifiers. The fundamental idea is to use inference rules to construct proofs directly, step by step.

Extension of Propositional Logic Rules

Predicate logic inherits all propositional inference rules (such as conjunction, implication, negation) and adds rules for quantifiers.

Introduction and Elimination Rules for Quantifiers

Two new pairs of rules are introduced to handle quantifiers:

• Universal Quantifier (\(\forall\)):
  • Introduction (\(\forall I\)): If you can derive \(\varphi(x)\) for an arbitrary element \(x\), you may conclude \(\forall x \varphi(x)\).
  • Elimination (\(\forall E\)): From \(\forall x \varphi(x)\), you may infer \(\varphi(a)\) for any specific element aa.
• Existential Quantifier (\(\exists\)):
  • Introduction (\(\exists I\)): From \(\varphi(a)\) for a particular element \(a\), conclude \(\exists x \varphi(x)\).
  • Elimination (\(\exists E\)): If \(\exists x \varphi(x)\) holds, and from the assumption \(\varphi(a)\) (for an arbitrary \(a\)), you derive a conclusion \(\psi\) independent of \(a\), then you can conclude \(\psi\).

Examples of Formal Proofs (Natural Deduction)

Example: Prove the statement “If everyone loves pizza, then someone loves pizza.”

Formally: \(\forall x \text{LovesPizza}(x) \rightarrow \exists y \text{LovesPizza}(y)\)

Proof Sketch:

1. Assume \(\forall x \text{LovesPizza}(x)\).
2. From this assumption, choose any specific individual, say \(a\), then we have \(\text{LovesPizza}(a)\) by \(\forall E\).
3. Now apply existential introduction (\(\exists I\)): From \(\{\text{LovesPizza}(a)\}\), conclude \(\exists y \text{LovesPizza}(y)\).

This example illustrates the intuitive connection between universal and existential quantification.

Hilbert-Style Proof Systems

Hilbert-style proof systems build from axioms and inference rules, similar to propositional logic but augmented for quantification.

Typical Axioms involving Quantifiers

Hilbert-style systems typically add axioms to propositional logic to handle quantifiers, such as:

• Universal Instantiation: \(\forall x \varphi(x) \rightarrow \varphi(a)\), where \(a\) is any term.
• Existential Generalization: \(\varphi(a) \rightarrow \exists x \varphi(x)\).

These axioms enable formal manipulation of quantified statements without explicitly referring to inference rules.

Examples and Subtleties Introduced by Quantification

Quantifiers add subtleties not present in propositional logic:

• Order of quantifiers matters significantly: \(\forall x \exists y P(x,y)\) differs importantly from \(\exists y \forall x P(x,y)\).
• Careful treatment of variables (bound vs. free) is crucial to avoid ambiguities.

Real Mathematical Example

Statement: “For every integer \(x\), there exists an integer \(y\) such that \(y = x + 1\).”

Formally: \(\forall x \in \mathbb{Z}, \exists y (y = x + 1)\)

Proof (Natural Deduction Sketch):

• Consider an arbitrary integer \(x\).
• Let \(y = x + 1\). Clearly, \(y\) is an integer.
• Thus, \(\exists y(y = x + 1)\).
• Since \(x\) was arbitrary, we conclude \(\forall x \exists y(y = x + 1)\).

Complexities and Subtleties Introduced by Quantification

Quantification introduces significant complexity, especially regarding variable scope and substitutions. Consider the formula: \(\forall x \exists y (x < y)\)

It is intuitively clear that “for every integer, there is always a larger one.” Yet, rearranging quantifiers drastically changes the meaning: \(\exists y \forall x (y > x)\)

Now, the statement claims a single largest integer, which is false in standard integer arithmetic.

Exercises

1. Using natural deduction, prove formally:

\(\forall x (Even(x) \rightarrow \exists y (y = x + 2 \wedge Even(y)))\)

2. Demonstrate why the following statement is not logically valid:

\(\exists x \forall y (x > y)\)

Provide a counterexample to illustrate your reasoning clearly.

3. Translate and formally prove the following informal statement using natural deduction:

• “If some integer is even, then not all integers are odd.”

Summary

Proof techniques in predicate logic enable precise mathematical reasoning through formalized methods. While natural deduction closely mirrors intuitive mathematical reasoning, Hilbert-style systems rely on powerful axioms and simple inference rules to build proofs systematically. Understanding quantification’s subtleties is critical for rigorous mathematical reasoning.

Mastering these proof methods provides the essential skillset required to handle advanced mathematical and logical concepts effectively.