Chapter 9

FOL Inference

Johannes Korbmacher about 50 min read updated 09/10/2026

In Chapter 8 · FOL, we introduced the concept of an FOL model and studied it as a form of knowledge representation. A model specifies which objects there are, what their properties are, and which relations they stand in. In this way, we can think of the models as storing information about the world. As we’ve seen, this information can be “queried” using FOL formulas.

We now turn to the logical purpose of FOL models: to define valid FOL inference. Following the definition pattern from Chapter 3 · Valid inference, we ask: Does every model that makes our premises true also make the conclusion true? To illustrate, consider Socrates again:

The premises tell us that Socrates is human and that all humans are mortal. Whatever else a model contains, those two facts require Socrates to be mortal. The same kind of reasoning appears in mathematics. If every number is smaller than its successor S(x), then every number has a larger number:

How can a computer establish such inferences? Having defined validity for FOL inference, we quickly meet a fundamental computational limit: as a matter of mathematical fact, no algorithm can decide every case. Yet FOL remains a standard for rigorous reasoning in mathematics and AI. So, we need methods for finding and checking proofs — even if they cannot settle every question. In this chapter, we will extend the resolution algorithm to FOL, we’ll extend natural deduction and Lean to quantifiers, and we’ll use Lean to verify a bona fide mathematical argument from Boolean algebra.

Valid inference

Our definition pattern for valid inference is the one from Chapter 3 · Valid inference: whenever the premises are true, the conclusion must be true too. Chapter 8 · FOL supplied the definition of FOL models and the truth conditions for FOL formulas in a model under a variable assignment. We get:

Note that for sentences, we can omit the assignment: every model of the premises must make the conclusion true. As in Chapter 3 · Valid inference, the symbol ∴ indicates an inference, while the symbol ⊨ asserts that it is valid.

To illustrate, take any model that makes the premises of our Socrates inference true. This means that in the model, all humans are mortal, and the object named Socrates is among its humans. So that object is mortal. Inspect the diagram below to convince yourself of the fact that our definitions give us precisely this result. Note that in the model there may be other objects, and Socrates may denote a different object in another model; the argument still works.

The diagram shows only what the premises tell us about an arbitrary model.

A countermodel (glossary, opens in a new tab) makes the premises true and the conclusion false. Reverse the Socrates inference:

Here is a complete countermodel with one mortal object and no humans: a model where the premises of the inference are true but the conclusion is false.

Our mathematical example uses the same method. In any model of ∀x (x < S(x)), take an arbitrary object d. The premise says that d < S(d), so S(d) supplies the existential witness. This works for every object d ∈ D:

As in Chapter 8 · FOL, we write LessThan(x, y) for x < y. Interpreting S(n) as n + 1 and < as the usual ordering gives our natural-number example. The inference itself needs only the stated premise. Neither symbol has its intended mathematical meaning built into FOL.

We cannot exchange the quantifiers in the conclusion. On the natural numbers, each x has a larger number, but no one number is larger than them all:

The witness may depend on x. We’ll return to this restriction when we introduce the quantifier rules.

Could we automate validity by checking models? In propositional logic, a truth-table lists all assignments to the finitely many variables. FOL has models of arbitrarily large finite size, and infinite models too.

Checking size one, then two, and so on never reaches an infinite model. Some FOL sentences have only infinite models, as we saw in Chapter 8 · FOL. Their negations hold in every finite model but can still fail in an infinite one. Finite testing can therefore miss a countermodel altogether.

This is the limit established by Church and Turing’s work on the decision problem (opens in a new tab) . The halting problem (glossary, opens in a new tab) can be encoded in first-order inference: a general decision procedure for these inferences would also decide whether any given program stops. Turing showed that no algorithm can do that. See Wikipedia’s halting problem article (opens in a new tab) .

Proofs still give us a way to automate inference. They are finite, and checking their steps can be mechanical. A complete calculus guarantees a proof for every valid inference. Searching all candidate proofs will eventually find it.

We will study resolution for automated proof search, then natural deduction and Lean for constructing and checking proofs. Both need to handle the objects inside our formulas. Even Socrates’s inference requires matching the general claim about Human(x) with the particular fact Human(Socrates). Finding such substitutions is our first computational task.

Unification

To apply modus ponens to the Socrates premises, we first instantiate the bound variable in the universal premise with the constant (glossary, opens in a new tab) Socrates. That gives us Human(Socrates) → Mortal(Socrates), to which we can apply modus ponens.

The choice of term came from matching Human(x) with Human(Socrates). We want an algorithm to find such matches even when the terms contain functions or several variables.

Here σ = [x/Socrates]. We use the substitution (glossary, opens in a new tab) convention from Chapter 8 · FOL: [x/t] replaces free occurrences of x by the term (glossary, opens in a new tab) t. It must not capture variables. For unification, we’ll initially work with terms and atomic formulas, which contain no quantifier binders.

A substitution can replace several variables simultaneously. For example, R(x,y) and R(a,f(a)) have the unifier [x/a,y/f(a)]. Constants and function symbols (glossary, opens in a new tab) remain fixed. We can’t unify Human(a) with Mortal(a) by replacing the predicate Human.

