12. Formal Proofs in First-Order Logic

We can extend the natural deduction system that we introduced in propositional logic to obtain a formal proof system for first-order logic.

Natural Deduction in First-Order Logic

The formal proofs in first-order logic are an extension of the natural deduction system we introduced in propositional logic. A proof is a finite list of formulas, each accompanied by a justification that uses one of the basic rules of the deduction system. When we have a formal proof whose premises are all in $\Gamma$ and whose final line has the sentence $\phi$ and is not contained in a subproof, we write

\[\Gamma \vdash \phi,\]

as we did in propositional logic.

The basic rules introduced in the propositional logic proof system are also basic rules in the first-order logic proof system. In the following section, we introduce a few additional rules to handle the quantifiers and the identity relation. Before we introduce these rules, however, we must revisit the notion of substitution in formulas.

For any formula $\phi$, variable $v$, and term $t$, the substitution of $v$ with $t$ in $\phi$ is the formula

\[\phi[v/t]\]

obtained by replacing every free instance of $v$ in $\phi$ with the term $t$. (In lecture 10, we already saw a similar notion of replacement when we specified how to evaluate formulas that contain quantifiers, though the definition here is purely syntactic: we will use it in formal proofs, not to evaluate formulas.)

Similarly, for any formula $\phi$ and terms $t$ and $u$, a partial substitution of $t$ with $u$ in $\phi$ is a formula

\[\phi[t/^*u]\]

obtained by replacing some (or none, or all) of the instances of $t$ in $\phi$ with $u$.

The First-Order Logic Deduction Rules

As mentioned above, all the basic rules of the deduction system for propositional logic are also basic rules for the first-order logic formal deduction system. We also introduce six additional rules to handle the $\forall$ and $\exists$ quantifiers and the $=$ predicate.

Universal Quantifier Rules

The Universal Elimination rule ∀E lets us replace the variable $x$ with the name of any other element of the domain in a $\forall x \phi$ formula.

Universal Elimination rule. When $\forall x \phi$ appears in the proof and $t$ is any term that does not contain any variable which become bound when it is substituted into $\phi$, we can eliminate the $\forall$ quantifier using substitution:
   m. ∀x 𝜑
   ⋮
   n. 𝜑[x/t]                  ∀E m

Note that the Universal Elimination rule can be justified with the formula on line $m$ when the eliminated quantifier is the outermost operator in the sentence. For example, we can not perform universal elimination on $(\forall x \phi \vee \psi)$ or on the $\forall y$ quantifier in $\forall x \forall y \phi$.

The Universal Introduction rule can be thought as the inverse of the Universal Elimination rule: if $\phi$ is a formula that includes a free variable $v$ that that does not occur in any premise or undischarged assumption, then $\forall x \phi{[v/x]}$ holds.

Universal Introduction rule. When $\phi$ appears in the proof and contains a free variable $v$ that does not appear in the premises or undischarged assumption, we can introduce the $\forall$ quantifier:
   m. 𝜑
   ⋮
   n. ∀x 𝜑[v/x]                  ∀I m

Existential Quantifier Rules

When $\phi$ is a sentence that includes the element name $a$ and evaluates to True in a structure, we know that there must be an element in the domain of this structure that causes $\phi$ to evaluate to True. The Existential Introduction rule implements this observation in the formal proof system.

Existential Introduction rule. When $\phi$ appears in the proof, $t$ is a term in $\phi$, and $x$ is a variable that does not appear in $\phi$, we can introduce the $\exists$ quantifier:
   m. 𝜑
   ⋮
   n. ∃x 𝜑[t/*x]                  ∃I m

The Existential Elimination rule can be viewed as a variant of the ⋁E rule. Both proceed by case analysis and show that if all cases lead to the same conclusion, we can apply the corresponding elimination rule. For the ∃E rule, all the cases are handled simultaneously in a single subproof.

Existential Elimination rule. When $v$ is a variable that does not appear in $\phi$, then we can eliminate an existential quantifier:
   i. ∃x 𝜑
   j. ⎡ 𝜑[x/v]           AS
      ⎢ ⋮
   k. ⎣ 𝜓
   ⋮
   n. 𝜓                  ∃E i, j-k 

Identity Rules

At any line in the proof, we can add an identity of any element to itself.

Identity Introduction rule. At any line in the proof, we can always add an identity from a term $t$ to itself:
    n. t = t               =I

When we have an identity $t=u$ between two terms $t$ and $u$, we can replace any instance of $t$ with $u$ or any instance of $u$ with $t$ in any formula $\phi$ that contains either of these terms. This rule is known as Identity Elimination.

Identity Elimination rule. For any terms $t$ and $u$ and any formula $\phi$,
   k. t=u
   l. 𝜑
   ⋮
   n. 𝜑[t/*u]               =E k, l
and
   k. t=u
   l. 𝜑
   ⋮
   n. 𝜑[u/*t]               =E k, l

The Identity Elimination rule is also known as Leibniz’s Law.

A First Proof

We can derive De Morgan’s Rules for quantifiers within our formal proof system.

Theorem. (De Morgan’s Laws)
\[\begin{align*} \forall x \neg \phi &\vdash \neg \exists x \phi, \\ \exists x \neg \phi &\vdash \neg \forall x \phi, \\ \neg \forall x \phi &\vdash \exists x \neg \phi, \mbox{ and} \\ \neg \exists x \neg \phi &\vdash \forall x \neg \phi. \end{align*}\]

Proof. Here is a proof of the first implication.

∀x ¬𝜑                   PR
⎡ ∃x 𝜑                  AS
⎢⎡ 𝜑[x/a]               AS
⎢⎢ ¬𝜑[x/a]              ∀E 1
⎢⎣ ⊥                    ¬E 3, 4
⎣ ⊥                     ∃E 2, 3-5
¬∃x 𝜑                   ¬I 2-6

The other three proofs are left as exercises.