5. Formal Proofs

We introduce in this lecture an alternative method for verifying the validity of logical arguments: formal proof systems.

In a formal proof system, we do not refer to any truth tables. Instead, we define a number of deduction rules. And we say that a set \(\Gamma\) of premises implies the conclusion \(\phi\), written symbolically as

if we can obtain \(\phi\) with a finite number of applications of the deduction rules with this set of premises.

In the special case where we can imply \(\phi\) from the empty set of premises, we write

and call \(\phi\) a theorem.

In order to determine when we have \(\Gamma \vdash \phi\), we must determine the set of rules that form valid arguments. Such a set of rules is a formal deduction system. There are many such systems. The one we introduce below is a type of natural deduction system.

A Natural Deduction System

In our natural deduction system, a proof is a sequence of lines. Each line has three elements: its line number, a formula, and a justification. A full proof in this system looks like this:

Claim. \(\{ (p \wedge (q \vee r)) \} \vdash ((p \wedge q) \vee (p \wedge r))\).

Formal proof.

 1. (p⋀(q⋁r))          PR
 2. p                  ⋀E 1
 3. (q⋁r)              ⋀E 1
 4. ⎡ q                AS
 5. ⎜ (p⋀q)            ⋀I 2, 4
 6. ⎣ ((p⋀q)⋁(p⋀r))    ⋁I 5
 7. ⎡ r                AS
 8. ⎜ (p⋀r)            ⋀I 2, 7
 9. ⎣ ((p⋀q)⋁(p⋀r))    ⋁I 8
10. ((p⋀q)⋁(p⋀r))      ⋁E 3, 4-6, 7-9

We will go over the formal definitions of all the parts of this formal proof in the next subsections. But before we do so, you may already notice that the proof above is quite similar to how we would prove the same claim in plain English:

Claim. Whenever the formula \((p \wedge (q \vee r))\) is satisfied, then so is \((p \wedge q) \vee (p \wedge r))\).

Proof. Fix any truth assignment to \(p,q,r\) for which \((p \wedge (q \vee r))\) is True.

By the definition of the \(\wedge\) connective, when \((p \wedge (q \vee r))\) is True, then \(p\) and \((q \vee r)\) must also both be True.

Consider now two cases:

• Assume $q$ is True. We already know that \(p\) must be True, so \((p \wedge q)\) is also True. In turn, this means that \(((p \wedge q) \vee \psi)\) is True for any formula \(\psi\). In particular, it means that \(((p \wedge q) \vee (p \wedge r))\) is True.

• Assume r is True. As above, we know in this case that \((p \wedge r)\) is True and that for any formula \(\phi\), \((\phi \vee (p \wedge r))\) is True. Therefore, \(((p \wedge q) \vee (p \wedge r))\) is True.

We know that \((q \vee r)\) is True. Therefore, at least one of $q$ or $r$ must be True. And as we just saw, in either case \(((p \wedge q) \vee (p \wedge r))\) is True.

The similarity between the formal proof and the informal one is the reason why the formal proof system we introduce is called a natural deduction system: this system aims to let us write proofs that mimic our natural (informal) reasoning as closely as possible.

The Deduction Rules

Each line in a formal proof must use one of the following derivation rules.

Elementary rules

There are two elementary rules that we can always use in a proof.

The first is the premise rule that lets us state any premise of our argument in any line of the proof. We write PR to any line that applies this rule.

Premise rule. For any premise \(\phi \in \Gamma\), we can add the line

   n. 𝜑           PR

The premise rule is the one we used in the first line of the example above. More generally, we can apply this line at any point in a proof.

Another very basic rule is re-iteration, where we simply repeat a line that occurred earlier in the proof. We write R m as the justification for lines that use this rule, replacing m with the number of the line being re-iterated.

Re-iteration rule. For any formula \(\phi\) that appears in the \(m\)th line in the proof, we can re-iterate it on line \(n > m\):

   m. 𝜑
   ⋮
   n. 𝜑                  R m

Conjunction rules

When \(\phi\) and \(\psi\) are two formulas that appear in the proof, we can use the conjunction introduction rule to add the formula \((\phi \wedge \psi)\) to the proof. The justification for this rule is ⋀I k, l where k and l are replaced with the lines of the two formulas that we AND together.

Conjunction Introduction. For any formulas \(\phi\) and \(\psi\) that appear in the proof, we can add the formula \((\phi \wedge \psi)\) to the proof:

   k. 𝜑
   l. 𝜓
   ⋮
   n. (𝜑 ⋀ 𝜓)            ⋀I k, l