For R(x,y) and R(z,z), the substitution [x/z,y/z] is an MGU. The substitution [x/a,y/a,z/a] also unifies them, but makes an additional choice – viz. [z/a]. An MGU leaves such a choice available for later inference steps.

Robinson’s algorithm

The first algorithm for unification (glossary, opens in a new tab) is due to John Alan Robinson (opens in a new tab) , who also developed the resolution method we’ll study next. The algorithm builds a substitution by comparing the expressions a pair of terms at a time.

Suppose we want to unify LiesBetween(Munich, y, z) and LiesBetween(x, Milan, Rome). Before comparing their arguments, we check:

1. Do the signs agree? Both literals are positive. A positive literal and a negative one, such as Human(x) and ¬Human(Socrates), cannot become identical by substituting terms.
2. Do the predicates agree? Both use the three-place predicate LiesBetween. Substitution cannot change a predicate symbol or its arity; for example, it cannot turn Human(x) into Mortal(x).

Our two literals pass both checks. We need to make the corresponding arguments agree too: Munich with x, y with Milan, and z with Rome. Record these requirements in a list:

Here s ≐ t asks for a substitution that makes s and t syntactically identical. ≐ records a syntactic matching requirement; = expresses identity between objects in a model. We start with the empty substitution σ = [] and go through the pairs in Eq.

For each pair s ≐ t, distinguish the following cases:

• Delete. If s and t are already identical, delete the pair. There is nothing to do for x ≐ x or Munich ≐ Munich.
• Occurs check / Eliminate. If only s is a variable, say x, check whether it occurs in t. If it does, stop: no unifier exists. This is called the occurs check (glossary, opens in a new tab) . If the occurs check passes, replace x by t in all other pairs and in the terms already recorded in σ. Add [x/t] to σ and delete the pair s ≐ t from Eq.
• Eliminate. If s and t are distinct variables, say x ≐ y, replace x by y throughout the other pairs and the terms already recorded in σ. Add [x/y] to σ and remove the pair from Eq.
• Orient. If only t is a variable, swap the sides and use the case where the first term is a variable. Our pair Munich ≐ x, for example, becomes x ≐ Munich.
• Clash / Decompose. If neither term is a variable, compare their outer symbols and arities. A constant counts as a symbol with no arguments. If the symbols or arities differ, stop — they cannot be unified. If they agree, replace the pair by its corresponding argument pairs. For example, fatherOf(x) ≐ fatherOf(y) becomes x ≐ y.
• Distinct constants, such as Munich and Milan, also give a symbol clash.

Repeat this procedure until a failure occurs or the list is empty. In our example, we successively record [x/Munich], [y/Milan], and [z/Rome]. No pairs remain, so their combination unifies the original literals. In general, successful termination gives a most general unifier.

Decompose compares the arguments of the two expressions. The remaining equations and the substitution σ record what still needs to be matched and what we have established so far.

The occurs check (glossary, opens in a new tab) prevents a variable from being replaced by a term containing that same variable. Try x and fatherOf(x). Whatever finite term replaces x, the right side still has an extra fatherOf around it. They cannot become identical. We delete x ≐ x before this check because identical terms need no replacement. Wikipedia’s occurs check (opens in a new tab) article explains the consequences of omitting it.

Updating earlier replacements is called composition. In Nested functions, we first record [y/motherOf(x)], then discover [x/London]. The final substitution must send y directly to motherOf(London).

For resolution, we want opposite-sign literals with matching atoms. We therefore apply the algorithm to those atoms, leaving their signs alone. The term comparisons are exactly the same.

Here is the algorithm in the Python-like Chapter 2 · pseudocode introduced in Chapter 2 · Formal languages. take_equation removes the first equation; left and right read its two sides. substitute_all replaces the variable throughout the remaining equations. compose makes the same replacement in recorded terms and adds the new binding. argument_equations supplies the pairs of arguments, and prepend puts them at the front of the list.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22

def unify(equations):
    substitution = empty_substitution()
    while not is_empty(equations):
        equation = take_equation(equations)
        first = left(equation)
        second = right(equation)
        if first == second:
            continue
        if is_variable(second) and not is_variable(first):
            equation = reverse(equation)
            first = left(equation)
            second = right(equation)
        if is_variable(first):
            if occurs(first, second):
                return failure
            equations = substitute_all(equations, first, second)
            substitution = compose(substitution, first, second)
        else:
            if not matching_heads(first, second):
                return failure
            equations = prepend(argument_equations(first, second), equations)
    return substitution

matching_heads checks the fixed symbol, its kind, and its arity. Each elimination removes a variable from the unsolved equations. Between eliminations, decomposition reduces the expressions to their parts. Thus the algorithm terminates. Its steps preserve the possible solutions, and successful termination supplies an MGU. Unification itself is decidable even though unrestricted first-order validity is not.

Wikipedia’s unification article (opens in a new tab) compares Robinson’s procedure with later algorithms.

Universally quantified rules such as ∀x∀y (Sibling(x,y) → Sibling(y,x)) can be used by instantiating both variables. A match with Sibling(a,b) supplies [x/a,y/b] and gives Sibling(b,a) by modus ponens. This supports first-order forward and backward chaining on suitable rule sets.

