Predicate logic builds on propositional logic by adding quantifiers and variables. Where propositional logic can only handle simple true/false statements, predicate logic lets you make claims about properties of objects and relationships between them. This is what makes it possible to express statements like "every even number greater than 2 is the sum of two primes" in a precise, formal way.
This topic matters because predicate logic is the language mathematicians use to write definitions, theorems, and proofs. Getting comfortable with it now will make everything from set theory to analysis feel more natural.
Fundamentals of predicate logic
Predicate logic takes the logical connectives you already know from propositional logic (and, or, not, implies) and adds two new ingredients: predicates that describe properties or relationships, and quantifiers that let you talk about entire collections of objects at once.
Propositional vs predicate logic
Propositional logic deals with simple statements that are either true or false, connected by logical operators. You can say things like "if it rains, the ground is wet," but you can't say anything about specific objects or their properties.
Predicate logic fixes this by introducing predicates. Instead of just being a standalone true/false statement, you can write to mean " has property ." For example, means "7 is prime."
- Propositional logic: "It is raining" (just true or false)
- Predicate logic: " is greater than 5" (depends on what is)
- Predicate logic can express statements about infinite domains, like "for all natural numbers , "
Quantifiers and variables
Two quantifiers do the heavy lifting in predicate logic:
- The universal quantifier means "for all" or "for every." The statement claims that every object in the domain has property .
- The existential quantifier means "there exists" or "for some." The statement claims that at least one object in the domain has property .
Variables like , , act as placeholders for objects in the domain of discourse (the set of things you're talking about). Quantifiers bind variables, turning open expressions into complete statements. For instance, on its own isn't true or false until you either assign a value to or quantify it: or .
Combining quantifiers lets you express sophisticated ideas. The formal definition of continuity of a function, for example, uses with nested quantifiers.
Predicates and arguments
A predicate is a property or relation that becomes true or false once you plug in specific arguments. The arity of a predicate is how many arguments it takes:
- Unary (1 argument): means " is even"
- Binary (2 arguments): means ""
- n-ary (n arguments): relations involving three or more objects
Before quantification, a predicate with variables is called a propositional function. It doesn't have a truth value yet. Once you quantify all the variables, it becomes a full sentence with a definite truth value.
Syntax of predicate logic
Syntax defines the rules for building valid expressions. Just like grammar rules in a language, these rules ensure that every formula has exactly one meaning.
Well-formed formulas
A well-formed formula (wff) is any expression built according to the syntactic rules of predicate logic:
- Atomic formulas are the simplest: a predicate applied to terms (variables or constants). Example: , .
- Compound formulas are built from atomic formulas using logical connectives (, , , , ) and quantifiers (, ).
- Parentheses clarify the order of operations and the scope of quantifiers.
The definition is recursive: if and are wffs, then , , , etc., are also wffs.
Scope of quantifiers
The scope of a quantifier is the portion of the formula that the quantifier governs. It extends from the quantifier to the end of the subformula it's attached to (usually marked by parentheses).
In , the scope of is the entire expression . But in , the scope of covers only , and the in is not bound by that quantifier.
When quantifiers are nested, like , each quantifier has its own scope. Getting scope wrong is one of the most common sources of ambiguity, so pay close attention to parentheses.
Free and bound variables
- A bound variable appears within the scope of a quantifier that binds it.
- A free variable is not within the scope of any quantifier.
In , the variable is bound and is free. The same variable can even be free in one part of a formula and bound in another.
A formula with no free variables is called a sentence. Sentences have definite truth values under a given interpretation; formulas with free variables do not (until you assign values to those variables).
Semantics of predicate logic
While syntax tells you how to write formulas, semantics tells you what they mean. Semantics is about assigning truth values to formulas based on an interpretation.
Truth values and interpretations
An interpretation specifies:
- A domain of discourse (the set of objects you're reasoning about)
- A meaning for each predicate (which objects satisfy it)
- A meaning for each constant (which object it refers to)
A variable assignment maps any free variables to specific elements in the domain. The truth value of a formula depends on both the interpretation and the variable assignment.
For example, is true under an interpretation if and only if is true for every element in the domain.
Models and structures
A model is an interpretation that makes a given formula (or set of formulas) true. A structure consists of a domain together with interpretations for all predicates and constants.
Two structures are isomorphic if there's a one-to-one correspondence between their domains that preserves all predicate relationships. Isomorphic structures satisfy exactly the same sentences.
Model theory, the study of relationships between formal theories and their models, is important for understanding whether axiom systems are consistent and whether certain statements are independent of others.
Satisfiability and validity
These three categories cover every formula:
- Satisfiable: true under at least one interpretation
- Valid (a tautology): true under every interpretation
- Unsatisfiable: false under every interpretation
One major difference from propositional logic: validity in predicate logic is undecidable. There's no algorithm that can always determine in finite time whether an arbitrary predicate logic formula is valid. (For propositional logic, you can always just build a truth table.)

Quantifier rules and operations
Knowing how quantifiers interact with logical connectives is essential for manipulating formulas in proofs.
Universal quantification
claims that a property holds for every element in the domain. If even one element fails to satisfy the property, the universally quantified statement is false.
Key distributivity facts:
- distributes over conjunction:
- does not distribute over disjunction:
To see why the second fails, consider a domain where every element is either red or blue, but not all elements are red and not all are blue.
Existential quantification
claims that at least one element in the domain satisfies the property.
Key distributivity facts:
- distributes over disjunction:
- does not distribute over conjunction:
For the second, knowing that some element is and some element is doesn't mean a single element is both.
Negation of quantifiers
Negating quantifiers flips them and pushes the negation inward. These are sometimes called De Morgan's laws for quantifiers:
- ("Not everything is " means "something is not ")
- ("Nothing is " means "everything is not ")
These equivalences are used constantly in proofs, especially in proofs by contradiction where you negate a quantified statement and work with the result.
Inference in predicate logic
Inference rules let you derive new true statements from ones you already know. Predicate logic keeps the rules from propositional logic and adds rules for handling quantifiers.
Rules of inference
The four quantifier rules to know:
- Universal instantiation: From , conclude for any constant in the domain. (If something is true for all, it's true for any specific one.)
- Universal generalization: If you can prove for an arbitrary (with no special assumptions about ), conclude .
- Existential generalization: From for some specific constant , conclude . (If it's true for one, then something satisfies it.)
- Existential instantiation: From , introduce a new constant (not used elsewhere in the proof) and assume .
These combine with propositional rules like modus ponens (from and , conclude ).
Validity of arguments
An argument is valid if whenever all the premises are true, the conclusion must also be true. Validity depends entirely on the logical form, not on what the predicates actually mean.
An argument that is both valid and has true premises is called sound. Soundness is what you actually want in a mathematical proof: correct reasoning from true starting points.
Soundness vs completeness
These are properties of the logical system itself, not of individual arguments:
- Soundness: Every formula that can be proved is actually true in every model. (The system never proves anything false.)
- Completeness: Every formula that is true in every model can be proved. (The system can prove everything that's true.)
Gödel's completeness theorem (1929) shows that first-order predicate logic is both sound and complete. This is a strong guarantee: the proof system perfectly matches the semantics. Don't confuse this with Gödel's incompleteness theorems, which are about specific mathematical theories like arithmetic, not about the logic itself.
Limitations of predicate logic
First-order predicate logic is powerful, but it can't do everything. Recognizing its boundaries helps you understand why mathematicians sometimes reach for stronger systems.
Expressiveness and decidability
- First-order logic cannot express certain concepts directly, such as "the transitive closure of a relation" or "there are finitely many elements satisfying ."
- Validity is undecidable: no algorithm can determine whether an arbitrary first-order formula is valid. However, it is semi-decidable, meaning if a formula is valid, a proof procedure will eventually find a proof. If it's not valid, the procedure might run forever.
- The Löwenheim-Skolem theorem shows that if a first-order theory has an infinite model, it has models of every infinite cardinality. This means first-order logic can't pin down the "size" of infinite structures.
Higher-order logic
Higher-order logic allows quantification over predicates and functions, not just individual elements. You can write things like "for every property ..." which first-order logic can't express.
This extra power lets you define concepts like continuity and compactness more naturally. The trade-off is that higher-order logic loses the completeness and compactness properties that make first-order logic so well-behaved. Higher-order logic is used in formal verification of software and hardware.

Modal logic extensions
Modal logic adds operators for necessity () and possibility (). Instead of just asking whether something is true, you can ask whether it must be true or could be true.
Kripke semantics provides the formal framework: truth is evaluated across a set of "possible worlds" connected by an accessibility relation. Modal logic has applications in philosophy, computer science (reasoning about program states), and temporal reasoning.
Applications of predicate logic
Predicate logic isn't just theoretical. It shows up in practical systems you interact with regularly.
Formal verification
Formal verification uses predicate logic to prove that software or hardware behaves correctly. Engineers write specifications as logical formulas and then use automated theorem provers to verify that a system meets those specifications. This is especially critical in safety-sensitive fields like aerospace, medical devices, and automotive systems, where bugs can be catastrophic.
Database query languages
SQL and relational databases are grounded in predicate logic. Relational calculus, one of the theoretical foundations of database queries, is essentially first-order logic applied to tables of data. When you write a SQL WHERE clause, you're constructing a predicate. Query optimizers use logical equivalences to rewrite queries into more efficient forms.
Artificial intelligence reasoning
Predicate logic is a core tool for knowledge representation in AI. Expert systems encode domain knowledge as logical rules and use inference to draw conclusions. The programming language Prolog is directly based on first-order logic, with programs written as collections of facts and rules. Predicate logic also underlies automated planning and contributes to explainable AI, where formal reasoning makes a system's decisions transparent.
Proof techniques in predicate logic
These are systematic methods for constructing proofs in predicate logic. Each has different strengths depending on the situation.
Natural deduction
Natural deduction is a proof system that closely mirrors how mathematicians actually reason. You work with introduction rules (which let you conclude a connective or quantifier) and elimination rules (which let you use one).
For example, to prove , you assume an arbitrary element , prove without using anything special about , and then apply universal generalization. Proofs are structured as trees showing how each step depends on previous ones, and you can make temporary assumptions that get "discharged" later (as in conditional proofs).
Resolution method
Resolution is a refutation-based technique: to prove a formula, you negate it and show the negation leads to a contradiction.
- Negate the formula you want to prove.
- Convert everything to clausal form (a conjunction of disjunctions of literals).
- Repeatedly apply the resolution rule: if one clause contains and another contains , combine them into a new clause with and removed.
- If you derive the empty clause (a contradiction), the original formula is valid.
Resolution is complete for first-order logic, meaning it will always find a contradiction if one exists. It's the backbone of many automated theorem provers and logic programming systems.
Tableaux method
The tableaux method (also called the truth tree method) systematically breaks formulas apart to test satisfiability.
- Start with the formula you want to test (or its negation, if checking validity).
- Apply decomposition rules to break compound formulas into simpler components, branching the tree when a disjunction requires considering multiple cases.
- If every branch contains a contradiction (both and for some formula), the tableau is closed, and the original formula is unsatisfiable.
- If any branch stays open with no contradictions, that branch describes a model, showing the formula is satisfiable.
Tableaux are particularly useful for finding counterexamples and for exploring what models look like.
Predicate logic in mathematics
Predicate logic provides the formal language that modern mathematics is built on.
Set theory formalization
Zermelo-Fraenkel set theory (ZF, or ZFC with the Axiom of Choice) is axiomatized in first-order predicate logic. Each axiom is a first-order sentence describing what sets exist and how they behave. This careful formalization was developed partly to avoid paradoxes like Russell's paradox (the set of all sets that don't contain themselves). ZF set theory serves as the standard foundation for nearly all of modern mathematics.
Number theory applications
The Peano axioms for the natural numbers are expressed in predicate logic. They define zero, the successor function, and the principle of induction, giving a formal basis for arithmetic.
Gödel's incompleteness theorems use predicate logic to encode statements about number theory within number theory itself, showing that any consistent system powerful enough to describe arithmetic contains true statements it cannot prove. Number theory formalized in predicate logic also underpins applications in cryptography and theoretical computer science.
Foundations of mathematics
Predicate logic provides the formal language for axiomatizing mathematical structures like groups, rings, and fields. Each of these is defined by a set of first-order axioms, and predicate logic lets you rigorously investigate questions about consistency (can the axioms ever contradict each other?) and independence (can a statement be neither proved nor disproved from the axioms?).
Gödel's incompleteness theorems, which are results about formal systems expressed in predicate logic, reveal fundamental limits on what any sufficiently powerful formal system can achieve. Predicate logic thus serves as both the tool for building mathematical foundations and the lens for understanding their limitations.