1 Basic concepts
Predicate logic, more commonly called first-order logic, is a formal language for talking about objects and the properties they have. It also describes relations among objects, such as “is larger than,” “is the parent of,” or “lies between.” In contrast to propositional logic, which treats whole statements as indivisible units, predicate logic breaks statements into components that can be analyzed and recombined with precision.
Its basic expressive power comes from a small set of ideas: terms that name or describe objects, predicates that express properties and relations, and logical connectives that combine statements. By adding variables and quantifiers, the system can make general claims such as “every object with property P has property Q” or “there exists an object with a given feature.”
1.1 Propositions and predicates
A proposition is a statement that is either true or false. In predicate logic, a proposition may be built from simpler expressions rather than treated as a single symbol. A predicate is an expression that becomes a proposition when applied to the appropriate terms. For example, “is even” can be viewed as a one-place predicate, while “is taller than” can be viewed as a two-place predicate.
Predicates allow logic to represent internal structure. Instead of writing only that a sentence is true or false, the language can specify what object is being discussed and what property or relation is asserted about it.
1.2 Terms and variables
Terms are expressions that refer to objects in the domain being discussed. They may be names, variables, or expressions built from functions. Variables serve as placeholders for objects and are used to state general patterns without naming each object individually.
A term does not itself claim anything; it simply denotes an object or stands for one. A formula becomes meaningful as a claim once terms are combined with predicates and logical operators.
1.3 Constants and functions
Constants are symbols used to refer to particular objects. In a mathematical setting, a constant may denote a specific number, element, or distinguished entity. Function symbols construct new terms from existing ones. For instance, if a function symbol represents “successor,” then applying it to a term yields another term.
Functions make the language richer by allowing the naming of objects indirectly through operations. This is especially useful in mathematics, where many objects are defined by how they are generated from others.
1.4 Relations and predicates
Relations connect objects in a domain. A relation may involve one object, several objects, or many objects at once. Predicates are the symbols used to express such relations. A predicate with one argument expresses a property, while a predicate with two or more arguments expresses a relation among the objects.
This distinction helps formalize everyday and mathematical language. For example, being prime is a property of a number, while being adjacent to is a relation between two objects.
1.5 Logical connectives
Logical connectives combine simpler formulas into more complex ones. The standard connectives include negation, conjunction, disjunction, implication, and biconditionality. They are used in predicate logic in much the same way as in propositional logic, but now they operate on formulas that may contain variables and quantifiers.
These connectives determine how the truth of a larger statement depends on the truth of its parts. They are essential for building structured arguments and for expressing compound conditions.
2 Syntax of predicate logic
The syntax of predicate logic specifies how symbols may be arranged to form legitimate expressions. It defines the grammar of the language, including which strings count as terms and which count as formulas. This formal discipline ensures that expressions can be interpreted consistently and manipulated by proof rules.
Syntax is separate from meaning. A formula may be well formed even if it has no immediate interpretation, while an ill-formed string has no standing within the system at all.
2.1 Well-formed formulas
Well-formed formulas are the valid statements of the language. They are built according to precise formation rules from predicates, terms, connectives, and quantifiers. A formula may be atomic, such as a predicate applied to terms, or compound, such as a negation or a quantified statement.
The notion of well-formedness prevents ambiguity. It guarantees that every expression can be parsed in a determinate way.
2.2 Formation rules
Formation rules specify how complex formulas are constructed from simpler ones. They state, for example, that if an expression is a formula, then its negation is also a formula, and that if two expressions are formulas, then their conjunction or implication is also a formula. Similar rules govern the formation of terms from variables, constants, and function symbols.
These rules define the recursive structure of the language. Because they are finite and exact, they make formal reasoning possible.
2.3 Free and bound variables
A variable is free in a formula if it is not governed by a quantifier within that formula. It is bound if it falls within the scope of a quantifier that applies to it. This distinction matters because free variables often function like placeholders, while bound variables are locally controlled by quantification.
For example, in a formula saying that every object with a property has another property, the quantified variables are bound, whereas an unquantified variable may remain free. A sentence with no free variables is typically treated as a complete statement.
2.4 Substitution
Substitution is the process of replacing a variable with a term. It is central to formal derivations and semantic evaluation. Care must be taken to avoid capturing variables accidentally, which can happen if a substituted term contains a variable already bound in the target formula.
Proper substitution preserves the intended meaning of a formula. It is used extensively in proof systems, especially when instantiating universally quantified statements or constructing examples from existential ones.
3 Quantifiers
Quantifiers extend predicate logic beyond individual statements by allowing claims about all objects or at least one object in a domain. They are among the defining features of first-order logic and give the system its power to express generality and existence.
The two fundamental quantifiers are universal and existential quantification. Together they make it possible to state broad mathematical laws, definitions, and relational conditions.
3.1 Universal quantifier
The universal quantifier expresses that a formula holds for every object in the domain. It is commonly read as “for all.” A universally quantified statement can represent a general rule, such as a property shared by all members of a class.
Universal quantification is often used in definitions and theorems because it captures patterns that are meant to apply without exception within the chosen domain.
3.2 Existential quantifier
The existential quantifier asserts that there is at least one object for which a formula holds. It is commonly read as “there exists.” This type of statement is used to express the presence of an example, witness, or solution.
Existential claims are weaker than universal ones, but they are equally important. Many mathematical and logical arguments depend on proving that an object with certain characteristics exists.
3.3 Scope of quantifiers
The scope of a quantifier is the part of the formula over which it has effect. The meaning of a statement may change when the scope is altered, especially when multiple quantifiers appear in the same formula. Careful attention to scope is essential for correct interpretation.
Scope also helps distinguish nested structures from independent ones. The placement of parentheses and quantifiers determines which variables are controlled by which quantifiers.
3.4 Nested quantification
Nested quantification occurs when one quantifier appears inside the scope of another. Such formulas can express more subtle claims, including ordered dependencies among objects. For example, a statement may say that for every object there exists another object related to it in a specific way.
The order of nested quantifiers often matters. Swapping universal and existential quantifiers can produce a very different meaning, and in many cases the difference is substantial.
4 Semantics and interpretation
Semantics explains what predicate logic formulas mean. It provides a bridge between syntax and the objects, relations, and structures to which formulas refer. Without semantics, the language would be only a formal calculus of symbols.
Interpretation assigns meaning to the nonlogical symbols of the language and evaluates formulas as true or false relative to a chosen structure. This makes the system applicable to mathematics and other formal domains.
4.1 Structures and domains
A structure consists of a domain of objects together with an assignment of meaning to the symbols of the language. The domain is the collection of entities under discussion, which may be numbers, sets, persons, or any other well-defined class. The structure determines what counts as an object in the interpretation.
Different structures can make the same formula true or false. This flexibility is one reason predicate logic is so widely used.
4.2 Interpretation of symbols
An interpretation assigns referents to constants, functions to function symbols, and relations to predicates. Logical symbols such as connectives and quantifiers keep their standard meanings. The interpretation determines how a formula is to be read within the domain.
Because symbols are interpreted relative to a structure, the same formal expression can describe different situations in different contexts. This feature makes the language abstract yet adaptable.
4.3 Truth conditions
Truth conditions specify when a formula is true under a given interpretation and variable assignment. Atomic formulas are true when the corresponding relation holds of the interpreted terms. Compound formulas are evaluated according to the meanings of the connectives and quantifiers.
Truth in predicate logic is therefore recursive and systematic. Each larger formula depends on the truth of its parts and on how variables are assigned.
4.4 Models and satisfaction
A model is a structure in which a set of formulas is true. Satisfaction is the relation between a structure and a formula or collection of formulas when the interpretation makes them true. These notions are central in model theory, where one studies the relationship between formal languages and mathematical structures.
Model-theoretic ideas help explain consistency, consequence, and equivalence. They are also useful for understanding what it means for a theory to describe a class of structures.
5 Equality
Equality is often included in predicate logic as a special logical symbol. It allows one to state that two terms refer to the same object. This makes the language more expressive and helps formalize identity-based reasoning.
When equality is present, it is typically governed by special axioms or rules that ensure it behaves like genuine identity.
5.1 Identity relation
The identity relation states that two terms denote the same object. It is usually written with a dedicated equality sign. Unlike ordinary predicates, equality has a fixed logical role rather than being interpreted as an arbitrary relation.
Identity is fundamental in mathematics, where one often needs to distinguish between objects that are equal and objects that merely resemble one another.
5.2 Substitutivity of equals
Substitutivity means that if two terms are equal, one may be replaced by the other in any context without changing truth. This principle captures an essential property of identity: equal objects are interchangeable with respect to all predicates and functions.
Substitutivity is one of the most important logical uses of equality. It supports rigorous derivations and prevents distinctions without difference.
5.3 Axioms for equality
Axioms for equality typically include reflexivity, and may also include congruence principles for functions and predicates. These axioms ensure that equality behaves consistently with the rest of the formal system. In some presentations, equality is treated as a logical symbol with built-in rules rather than as an ordinary relation.
Such axioms make it possible to reason about identical objects in a controlled and general way.
6 Inference and proof
Inference in predicate logic concerns the valid movement from premises to conclusions. Proof systems provide formal rules that permit such movement step by step. These systems are designed to preserve truth under interpretation.
Different proof styles highlight different aspects of reasoning, but they all aim to capture valid logical consequence in a precise manner.
6.1 Natural deduction
Natural deduction is a proof method that mirrors ordinary reasoning. It uses introduction and elimination rules for connectives and quantifiers, allowing formulas to be derived in a structured sequence. The method is often valued for its readability and closeness to informal argument.
It is especially useful in teaching and in constructing proofs that follow a clear argumentative flow.
6.2 Sequent calculus
Sequent calculus represents inference as transformations between sequents, which express that certain premises entail certain conclusions. Its rules are highly systematic and are well suited to metatheoretic analysis. The format makes structural features of inference explicit.
This proof style is influential in logic and computer science because it supports formal manipulation of derivations.
6.3 Axiomatic systems
Axiomatic systems begin with selected axioms and use inference rules to derive theorems. In predicate logic, these systems are designed so that all valid formulas can be obtained by formal derivation. They provide a compact and rigorous framework for logical deduction.
Axiomatic presentations emphasize economy and precision. They are often used to study the foundational properties of logic.
6.4 Rules for quantifiers
Rules for quantifiers govern how universal and existential statements may be introduced or applied in proofs. Universal instantiation allows a general statement to be applied to a particular case, while universal generalization allows a proven property of an arbitrary object to be stated universally. Existential instantiation and existential introduction serve analogous roles for existence claims.
These rules require careful handling of variable conditions. Improper use can lead to invalid conclusions.
6.5 Soundness
Soundness means that every formula provable in the system is valid in all intended interpretations. In other words, the proof rules do not permit false conclusions from true premises. This property is essential because it guarantees that formal derivations are trustworthy.
Soundness connects proof theory with semantics. It shows that syntactic derivability respects meaning.
6.6 Completeness
Completeness means that every valid formula is provable in the system. For first-order logic, this is a major metatheoretic result and one of the central achievements of formal logic. It establishes that the proof system is powerful enough to capture all semantic validity.
Completeness links the limitations of proof with the full range of logical truth. Together with soundness, it gives first-order logic a particularly robust logical foundation.
7 Normal forms and transformations
Normal forms are standardized ways of rewriting formulas without changing their logical content. They are useful in automated reasoning, proof analysis, and decision procedures for restricted fragments. Transformations into normal form often simplify the structure of formulas.
These methods do not alter the underlying meaning, but they can make a formula easier to study or process mechanically.
7.1 Prenex normal form
A formula is in prenex normal form when all quantifiers appear at the front, followed by a quantifier-free matrix. Converting to this form can clarify the logical structure of a statement by separating quantification from the internal propositional content.
Prenex form is commonly used as an intermediate step in theoretical and computational logic. It is particularly helpful when analyzing quantifier patterns.
7.2 Skolemization
Skolemization is a transformation that removes existential quantifiers by introducing new function symbols or constants. It preserves satisfiability under appropriate conditions, though not exact logical equivalence in a simple sense. The method is widely used in automated theorem proving.
By replacing existential claims with explicit witnesses, Skolemization helps simplify formulas for further processing.
7.3 Conjunctive normal form
Conjunctive normal form is a standardized shape in which a formula is expressed as a conjunction of disjunctions of simpler components. In first-order logic, reaching this form often requires several preliminary transformations, including the elimination of implications and the movement of quantifiers.
This form is important because it supports resolution-based proof methods and other mechanical procedures.
7.4 Elimination of quantifiers
Quantifier elimination seeks to rewrite formulas so that no quantifiers remain, when this is possible in a given theory. Some mathematical structures admit systematic elimination procedures, which can make reasoning much simpler. In such cases, statements can be reduced to quantifier-free equivalents.
Where available, quantifier elimination is a powerful tool for deciding theories and describing definable sets.
8 Decision problems and limitations
Decision problems ask whether there is an effective method for determining the truth or satisfiability of formulas. Predicate logic is rich enough to express many kinds of reasoning, but this expressiveness comes with important limitations. Some tasks are solvable only in restricted cases.
Understanding these limitations is crucial for both logic and computation.
8.1 Satisfiability
A formula is satisfiable if there is some model in which it is true. Satisfiability asks whether such a model exists. This problem is central in logic, because it concerns whether a formula describes a coherent situation at all.
Satisfiability is often easier to study than validity, but in first-order logic it remains highly nontrivial in general.
8.2 Validity
A formula is valid if it is true in every model of the language. Validity is the semantic counterpart of logical theoremhood. Determining whether a formula is valid is a fundamental problem in formal reasoning.
Because validity quantifies over all interpretations, it is typically harder than checking truth in a single structure.
8.3 Decidability
A logical system is decidable if there is an algorithm that always determines whether a formula has a given property, such as validity or satisfiability. Some fragments of first-order logic are decidable, especially when the language or theory is restricted. However, full first-order logic is not decidable.
Decidability is a major concern in logic, computer science, and automated reasoning because it marks the boundary between tractable and intractable formal tasks.
8.4 Undecidability
Undecidability means that no algorithm can solve the relevant problem in all cases. For full predicate logic, key problems such as validity are undecidable. This does not imply that specific formulas cannot be solved, only that there is no universal procedure for all formulas.
Undecidability reveals a fundamental limit on mechanical reasoning. It is one of the most important results in mathematical logic.
8.5 Compactness theorem
The compactness theorem states that if every finite subset of a set of first-order sentences is satisfiable, then the whole set is satisfiable. This result has strong consequences for model construction and theory analysis. It often allows one to infer the existence of models from finite consistency conditions.
Compactness is a hallmark of first-order logic and plays a major role in model theory and abstract algebra.
9 Relationship to other logical systems
Predicate logic sits within a broader family of logical systems. It is more expressive than propositional logic, but less expressive than some higher-order systems. Its relation to other logics helps clarify what it can and cannot say.
Comparisons with related systems also highlight why first-order logic became the standard framework in much of mathematics and theoretical computer science.
9.1 Propositional logic
Propositional logic treats whole statements as atomic units and studies how they combine using logical connectives. Predicate logic extends this framework by analyzing the internal structure of statements. It introduces variables, predicates, and quantifiers, which greatly increase expressive power.
Many basic logical principles remain the same in both systems, but predicate logic can state patterns that propositional logic cannot capture directly.
9.2 Higher-order logic
Higher-order logic goes beyond first-order logic by allowing quantification over predicates, relations, or other higher-level entities. This expansion increases expressive power significantly. It can represent concepts that are awkward or impossible to define within first-order logic alone.
The tradeoff is that higher-order systems are generally less manageable from a proof-theoretic and semantic standpoint.
9.3 Modal logic
Modal logic adds operators for necessity, possibility, or related notions. Although it is structurally different from predicate logic, the two systems can be combined or compared through formal translations. Predicate logic supplies a framework for objects and relations, while modal logic introduces an additional layer of modality.
Their interaction is important in philosophy, linguistics, and the study of possible-world semantics.
9.4 Second-order logic
Second-order logic allows quantification over sets, properties, or relations of objects. It is stronger than first-order logic and can characterize certain structures more categorically. However, this greater expressiveness comes with reduced completeness properties and more difficult metatheory.
The distinction between first-order and second-order logic is a central topic in the foundations of logic.
10 Applications
Predicate logic is widely used wherever precise formal description is needed. Its applications range from pure mathematics to computer science and verification. Because it offers a uniform language for stating and analyzing structure, it remains one of the most influential formal systems in modern thought.
10.1 Mathematics
In mathematics, predicate logic underlies formal definitions, theorems, and proofs. It is used to express axioms for structures such as groups, fields, orders, and set-theoretic systems. The language is especially valuable because it can state universal laws and existence claims with exact clarity.
Mathematicians also use it as a metatheoretical tool to study consistency, completeness, and definability.
10.2 Computer science
In computer science, predicate logic appears in databases, programming language theory, knowledge representation, and specification languages. It provides a formal basis for querying structured information and for describing the behavior of systems. Logical formulas can encode constraints, invariants, and relationships among data items.
Its precision makes it useful for reasoning about programs and algorithms at an abstract level.
10.3 Automated theorem proving
Automated theorem proving uses algorithms to search for formal proofs or establish logical consequence. Predicate logic is a primary target for such systems because it is expressive enough for many mathematical and computational tasks. Techniques often rely on normal forms, unification, resolution, and related methods.
This area connects logic with symbolic computation and has influenced both theoretical research and practical tools.
10.4 Formal verification
Formal verification applies logical methods to check whether systems meet specified requirements. Predicate logic can express safety conditions, consistency constraints, and behavioral properties. It is used in the analysis of software, hardware, and abstract models.
The appeal of formal verification lies in its ability to provide rigorous guarantees, especially where informal testing may miss subtle errors.