We cannot delete quantifiers wherever they occur. Consider:

This says that anyone bigger than everything is a giant. Together with ∀y BiggerThan(PolyphemOS,y), it entails Giant(PolyphemOS). The single fact BiggerThan(PolyphemOS,tinymouse) does not suffice. A domain with two objects p,m, with BiggerThan true only of (p,m) and Giant true of nothing, gives a countermodel to that second inference. Interpret PolyphemOS as p and tinymouse as m.

The inner universal occurs in a conditional antecedent. Rewriting the conditional exposes its role:

The rewritten formula contains an existential quantifier. Before applying resolution, we need to replace it in a way that preserves satisfiability.

Normal forms

Resolution, like the other algorithms we’ve studied, expects its input in a particular form. In Chapter 5 · Boolean SAT, that form was CNF: a conjunction of clauses. First-order resolution also works with clauses, but their atoms can now contain predicates, variables, and function terms. The clauses have no written quantifiers; their variables are understood as universally quantified.

How do we put a quantified formula into this form? In propositional logic, we could use equivalent rewrites throughout. In FOL, we cannot generally eliminate existential quantifiers that way. For example, ∃x Human(x) says that there is a human, but does not name one. Replacing it with Human(a) would make a claim about a particular object, which might not be human. We need a different guarantee for this preprocessing step.

Other first-order normal forms organize quantifiers differently. Prenex normal form (opens in a new tab) , for example, puts all quantifiers at the front. We won’t study those forms here; our aim is the clause form required by resolution.

Equisatisfiability

For a satisfiability test, we need to preserve whether a model exists. We met this requirement in the optional discussion of Tseytin conversion in Chapter 5 · Boolean SAT:

Logical equivalence (glossary, opens in a new tab) requires the same truth-value in every model. Equisatisfiability requires only agreement on whether there is a model at all. That is enough for a refutation: if the rewritten input has no model, neither does the original input.

Consider ∃x Human(x) again. This time, introduce a fresh constant sk₁ and replace the sentence by Human(sk₁). If there is a human, we can interpret sk₁ as that human. Conversely, if Human(sk₁) is true, there is a human. The two sentences are therefore equisatisfiable.

They are not equivalent. In a model containing a human and a nonhuman, ∃x Human(x) is true. Interpreting sk₁ as the nonhuman makes Human(sk₁) false. We can make it true by choosing the human instead.

Freshness lets us make this choice without changing the interpretation of any symbol in the original input. Thus we can preserve satisfiability of the premises together with the negated conclusion, which is what a refutation needs. For example, if we also have ¬Human(a), using a as the witness would introduce a contradiction; a fresh sk₁ can name someone else.

Skolemization

The trick for eliminating existential quantifiers is called Skolemization (glossary, opens in a new tab) . We give each existential a fresh name for its witness. The result is equisatisfiable with the original formula, which is enough for testing satisfiability and consequence. When a witness depends on another object, its name must be a function term.

We prepare the formula and eliminate its existentials in this order:

1. Eliminate → and ↔. Use the same equivalences as in propositional CNF conversion, starting with A → B ≡ ¬A ∨ B.
2. Move negations to atoms. Use De Morgan’s laws, remove double negations, and rewrite ¬∀x A as ∃x¬A and ¬∃x A as ∀x¬A. This gives negation normal form (glossary, opens in a new tab) : negations apply only to atoms. A negated universal has now become an existential, so it too needs a witness.
3. Give distinct quantifiers distinct variables. This is α-renaming (glossary, opens in a new tab) . For example, ∃x(Human(x) ∧ ∀x Mortal(x)) becomes ∃x(Human(x) ∧ ∀y Mortal(y)). Choose names unused elsewhere in the input. The renamed occurrences still belong to the same quantifiers.
4. Replace each existential by a fresh witness. Work from the outside in. List the universal variables whose scopes contain that existential; they become the arguments of its witness function. If there are none, use a constant. Apply the following rule until no existential quantifiers remain.

Here ⟹ marks an equisatisfiable transformation of the whole sentence. The substitution replaces the free occurrences of y in B; the new symbol must be unused throughout the input. The first three preparation steps preserve equivalence. The witness replacement preserves satisfiability.

For ∀x∃y R(x,y), the witness for y may depend on x. A fresh Skolem function (glossary, opens in a new tab) sk₁ records that choice:

For ∃y∀x R(x,y), we must choose one witness before considering x. In this separate example, sk₁ is a fresh Skolem constant (glossary, opens in a new tab) :

The difference is visible in a two-object model where R is identity. Every object is related to itself, so the first sentence is true. No one object is related to both objects, so the second is false. Using a constant for the first sentence would incorrectly require a shared witness.

Each existential gets its own fresh symbol. For example, ∀x(∃y R(x,y) ∧ ∃z R(z,x)) becomes ∀x(R(x,sk₁(x)) ∧ R(sk₂(x),x)). Different symbols allow different choices; sk₁(d) and sk₂(d) may still denote the same object. Only enclosing universal quantifiers supply arguments: in ∀x((∀y R(x,y)) ∨ ∃z R(x,z)), the witness for z is sk₁(x). The quantifier ∀y belongs to the other branch.

