Predicate Logic

Introduction

Predicate logic expands propositional logic by incorporating variables, predicates, and quantifiers. It enables statements about objects and their properties. Central to discrete mathematics, it underpins formal reasoning in mathematics, computer science, and artificial intelligence. Predicate logic allows expression of complex assertions beyond simple true/false values.

"Mathematics is the art of giving the same name to different things." -- Henri Poincaré

Syntax of Predicate Logic

Alphabet

Basic symbols: variables (x, y, z), predicate symbols (P, Q, R), function symbols (f, g), logical connectives (¬, ∧, ∨, →, ↔), quantifiers (∀, ∃), equality (=), parentheses ().

Terms

Definition: variables and function applications. Formation rules: variable is term; if f is n-ary function symbol, and t₁,...,tₙ terms, then f(t₁,...,tₙ) is term.

Atomic Formulas

Predicate symbol applied to terms: if P is n-ary predicate and t₁,...,tₙ terms, then P(t₁,...,tₙ) is atomic formula. Equality t₁ = t₂ also atomic.

Well-Formed Formulas (WFF)

Inductively defined: atomic formulas are WFF; if φ, ψ WFF, then ¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) are WFF; if φ WFF and x variable, then ∀x φ and ∃x φ WFF.

Free and Bound Variables

Variables in scope of quantifier are bound; others are free. Formula is closed if it contains no free variables.

Semantics of Predicate Logic

Interpretations

Interpretation assigns domain D, maps function symbols to functions over D, predicate symbols to relations over D.

Variable Assignments

Assignment function maps variables to elements of D. Used to evaluate formulas with free variables.

Truth Evaluation

Atomic formula true if tuple of assigned elements in predicate relation. Complex formulas evaluated via logical connectives semantics.

Quantifier Semantics

∀x φ true if φ true for all assignments differing only in x; ∃x φ true if φ true for some such assignment.

Logical Consequence

Formula ψ is logical consequence of Γ if ψ true in every interpretation and assignment where all formulas in Γ true.

Quantifiers

Universal Quantifier (∀)

Meaning: "for all". Syntax: ∀x φ(x). Semantics: φ holds for every element in domain.

Existential Quantifier (∃)

Meaning: "there exists". Syntax: ∃x φ(x). Semantics: at least one element satisfies φ.

Bound and Free Variables

Quantifiers bind variables; variables outside quantifiers remain free. Scope of quantifier is formula following it.

Nested Quantifiers

Order matters: ∀x ∃y φ(x,y) differs from ∃y ∀x φ(x,y). Changing order changes meaning.

Quantifier Negation

Rules: ¬∀x φ ≡ ∃x ¬φ, ¬∃x φ ≡ ∀x ¬φ. Enables formula manipulation.

Formulas and Well-Formed Formulas

Atomic Formulas

Predicates applied to terms or equality statements. Base components of formulas.

Compound Formulas

Constructed using logical connectives on formulas: ¬, ∧, ∨, →, ↔.

Quantified Formulas

Contain quantifiers ∀, ∃ binding variables. Enable expression of generality and existence.

Free vs Bound Variables

Free variables not within scope of quantifiers; bound variables are quantified. Closed formulas have none free.

Formula Examples

∀x (P(x) → ∃y Q(x,y))∃z (R(z) ∧ ¬S(z))P(a) ∧ ∀y Q(y)

Proof Systems and Inference Rules

Hilbert Systems

Axiomatic basis with inference rules like Modus Ponens. Compact but less intuitive.

Natural Deduction

Rules mimic human reasoning: introduction and elimination for connectives and quantifiers.

Sequent Calculus

Formal system using sequents; facilitates proof transformations and cut-elimination.

Inference Rules for Quantifiers

Universal introduction/elimination, existential introduction/elimination. Careful variable conditions apply.

Soundness and Completeness

Soundness: all derivable formulas are logically valid. Completeness: all logically valid formulas are derivable.

Models and Interpretations

Domain of Discourse

Nonempty set over which variables range. Basis for semantic evaluation.

Interpretation Functions

Map function symbols to functions, predicate symbols to relations on domain.

Model Definition

A model satisfies a formula if formula evaluates to true under interpretation and assignment.

Countermodels

Interpretations where formula is false, used to demonstrate non-validity.

Logical Equivalence

Two formulas logically equivalent if satisfied by exactly same models.

Expressiveness and Limitations

Expressive Power

Can define properties and relations over objects. Expresses general statements, existence, uniqueness.

Comparison with Propositional Logic

More expressive: handles internal structure of propositions, not just truth values.

Limitations

Cannot express higher-order properties directly; restricted to first-order quantification.

Undecidability

Validity problem in predicate logic is undecidable. No algorithm can decide truth of all formulas.

Compactness and Löwenheim-Skolem

Compactness: if every finite subset satisfiable, whole set satisfiable. Löwenheim-Skolem: infinite models of various cardinalities exist.

Applications of Predicate Logic

Mathematical Foundations

Formalizes theories: arithmetic, set theory, algebra. Basis for rigorous proofs.

Computer Science

Specification languages, program verification, automated theorem proving.

Artificial Intelligence

Knowledge representation, reasoning engines, logic programming (Prolog).

Database Theory

Query languages (e.g., relational calculus), integrity constraints expressed in predicate logic.

Philosophy and Linguistics

Formal semantics of natural language, analysis of arguments and meaning.

Computability and Decidability

Decidability of Fragments

Some fragments decidable (monadic predicate logic), full first-order logic undecidable.

Gödel's Incompleteness Theorems

Limits of formal systems: some truths not provable within system.

Church-Turing Thesis

Expressiveness corresponds to computability limits; no mechanical procedure for all logical truths.

Automated Theorem Proving

Algorithms attempt proof search; often incomplete or resource-intensive.

Satisfiability Problems

First-order satisfiability is semi-decidable; algorithms may not terminate on all inputs.

Extensions and Variants

Higher-Order Logic

Quantification over predicates and functions; more expressive but less decidable.

Modal Predicate Logic

Introduces modal operators (necessity, possibility) alongside predicates.

Intuitionistic Predicate Logic

Constructivist approach; rejects law of excluded middle.

Description Logics

Subset designed for knowledge representation; balances expressiveness and decidability.

Many-Sorted Logics

Variables sorted by type; simplifies complex domains.

Examples and Exercises

Example 1: Simple Formula

∀x (Human(x) → Mortal(x)) expresses "All humans are mortal."

Example 2: Existence Statement

∃x (Prime(x) ∧ Even(x)) states "There exists a prime number that is even."

Exercise 1

Translate "Every student likes some course" into predicate logic.

Exercise 2

Prove validity of ∀x (P(x) → Q(x)) → (∃x P(x) → ∃x Q(x)) using natural deduction.

Exercise 3

Given:Domain = {1,2,3}Interpretation:P = {1,3}Q = {2,3}Evaluate truth of ∃x (P(x) ∧ Q(x))?

References

• Enderton, H. B., A Mathematical Introduction to Logic, Academic Press, Vol. 2, 2001, pp. 150-300.
• Chang, C. C., Keisler, H. J., Model Theory, North-Holland, Vol. 73, 1990, pp. 45-120.
• Endriss, U., Logic in Computer Science, Cambridge University Press, 2011, pp. 100-180.
• Smullyan, R. M., First-Order Logic, Dover Publications, 1995, pp. 210-290.
• Marker, D., Model Theory: An Introduction, Springer, Vol. 217, 2002, pp. 70-145.