In the other direction, when \((\phi \wedge \psi)\) appears in the proof, we can use conjunction elimination to add \(\phi\) or \(\psi\) to the proof. We write ⋀E m as justification when we use this rule with the conjunction at line m.

Conjunction elimination. For any formulas \(\phi\) and \(\psi\), when \((\phi \wedge \psi)\) appears in the proof, we can add \(\phi\) to the proof:

   m. (𝜑 ⋀ 𝜓) 
   ⋮
   n. 𝜑                   ⋀E m

and we can also add \(\psi\) to the proof:

   m. (𝜑 ⋀ 𝜓) 
   ⋮
   n. 𝜓                   ⋀E m

Note that the same line m with formula \((\phi \wedge \psi)\) can be used to justify two separate applications of the conjunction elimination rule when we want to add both \(\phi\) and \(\psi\) to the proof. Indeed, this is what we did in lines 2 and 3 of the example proof in the previous section.

Disjunction rules

The disjunction introduction rule is simple: whenever \(\phi\) appears in the proof, we can always add \((\phi \vee \psi)\) or \((\psi \vee \phi)\) to the proof as well. We write ⋁I m as justification for this rule when \(\phi\) appears at line m.

Disjunction introduction. For any formula \(\phi\) that appears in the proof and any formula \(\psi\), we can add \((\phi \vee \psi)\) to the proof:

   m. 𝜑
   ⋮
   n. (𝜑 ⋁ 𝜓)           ⋁I m

and we can add \((\psi \vee \phi)\) to the proof:

   m. 𝜑
   ⋮
   n. (𝜓 ⋁ 𝜑)           ⋁I m

The disjunction elimination rule is a bit more involved. This rule is applicable in a setting where we know three things:

• \((\phi \vee \psi)\) is true.
• If \(\phi\) is true, then so is \(\theta\).
• If \(\psi\) is true, then so is \(\theta\).

In this setting, we know that \(\theta\) must be true. But to define a rule that captures this logic, we need to introduce the idea of subproofs.

Definition. A subproof is a consecutive set of lines of a proof that satisfies the following conditions:

• The first line of a subproof is called its assumption. It can contain any formula and is annotated with AS.
• The last line of a subproof is called its conclusion.
• Lines that appear after the end of the subproof can refer to the subproof as a whole in their justification (as we see in specific rules below) but cannot use individual lines of the subproof as justifications.

When writing subproofs, we clearly demark their start and end points using indentation and additional notation. In the Quick Reference Guide, we use boxes to do so. On this page, we use plain-text square brackets to suggest similar boxes. Other resources use slightly different notation, sometimes with vertical lines and horizontal lines under the assumption.

Disjunction elimination. For any formulas \(\phi\), \(\psi\), and \(\theta\), when \((\phi \vee \psi)\) is in the proof and there are two subproofs with assumptions \(\phi\) and \(\psi\), respectively, and conclusion \(\theta\), then we can add \(\theta\) to the proof:

   i. (𝜑 ⋁ 𝜓) 
   j. ⎡ 𝜑                   AS
   k. ⎣ 𝜃
   l. ⎡ 𝜓                   AS
   m. ⎣ 𝜃
   ⋮
   n. 𝜃                     ⋁E i, j-k, l-m

Negation and contradiction rules

The rules for negation require the introduction of a new symbol: \(\bot\) is a special formula symbol that we will use to represent a contradiction.

The basic rule for contradictions is that every formula can be derived from them.

Contradiction elimination. If \(\bot\) appears in the proof, we can add any formula \(\phi\) to the proof:

   m. ⊥
   ⋮
   n. 𝜑                  ⊥E m

If both \(\phi\) and \(\neg \phi\) appear in the proof, we have a contradiction and we can represent this in the proof by using the negation elimination rule to add \(\bot\) to the proof. The use of the negation elimination rule is justified by ¬E k, l where k is the line number where \(\phi\) appears and l is the number of the line containing \(\neg \phi\).

Negation elimination. For any formula \(\phi\) where both \(\phi\) and its negation \(\neg \phi\) appear in the proof, we can add the contradiction \(\bot\) to the proof:

   k. 𝜑
   l. ¬𝜑
   ⋮
   n. ⊥                  ¬E k, l

The negation introduction rule, also known as proof by contradiction can be used to add \(\neg \phi\) to a proof if we have a subproof showing that the assumption \(\phi\) leads to the contradiction \(\bot\). We write ¬I k-l to justify the use of the rule when the subproof leading to contradiction is from line k to line l.