The following examples show the four steps, one rewrite at a time:

CNF conversion

Skolemization leaves us with universal quantifiers and a formula built from literals using ∧ and ∨. We still need a conjunction of clauses. The full conversion procedure is:

1. Eliminate arrows, move negations inward, rename bound variables, and Skolemize, following the four steps above.
2. Leave the remaining universal quantifiers implicit. Since their variables are distinct and only ∧ and ∨ connect their scopes, we can read all remaining variables as universally quantified.
3. Distribute ∨ over ∧, using the propositional CNF equivalences.
4. Take each conjunct as a clause. Its universal closure (glossary, opens in a new tab) quantifies all its free variables; each clause has its own variable scope.

For example, start with:

There are no arrows or negations to change, and the bound variables are already distinct. Skolemization gives:

Leave ∀x implicit and distribute the disjunction. The resulting CNF is:

Both clauses are understood as universally closed. The conjunction is satisfiable exactly when the original sentence is. We can now pass these clauses to resolution.

FOL resolution

With the input in clause form, we can use unification to extend resolution to FOL. As in Chapter 5 · Boolean SAT, we test an inference by looking for a contradiction in its premises together with the negated conclusion.

For an inference, add the negation of the conclusion to the premises:

A model of these sentences would be a countermodel to the inference. A refutation (glossary, opens in a new tab) rules out such a model. This is the same reduction we used in Chapter 5 · SAT, now over FOL models. The undecidability result rules out a general decision procedure for FOL SAT too.

For Socrates, the premises and negated conclusion have the clause form:

The semicolons separate conjuncts. The first clause means ∀x(¬Human(x) ∨ Mortal(x)). As in Chapter 6 · Conditionals, associativity, commutativity, and idempotence let us ignore brackets, order, and repeated identical literals within a clause. The empty clause (glossary, opens in a new tab) ⊥ is false in every model; deriving it establishes that the clauses cannot all be true.

In Chapter 5 · SAT, resolution cancelled an atom against its negation. In FOL, we first use unification to make the selected atoms match. For instance, Human(x) matches Human(Socrates) under [x/Socrates].

The rule for first-order resolution (glossary, opens in a new tab) is:

In Resolution, B and D are atoms, and σ is their MGU. The other literals form C and E; either part can be empty. Remove the two opposite-sign literals, join what remains, and apply σ throughout. The Factoring rule beneath it combines matching literals of the same sign within one clause. We’ll use that rule shortly.

The selected opposite-sign literals are the pivots (glossary, opens in a new tab) . Their atoms must unify. Apply the substitution to every remaining literal in both clauses. Resolving (¬Human(x) ∨ Mortal(x)) with Human(Socrates) therefore gives Mortal(Socrates). Resolving that with ¬Mortal(Socrates) gives the empty clause.

Each use of a clause needs fresh variables. This is called standardizing apart (glossary, opens in a new tab) . For example, P(x) and ¬P(f(x)) have separate universal scopes. Renaming the second variable to y permits the unifier [x/f(y)] and an empty resolvent. Treating the two printed occurrences of x as one variable would incorrectly make the occurs check block that inference.

Factoring (glossary, opens in a new tab) unifies two same-sign literals in one clause, applies the unifier to the whole clause, and retains one copy of the resulting duplicate literal.

The clauses (P(x) ∨ P(y)) and (¬P(u) ∨ ¬P(v)) are jointly unsatisfiable. Factoring gives the unit clauses P(y) and ¬P(v), which resolve to the empty clause. Binary resolution alone is insufficient for completeness; factoring supplies the required same-clause inferences.

Return to our inference about PolyphemOS: it is bigger than everything, and anyone bigger than everything is a giant. To show that Giant(PolyphemOS) follows, we prepare a refutation:

The premises are ∀x((∀y BiggerThan(x,y)) → Giant(x)) and ∀z BiggerThan(PolyphemOS,z); add ¬Giant(PolyphemOS). Our normal-form procedure gives these three clauses:

The first premise’s inner ∀y became an existential when we moved its negation inward. Its fresh witness sk₁(x) depends on x.

Resolve the first two clauses on BiggerThan. Their atoms require [x/PolyphemOS,z/sk₁(PolyphemOS)]; the remaining clause is Giant(PolyphemOS). Resolving it with the negated conclusion gives ⊥.

Since the prepared clauses are unsatisfiable, the premises together with the negated conclusion are unsatisfiable too. Thus the conclusion follows in every model of the original premises. The Skolem function was an auxiliary symbol used in the refutation. Knowing only that PolyphemOS is bigger than tinymouse would not supply the needed instance BiggerThan(PolyphemOS,sk₁(PolyphemOS)).

Fair search (glossary, opens in a new tab) eventually considers every eligible inference, so it eventually finds such a refutation. A satisfiable input may keep generating clauses such as P(a), P(f(a)), P(f(f(a))), …. Stopping after a fixed number of steps leaves the answer undecided.

