- #1

- 315

- 1

Suppose you have a formal proof of a statement S, but you want to prove a statement S' which is in some way similar to S. The question is, how might a computer slightly alter the proof of S in such a way that it becomes a proof of S'?

Here's an example (using v for disjunction, n for conjunction). Skip it if you find it tedious.

Now suppose that instead of S = ((A v B) n C) -> (((A v B) v (A v B)) n C), we wanted to prove S' = (~(A n B) n C) -> (((~A v ~B) v D) n C). This could be done as follows:

The proof for S' has been derived from the proof for S, by replacing the premise (A v B) n C with the premise ~(A n B) n C, applying DeMorgan's rule after step 2, and introducing D instead of (A v B) in the disjunction introduction.

Here's an example (using v for disjunction, n for conjunction). Skip it if you find it tedious.

Code:

```
1. (A v B) n C (assume.)
| 2. (A v B) (1, conjunction elimination)
| 3. (A v B) v (A v B) (2, disjunction introduction)
| 4. C (1, conjunction elimination)
| 5. ((A v B) v (A v B)) n C (3,4, conjunction introduction)
6. ((A v B) n C) -> (((A v B) v (A v B)) n C) (1,5,conditional proof)
```

Code:

```
1. ~(A n B) n C (assume.)
| 2. ~(A n B) (1, conjunction elimination)
| 3. ~A v ~B (2, DeMorgan)
| 4. (~A v ~B) v D (3, disjunction introduction)
| 5. C (1, conjunction elimination)
| 6. ((~A v ~B) v D) n C (4,5, conjunction introduction)
7. (~(A n B) n C) -> (((~A v ~B) v D) n C) (1,6,conditional proof)
```

Last edited: