Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Proof Alteration

  1. May 16, 2009 #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.
    Code (Text):

    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:
    Code (Text):

    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.
    Last edited: May 16, 2009
  2. jcsd
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook

Can you offer guidance or do you also need help?
Draft saved Draft deleted