With identity, we need rules that respect its fixed interpretation. For example, a=b and P(a) entail P(b). Treating = as an arbitrary predicate would miss this. Equality axioms can be added, while automated provers commonly use specialized equality inferences such as paramodulation or superposition.

Natural deduction

Resolution supplies refutations. To build proofs directly from quantified premises, we extend the natural deduction rules from Chapter 7 · Proofs. The propositional rules still apply. Four quantifier rules control when we may introduce an arbitrary object, instantiate a general claim, supply a witness, or reason from an unknown witness.

Quantifier rules

Universal introduction lets us infer ∀x A from a derivation of A, provided x is not free in any undischarged assumption on which the derivation depends.

The variable x stands for an arbitrary object. Such a variable is often called an eigenvariable (glossary, opens in a new tab) . The side condition ensures that our argument has not assumed anything special about that object. For example, from the open assumption x < z, we cannot infer ∀x (x < z): x is free in an assumption on which the conclusion depends. In the natural numbers, assigning 0 to x and 1 to z makes the assumption true, but ∀x (x < z) is false. In particular, 1 is not smaller than itself.

This blocks the attempted quantifier swap from our earlier example. From ∀x∃y (x < y), we may instantiate at x and reason temporarily with x < z, where z names a witness larger than x. We may not generalize that temporary assumption to ∀x (x < z). The assumption x < z is still open, so the chosen witness may depend on x. Calling x arbitrary does not remove that dependence.

Once an assumption has been discharged, it no longer restricts universal introduction. The next proof first discharges Human(x) to obtain Human(x) → Human(x). No open assumption contains x, so generalization is then allowed:

Universal elimination lets us infer A[x/t] from ∀x A, provided the term t is free for x in A.

Free for (glossary, opens in a new tab) means that no variable in the replacing term becomes bound when we substitute it for a free occurrence of x in A. Consider ∀x∃y (x < y). If we replace x by y in its displayed scope without checking this condition, we get ∃y (y < y). The original sentence is true in the natural numbers, but this supposed instance is false: no number is smaller than itself. The inserted y was captured by the existential quantifier.

We can use y as the term after renaming the conflicting binder. Write the premise as ∀x∃z (x < z); universal elimination now gives ∃z (y < z). Here y remains free, and the conclusion says that the object assigned to it has a larger object.

Together, these rules let us distribute the universal quantifier over a conjunction. Instantiate the premise at an arbitrary x, project each conjunct, and generalize each result:

Existential introduction lets us infer ∃x A from A[x/t], provided t is free for x in A.

The term t supplies a witness (glossary, opens in a new tab) . The free-for condition is the same as for universal elimination. For a counterexample, take A to be ∀y (x = y) and try to use y as the term replacing x. Substituting without renaming would give ∀y (y = y). The resulting inference is invalid:

The left sentence is true in every model. The right sentence says that one object is identical to every object, which is false in any domain with at least two objects. The attempted substitution captured y. After renaming the bound variable, the required instance would be ∀z (y = z), which the reflexivity sentence does not give us.

For example, from Human(Socrates) we obtain ∃x Human(x) using Socrates:

Existential elimination uses ∃x A and a derivation of C under the temporary assumption A[x/z]. It infers C and discharges that assumption. The witness variable z must be free for x in A and must not occur free in C, in ∃x A, or in any remaining undischarged assumption of the inference.

The temporary assumption lets us reason about a witness without knowing which object it is. Discharging that assumption must leave a conclusion independent of the name we chose. Each freshness condition prevents a different mistake:

• The witness variable must not be free in the conclusion C. From ∃y (x < y), we can open a subproof with x < z, but we cannot export x < z as its conclusion. The premise is true in the natural numbers; x < z is false when both free variables are assigned 0. The premise promises a larger object, without saying that an independently chosen z names it.
• The witness variable must not be free in another assumption that remains open. Suppose we also assume ¬(x < z). Using this same z as the witness for ∃y (x < y) would produce a contradiction from x < z and ¬(x < z). But both original premises are true when x and z are assigned 0: there is a number larger than 0, and 0 is not larger than itself. A fresh witness variable avoids that false identification.
• The witness variable must not be free in the existential premise itself. From ∃y (z < y), choosing z as the witness for y would give the temporary assumption z < z. The premise is true in the natural numbers, while that assumption is impossible there. We must give the witness a fresh name.

The substitution A[x/z] must also be free of capture. Rename any conflicting bound variables before opening the subproof. Then discharge the witness assumption when applying existential elimination; any other assumptions used by the subproof remain open.

For example, ∃x Black(x) lets us establish ∃x(Black(x) ∨ White(x)). The temporary witness proves the disjunction, and we existentially quantify it before closing the subproof. The final conclusion contains no free occurrence of its name:

The Chapter 7 · proof strategies extend to quantified goals. A universal goal suggests introducing an arbitrary object. An existential goal asks for a witness and a proof of its instance. The premises help determine which object to use: a universal premise can be instantiated at a useful term, while an existential premise opens a temporary subproof with an unknown witness.

