Predicate logic, also called first-order predicate calculus, is a formal system that extends propositional logic with quantifiers and predicates over individual variables, allowing statements about the properties of and relations between objects in a domain of discourse. It introduces the universal and existential quantifiers, enabling expressions such as ‘for all x, P(x)’ and ‘there exists an x such that P(x)‘. Predicate logic provides the semantic and syntactic backbone for much of automated reasoning, formal specification, and knowledge representation.
Overview
- Predicate logic separates a sentence into a predicate (a property or relation) applied to one or more terms (constants, variables, or function applications).
- Variables are bound by quantifiers: the universal quantifier asserts a property holds of every individual, the existential quantifier asserts it holds of at least one.
- Its model-theoretic semantics interpret formulae over a domain with an assignment of meanings to predicate, function, and constant symbols, giving a rigorous notion of truth.
- Soundness and completeness results (Goedel’s completeness theorem) guarantee that valid arguments are exactly those derivable in standard proof calculi.
Key aspects
- Quantifiers — universal and existential binding of variables across a domain of discourse.
- Predicates and functions — relations and mappings over individuals, distinguishing it from purely sentential logic.
- Well-formed formulae — a recursive syntax built from atomic predicates, connectives, and quantifiers.
- Inference rules — universal instantiation, existential generalisation, modus ponens and resolution.
- Decidability — first-order validity is semi-decidable, motivating practical proof-search strategies.
Applications
- Automated theorem proving and proof assistants for mathematics and verification.
- Formal specification of software and hardware behaviour and their verification.
- Description-logic fragments powering ontologies and the semantic web.
- Query languages and rule engines in knowledge-based and expert systems.