Proving Similar Statements Using Proof Alteration

[mXSCNT]

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.

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)

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:

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)

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.

 

[mmwave]

This slight alteration allows the proof to still follow the same logical structure and rules, but with different premises and conclusion.

In general, a computer can alter a formal proof by substituting different logical statements or symbols, using different logical rules or axioms, or rearranging the steps of the proof to fit a different structure. However, it is important to note that the computer must be programmed with the necessary knowledge and understanding of logical rules and principles in order to make these alterations accurately and effectively. Additionally, the computer may also need to be able to recognize patterns and similarities between statements in order to make the appropriate changes.