For example, from ∃x∀y R(x,y) we want ∀y∃x R(x,y). Start with the universal goal and take an arbitrary y. The existential premise supplies an unknown x together with ∀y R(x,y). Instantiate that assumption at our chosen y, then use x as the witness for ∃x R(x,y). This conclusion has no free x, so we can close the witness subproof and generalize y. The reverse inference would require one witness that works for every y; separate witnesses do not guarantee that. For a countermodel to the reverse inference, interpret R(x,y) as y < x in the natural numbers, as in our earlier example .

The natural deduction exercises let you construct these proofs, with the quantifier side conditions checked at each step.

The four quantifier rules can be used together with either intuitionistic or classical propositional rules. Here we use the classical rule from Chapter 7 · Logical proofs. One place we need it is the inference from ¬∀x A(x) to ∃x¬A(x).

Assume temporarily that ∃x¬A(x) is false. For an arbitrary x, the assumption ¬A(x) would provide exactly such a witness and lead to a contradiction. Classical reasoning gives A(x). Generalizing gives ∀x A(x), contradicting the premise. A second classical step discharges the temporary assumption and establishes the existential conclusion.

The converse, from ∃x¬A(x) to ¬∀x A(x), needs no classical step: an unknown counterexample contradicts a universal claim instantiated there. Both directions between ¬∃x A(x) and ∀x¬A(x) also have intuitionistic proofs. In the exercises, identify which rule closes each contradiction; negation introduction and the classical rule have different conclusions.

Identity

Chapter 8 · FOL interprets identity (glossary, opens in a new tab) as sameness of domain objects. If a=b and Human(a), then Human(b): the two names denote one object. Reflexivity and substitution express this interpretation in proofs.

Identity introduction infers t=t without premises. Identity elimination infers A[x/t] from s=t and A[x/s], provided both substitutions are free for x in A.

The free-for condition applies to identity substitution too. Suppose we have a = y and ∀y R(a,y). Replacing a directly by y would give ∀y R(y,y), capturing the free variable from the identity. Rename the bound variable first: from ∀z R(a,z) we obtain ∀z R(y,z). The free y continues to denote the object identified with a.

Identity elimination can replace selected occurrences. From a=b and R(a,a), using R(a,x) as the substitution formula gives R(a,b). You can try this in the identity exercises .

With these rules, natural deduction covers FOL with identity. Resolution requires the additional equality rules discussed above. Unification compares syntactic expressions, so distinct constants a and b still fail to unify even when an assumption states a=b.

This is Gödel’s completeness theorem. Every first-order consequence has a proof, but completeness gives us no algorithm that always decides whether a proof exists. This is the distinction between semidecidability and decidability from the opening section .

Lean

We can also write these proofs in Lean, as in Chapter 7 · Logical proofs. There we represented propositions by Lean types in Prop. For FOL we also need a type of objects and predicates on those objects:

variable (Domain : Type)
variable (Human Mortal : Domain → Prop)
variable (Socrates : Domain)

Open this code in L∃∀N (opens in a new tab)

These declarations mirror the semantic values we assign in a structure. Domain represents its domain D; Socrates : Domain supplies the object interpreting the constant Socrates. Human : Domain → Prop represents the predicate interpretation: Human d is the proposition that the object d belongs to its extension. A function symbol would have a declaration such as fatherOf : Domain → Domain, representing its total function on domain objects.

FOL terms are syntactic expressions denoting those objects. The Lean variables here supply their semantic interpretations. A declaration x : Domain gives an object; a declaration hx : Human x gives a proof of a proposition about that object. The quantifier rules use both kinds of declaration.

A binary predicate such as LessThan(x, y) takes two objects. We can supply these one at a time: after choosing x, we have the unary predicate “is greater than x”, waiting for its argument y. For example, fixing x at 3 gives the property of being greater than 3.

This way of representing a function of two arguments is called currying (glossary, opens in a new tab) , after Haskell Curry (opens in a new tab) . The curried function takes the first object and returns a unary function that takes the second. For a predicate R, we therefore write R : Domain → (Domain → Prop). Lean allows us to omit these brackets: R : Domain → Domain → Prop. Given a : Domain, R a is the unary predicate waiting for its second object; R a b supplies that object and expresses the proposition R(a, b).

Let’s use this to express an inference with ∀x∃y R(x,y). If every object is related to some object, then the particular object a is related to some object. With R interpreted as <, this says: if every number has a larger number, then a has a larger number.

variable (Domain : Type)
variable (R : Domain → Domain → Prop) (a : Domain)

example (h : ∀ x, ∃ y, R x y) : ∃ y, R a y := by
  exact h a

Open this code in L∃∀N (opens in a new tab)

Open this code in Lean. The premise h supplies a proof of ∃ y, R x y for any object x; h a supplies it for a. We don’t need to choose the witness ourselves. Try changing the conclusion to ∃ y, ∀ x, R x y: h a no longer proves it. The premise allows a different witness for each object, whereas the changed conclusion requires one witness for them all.

To prove a universal claim, introduce an arbitrary object. To use one, apply its proof to an object. The Socrates proof has two applications:

variable (Domain : Type) (Human Mortal : Domain → Prop)
variable (Socrates : Domain)