Negation introduction. For any formula \(\phi\), if we have a subproof with assumption \(\phi\) and conclusion \(\bot\), then we can add \(\neg \phi\) to the proof:

   k. ⎡ 𝜑                    AS
   l. ⎣ ⊥
   ⋮
   n. ¬𝜑                     ¬I k-l

Another rule that is closely related is reductio ad absurdum:

Reductio ad absurdum. For any formula \(\phi\), if we have a subproof with assumption \(\neg \phi\) and conclusion \(\bot\), then we can add \(\phi\) to the proof:

   k. ⎡ ¬𝜑                    AS
   l. ⎣ ⊥
   ⋮
   n. 𝜑                       RAA k-l

Conditional rules

When \((\phi \to \psi)\) and \(\phi\) both are known to be true, then we can conclude that \(\psi\) is also true. This deduction rule is known as modus ponens, but for consistency with the notation above, we also call it conditional elimination and use the justification →E when we apply this rule.

Conditional elimination. When \((\phi \to \psi)\) and \(\phi\) both appear in the proof, then we can add \(\psi\) to the proof as well:

   k. (𝜑 → 𝜓)
   l. 𝜑
   ⋮
   n. 𝜓                       →E k, l

When we have a subproof with assumption \(\phi\) and conclusion \(\psi\), we can add the formula \((\phi \to \psi)\) to the proof. This operation is known as discharging the assumption. We call the rule which performs this operation the conditional introduction rule.

Conditional introduction. When there is a subproof with assumption \(\phi\) and conclusion \(\psi\) in the proof, we can add the formula \((\phi \to \psi)\) to the proof:

   k. ⎡ 𝜑                     AS
   l. ⎣ 𝜓
   ⋮
   n. (𝜑 → 𝜓)                 →I k-l

Biconditional rules

The formula \((\phi \leftrightarrow \psi)\) is true if and only if \((\phi \to \psi)\) and \((\psi \to \phi)\) are both true. We can use this identity to introduce biconditional formulas in a proof.

Biconditional introduction. When \((\phi \to \psi)\) and \((\psi \to \phi)\) both appear in a proof, we can add the formula \((\phi \leftrightarrow \psi)\) as well:

   k. (𝜑 → 𝜓)
   l. (𝜓 → 𝜑)
   ⋮
   n. (𝜑 ↔︎ 𝜓)                ↔︎I k, l

And we can use the same identity to eliminate biconditional formulas.

Biconditional elimination. When \((\phi \leftrightarrow \psi)\) appears in a proof, we can add the formula \((\phi \to \psi)\) to the proof:

   m. (𝜑 ↔︎ 𝜓)
   ⋮
   n. (𝜑 → 𝜓)                ↔︎E m

and we can add the formula \((\psi \to \phi)\) as well:

   m. (𝜑 ↔︎ 𝜓)
   ⋮
   n. (𝜓 → 𝜑)                ↔︎E m

Summary

The rules described above are all the basic rules that we need to completely define our proof system. For reference, here is the list of all line justification labels and the associated deduction rule:

• PR: Premise statement
• R: Re-iteration
• AS: Assumption statement (in subproofs)
• ⋀I: Conjunction introduction
• ⋀E: Conjunction elimination
• ⋁I: Disjunction introduction
• ⋁E: Disjunction elimination (Proof by cases)
• ⊥E: Contradiction elimination
• ¬I: Negation introduction (Proof by contradiction)
• ¬E: Negation elimination
• RAA: Reductio ad absurdum
• →I: Conditional introduction (Discharging the assumption)
• →E: Conditional elimination (Modus ponens)
• ↔︎I: Biconditional introduction
• ↔︎E: Biconditional elimination

See also this Quick Reference Guide for a compact summary of the rules described above.

With the basic rules in place, we can define what it means for a set of premises to formally imply a conclusion:

Definition. The set \(\Gamma\) of formulas implies the formula \(\phi\), denoted

\[\Gamma \vdash \phi\]

if and only if there is a formal proof with a finite number of lines where:

• each line is obtained by applying one of the basic rules listed above,
• all of the formulas in PR lines are in \(\Gamma\), and
• the last line of the proof is \(\phi\) and is not contained in a subproof.

In the next lecture, we work through some examples of formal proofs in this system. The following lectures then establish some fundamental properties of this proof system that relate it back to the notion of logical consequence we covered previously.