6. Examples of Formal Proofs

We continue our exploration of the formal proof system introduced in the previous lecture by looking at some examples.

First Examples

We begin with some simple examples, in the sense that all of the formal proofs of the claims in this section are short. But a quick word of warning: they are not all easy!

Commutativity

We can establish the commutativity of conjunctions with a simple proof.

Claim 1. \(\{ (p \wedge q) \} \vdash (q \wedge p)\).

Proof.

  1. (p⋀q)        PR
  2. p            ⋀E 1
  3. q            ⋀E 1
  4. (q⋀p)        ⋀I 3, 2

The proof of the commutativity of biconditionals is just as simple.

Claim 2. \(\{ (p \leftrightarrow q) \} \vdash (q \leftrightarrow p)\).

Proof.

  1. (p↔︎q)        PR
  2. (p→q)        ↔︎E 1
  3. (q→p)        ↔︎E 1
  4. (q↔︎p)        ↔︎I 3, 2

Disjunctions are also commutative, but the proof of that fact is a little bit longer.

Claim 3. \(\{ (p \vee q) \} \vdash (q \vee p)\).

Proof.

  1. (p⋁q)        PR
  2. ⎡ p          AS
  3. ⎣ (q⋁p)      ⋁I 2
  4. ⎡ q          AS
  5. ⎣ (q⋁p)      ⋁I 4
  6. (q⋁p)        ⋁E 1, 2-3, 4-5

Proofs with conditionals

The conditional connective is not commutative but it is transitive.

Claim 4. \(\{ (p \to q), (q \to r) \} \vdash (p \to r)\).

Proof.

  1. (p→q)        PR
  2. (q→r)        PR
  3. ⎡ p          AS
  4. ⎢ q          →E 1, 3
  5. ⎣ r          →E 2, 4
  6. (p→r)        →I 3-5

Another basic property of the conditional connective is in the claim below. Note that the proof of this claim uses nested subproofs.

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

Proof.

  1. ((p⋀q)→r)    PR
  2. ⎡ p          AS
  3. ⎢ ⎡ q        AS
  4. ⎢ ⎢ (p⋀q)    ⋀I 2, 3
  5. ⎢ ⎣ r        →E 1, 4
  6. ⎣ (q→r)      →I 3-5
  7. (p→(q→r))    →I 2-6

Proofs with negation

Let’s examine the negation connective. In our proof system, we can show that \(p \equiv \neg \neg p\). We start with one direction:

Claim 6. \(\{ p \} \vdash \neg \neg p\).

Proof.

  1. p            PR
  2. ⎡ ¬p         AS
  3. ⎣ ⊥          ¬E 2, 1
  4. ¬¬p          ¬I 2-3

For the other direction, the proof is similar but differs in one important respect:

Claim 7. \(\{ \neg \neg p\} \vdash p\).

Proof.

  1. ¬¬p          PR
  2. ⎡ ¬p         AS
  3. ⎣ ⊥          ¬E 2, 1
  4. p            RAA 2-3

The following claim also has a short proof when we take advantage of a rule that we have not yet used above.

Claim 8. \(\{ \neg p \} \vdash (p \to q)\).

Proof.

  1. ¬p           PR
  2. ⎡ p          AS
  3. ⎢ ⊥          ¬E 2, 1
  4. ⎣ q          ⊥E 3
  5. (p→q)        →I 2-4

And some of the facts about negation that we can prove may look a bit surprising:

Claim 9. \(\{ (p \to \neg p) \} \vdash \neg p\).

Proof.

  1. (p→¬p)        PR
  2. ⎡ p           AS
  3. ⎢ ¬p          →E 1, 2
  4. ⎣ ⊥           ¬E 2, 3
  5. ¬p            ¬I 2-4

Derived Rules

There are a number of deduction rules that are commonly used in propositional logic and that have been studied extensively. We explore four of them, and show how they can be derived from our basic deduction rules.

Modus Tollens

Recall that modus ponens is equivalent to the conditional elimination (\(\to\)E) rule: if we know that \((p\to q)\) and \(p\) both hold, then we know that \(q\) must hold. Modus tollens is the closely related deduction showing that if \((p \to q)\) and \(\neg q\) both hold, then we must also have \(\neg p\).

Claim 10. \(\{ (p \to q), \neg q\} \vdash \neg p\).

Proof.

  1. (p→q)         PR
  2. ¬q            PR
  3. ⎡ p           AS
  4. ⎢ q           →E 1, 3
  5. ⎣ ⊥           ¬E 4, 2
  6. ¬p            ¬I 3-5

Law of the Excluded Middle

The law of the excluded middle states that for any proposition \(p\), it must be the case that \(p\) or \(\neg p\) is True. We can give a formal proof of this law.

Claim 11. \(\vdash (p \vee \neg p)\).

Proof.

  1. ⎡ ¬(p⋁¬p)      AS
  2. ⎢ ⎡ p          AS
  3. ⎢ ⎢ (p⋁¬p)     ⋁I 2
  4. ⎢ ⎣ ⊥          ¬E 3, 1
  5. ⎢ ¬p           ¬I 2-4
  6. ⎢ (p⋁¬p)       ⋁I 5
  7. ⎣ ⊥            ¬E 6, 1
  8. (p⋁¬p)         RAA 1-7

Disjunctive Syllogism

Another common deduction rule used in logical arguments is known as disjunctive syllogism. It states that if we know that \((p \vee q)\) is True and we know that \(p\) is False, then we must have that \(q\) is True.

Claim 12. \(\{ (p \vee q), \neg p \} \vdash q\).

Proof.

  1. (p⋁q)      PR
  2. ¬p         PR
  3. ⎡ p        AS
  4. ⎢ ⊥        ¬E 3, 2
  5. ⎣ q        ⊥E 4
  6. ⎡ q        AS
  7. ⎣ q        R 6
  8. q          ⋁E 1, 3-5, 6-7

De Morgan’s Laws

De Morgan’s Laws can be used to manipulate the position of negations inside formulas. We can establish these laws with formal proofs. Here is one such example:

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

Proof.

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