example (h : ∀ x, Human x → Mortal x) (hs : Human Socrates) : Mortal Socrates := by
  apply h Socrates
  exact hs

Open this code in L∃∀N (opens in a new tab)

h Socrates has type Human Socrates → Mortal Socrates. Applying that proof to hs gives the conclusion. These are universal and conditional elimination.

For existential elimination, introduce an object and assume that it has the required property. To introduce an existential, give a witness and a proof that the property holds of it:

variable (Domain : Type) (Black White : Domain → Prop)

example (h : ∃ x, Black x) : ∃ x, Black x ∨ White x := by
  apply Exists.elim h
  intro z hz
  apply Exists.intro z
  apply Or.inl
  exact hz

Open this code in L∃∀N (opens in a new tab)

After intro z hz, z : Domain is the unknown witness and hz : Black z is the assumption about it. Exists.intro z leaves the goal Black z ∨ White z. Or.inl selects its left disjunct, which hz proves. The exported conclusion contains no free occurrence of z.

Our FOL models have Chapter 8 · nonempty domains. Lean allows empty types, so Domain : Type alone does not impose this modelling assumption. We supply it with [Inhabited Domain], placed after the domain declaration:

variable (Domain : Type) [Inhabited Domain]
variable (A : Domain → Prop)

example (h : ∀ x, A x) : ∃ x, A x := by
  apply Exists.intro (default : Domain)
  exact h default

Open this code in L∃∀N (opens in a new tab)

[Inhabited Domain] is an assumption supplying a selected object of Domain. Lean retrieves that object with default; (default : Domain) states its type explicitly. We do not need to know which object was supplied. Since h applies to every object, h default proves the required instance. The first command chooses the witness and the second proves that it has A.

This is the convention used in the Lean exercises. It includes a choice of object as well as nonemptiness. The Socrates example already has a named object, and an existential premise supplies a witness inside its subproof; those particular proofs can proceed without using default.

Classical reasoning appears explicitly in Lean as apply Classical.byContradiction. For quantifier duality, we use proof by contradiction twice:

variable (Domain : Type)
variable (A : Domain → Prop)

example (h : ¬∀ x, A x) : ∃ x, ¬A x := by
  apply Classical.byContradiction
  intro hn
  apply h
  intro x
  apply Classical.byContradiction
  intro hx
  apply hn
  apply Exists.intro x
  exact hx

Open this code in L∃∀N (opens in a new tab)

As in Chapter 7 · Logical proofs, open Classical only allows names from that namespace to be written without their prefix. The command classical supplies classical decidability where needed. In this proof, the two applications of Classical.byContradiction identify the classical inferences themselves.

Lean also checks the identity rules. The tactic rfl proves reflexivity:

example (Domain : Type) (a : Domain) : a = a := by
  rfl

Open this code in L∃∀N (opens in a new tab)

Both sides are the same term, so no premise is needed. Eq.subst uses an identity to transport a proof to the corresponding instance:

variable (Domain : Type)
variable (Human : Domain → Prop) (a b : Domain)

example (heq : a = b) (ha : Human a) : Human b := by
  exact Eq.subst heq ha

Open this code in L∃∀N (opens in a new tab)

Curry–Howard

The Curry–Howard correspondence (glossary, opens in a new tab) extends to these quantifier rules. A proof of ∀x A(x) takes an object x and returns a proof of A(x). The return type depends on the input, so this is a dependent function (glossary, opens in a new tab) .

The witness supplied to existential introduction is an object of Domain; the accompanying proof inhabits a proposition about it. Existential elimination opens both parts within a subproof whose conclusion is independent of the witness. Lean’s Exists belongs to Prop, so this logical use of a witness does not provide unrestricted extraction of computational data.

The Lean exercises let you construct quantifier proofs and compare them with the natural deduction rules.

A hybrid AI system can propose proof steps with a learned model and check them with a formal prover. In mathematics, this requires stating the definitions and assumptions on which the proposed theorem depends. Our example with < used ∀x (x < S(x)) as a premise; a checker would need it to justify choosing S(x) as the witness. A checked proof establishes the formal conclusion from the formal assumptions. We must also check that those formulas express the mathematical claim we intended.

Example: Boolean Law

We now know enough Lean to verify a mathematical argument. Take our 13-line derivation of NOT NOT X = X in Chapter 4 · Boolean algebra. An AI could have proposed this argument. We can check that every step is justified by the Boolean laws.

Lean supplies the type Bool and its Boolean operations. Our notation corresponds to Lean as follows:

A Boolean value belongs to Bool; an equation between Boolean values is a proposition in Prop. We state the law with an explicit quantifier: ∀ x : Bool, (!!x) = x.

We can split a proof into subproofs using have. Writing have step_1 : (!!x) = (!!x) := by opens a proof of that identity. The indented rfl proves it. Afterward, step_1 names the result, so later steps can use it. Each numbered subproof below states its identity before proving it; the numbers follow our original derivation.

We use Lean’s Boolean laws (opens in a new tab) by instantiation: Bool.and_true x, for example, proves (x && true) = x. Eq.symm reverses an equality.

