SE 500 (Math for SE)   Fall 2024
HW #3: Proofs Involving Equivalence, Negation, and Inequivalence
Due: 5:00pm, Wednesday, Sept. 17

1. In each step in the proof below, Leibniz (often with an assist from Substitution) is applied. That is, in going from each line to the next, some subexpression E is replaced by an expression F such that E = F (or possibly F = E) is an instantiation of (i.e., the conclusion of applying Substitution to) one of the theorems in our arsenal. (That is, E = F (or else F = E) is P[r:=Q], where P is a theorem in our arsenal, r is a list of variables, and Q is a list (of length equal to r) of expressions.)

Here, the only theorems used are axioms (3.1), (3.2), and (3.3). Fill in each "hint" so as to inform the reader which theorem (and which instantiation of it) was used. The first hint is filled in for you. Also, somehow highlight the subexpressions E and F in each step. In the first step below, the former is underlined and the latter is in boldface. 

      (p ≡ q) ≡ (true ≡ (q ≡ r))

   =      < (3.3), with q:=p >

      (p ≡ q) ≡ ((p ≡ p) ≡ (q ≡ r))

   =      <                                                 >

      (p ≡ q) ≡ (p ≡ (p ≡ (q ≡ r)))

   =      <                                                 >

      (p ≡ q) ≡ (p ≡ ((p ≡ q) ≡ r))

   =      <                                                 >

      (p ≡ q) ≡ (((p ≡ q) ≡ r) ≡ p)

   =      <                                                 >

      (p ≡ q) ≡ ((p ≡ q) ≡ (r ≡ p))

   =      <                                                 >

      ((p ≡ q) ≡ (p ≡ q)) ≡ (r ≡ p)

   =      <                                                 >

      true ≡ (r ≡ p)

   =      <                                                 >

      r ≡ p

The remaining problems ask you to prove a theorem. In each case, you are to use only lower-numbered theorems than the one being proved. (For example, to prove Theorem (3.12), you may use only theorems up to (3.11).) Your proofs should follow the Gries & Schneider format, which is to say that they should look like the proof in Problem #1.

Here are the theorems.

2. Do Exercise 3.8, which is to prove Double Negation: (3.12) ¬¬p ≡ p

3. Do Exercise 3.9, which is to prove Negation of false: (3.13) ¬false ≡ true

4. Do an augmented version of Exercise 3.11, which is to prove Theorem (3.15) ¬p ≡ p ≡ false

Prove it in two different ways. As the textbook suggests, one proof should transform ¬p ≡ p ≡ false to true with the help of Theorem (3.11). A second proof should transform ¬p ≡ p to false.

5. On page 47, Gries proves theorem (3.11) (¬p ≡ q ≡ p ≡ ¬q) by showing it to be equivalent to an instance of theorem (3.5) (p ≡ p). Do Exercise 3.7, which is to prove theorem (3.11) in three different ways. Specifically, for each of these, transform the left-hand side into the right-hand side (or vice versa):

  1. (¬p ≡ q) ≡ (p ≡ ¬q)
  2. (¬p ≡ p) ≡ (q ≡ ¬q) (which is obtained from (3.11) by applying (3.2))
  3. ¬p ≡ (q ≡ p ≡ ¬q)
6. Do Exercise 3.13, which is to prove mutual associativity of ≡ and ≠ (3.18):

(3.18) ((p ≠ q) ≡ r) ≡ (p ≠ (q ≡ r))

using the heuristic of Definition Elimination (3.23).