Here are the laws from Chapter 4 · Boolean algebra in Lean. The last column gives a proof of the displayed identity for x y z : Bool; use it after exact or as an argument to Eq.subst. Lean states associativity in the reverse direction, so those entries use Eq.symm. For absorption, orAbsorption and andAbsorption are the names of the premises supplied in the verification exercises , not library theorem names.

The derivation below also uses complementation with the negated input first: Bool.not_or_self x proves (!x || x) = true, and Bool.not_and_self x proves (!x && x) = false. In the exercises, use only the laws allowed by the task: quoting the theorem you are asked to derive would skip the argument.

Some steps replace an expression inside AND or OR. We can justify this using the equality rules we already know: if a = b, then f a = f b. Here is the proof for functions on Boolean values:

example (f : Bool → Bool) (a b : Bool) (h : a = b) : f a = f b := by
  apply Eq.subst h
  rfl

Open this code in L∃∀N (opens in a new tab)

apply Eq.subst h reduces the goal f a = f b to f a = f a. Then rfl finishes the proof. This use of substitution is called congruence. Lean’s library supplies the same result under the name congrArg: congrArg f h proves f a = f b. We can use that name because we have just proved the fact it expresses.

For example, Bool.and (!!x) is the function that takes a Boolean value and ANDs it with !!x. Applying congruence to Eq.symm (Bool.or_not_self x) gives ((!!x) && true) = ((!!x) && (x || !x)). In step_3 below, Eq.subst uses this equality to replace the right-hand side of step_2.

example : ∀ x : Bool, (!!x) = x := by
  intro x
  have step_1 : (!!x) = (!!x) := by
    rfl
  have step_2 : (!!x) = ((!!x) && true) := by
    exact Eq.subst (Eq.symm (Bool.and_true (!!x))) step_1
  have step_3 : (!!x) = ((!!x) && (x || !x)) := by
    exact Eq.subst (congrArg (Bool.and (!!x)) (Eq.symm (Bool.or_not_self x))) step_2
  have step_4 : (!!x) = (((!!x) && x) || ((!!x) && !x)) := by
    exact Eq.subst (Bool.and_or_distrib_left (!!x) x (!x)) step_3
  have step_5 : (!!x) = (((!!x) && x) || false) := by
    exact Eq.subst (congrArg (Bool.or ((!!x) && x)) (Bool.not_and_self (!x))) step_4
  have step_6 : (!!x) = ((!!x) && x) := by
    exact Eq.subst (Bool.or_false ((!!x) && x)) step_5
  have step_7 : x = (x && true) := by
    exact Eq.symm (Bool.and_true x)
  have step_8 : x = (x && ((!!x) || !x)) := by
    exact Eq.subst (congrArg (Bool.and x) (Eq.symm (Bool.not_or_self (!x)))) step_7
  have step_9 : x = ((x && (!!x)) || (x && !x)) := by
    exact Eq.subst (Bool.and_or_distrib_left x (!!x) (!x)) step_8
  have step_10 : x = ((x && (!!x)) || false) := by
    exact Eq.subst (congrArg (Bool.or (x && (!!x))) (Bool.and_not_self x)) step_9
  have step_11 : x = (x && (!!x)) := by
    exact Eq.subst (Bool.or_false (x && (!!x))) step_10
  have step_12 : x = ((!!x) && x) := by
    exact Eq.subst (Bool.and_comm x (!!x)) step_11
  have step_13 : (!!x) = x := by
    exact Eq.subst (Eq.symm step_12) step_6
  exact step_13

Open this code in L∃∀N (opens in a new tab)

step_6 and step_12 have the same right-hand side. The final subproof substitutes x for that expression in step_6, giving step_13. exact step_13 finishes the proof. Open the code in Lean and try replacing one Boolean law with an inappropriate one: Lean will reject the step.

Here we have taken a meta-perspective on Boolean logic: we quantify over truth-values and prove an identity between the functions that interpret its connectives. Those truth-values are now the objects of our mathematical argument. Lean makes the move between syntax and semantics explicit through types. It supports valid FOL reasoning within a richer type theory, in which we can also define formal languages, their models, and their proof systems and reason mathematically about them. The same proof-checking machinery applies to other mathematics.

Lean can also find a proof of our law automatically:

example : ∀ x : Bool, (!!x) = x := by simp

Open this code in L∃∀N (opens in a new tab)

The simp tactic uses registered simplification laws to construct a proof, which the kernel checks. Understanding how to guide this automation is a next step in learning Lean. Continue with Theorem Proving in Lean 4 (opens in a new tab) , especially its chapter on tactics (opens in a new tab) . We have seen how inference rules become checked proofs; that gives us a basis for studying Lean’s more powerful methods of finding them.

Further readings

• Russell and Norvig, Artificial Intelligence: A Modern Approach, 4th edition (opens in a new tab) , chapter 9, for unification, chaining, and first-order resolution.
• Richard Zach, Sets, Logic, Computation (PDF) (opens in a new tab) , §§11.3 and 11.6 for quantifier derivations, and chapter 12 for completeness.
• Theorem Proving in Lean 4, Quantifiers and Equality (opens in a new tab) , for dependent functions, existential proofs, and equality in Lean.