# Posts Tagged ‘Lemma’

## Axiomatic Proof of Modus Ponens

Posted by allzermalmer on November 22, 2013

Here is a proof of Modus Ponens. This proof will use Polish Notation, relies on three axioms & one rule of inference. The proof for Modus Ponens will rely on 13 Lemmas. This axiomatic system only has two primitive logical operators, which is C and N, or Implication and Negation.

A quick note on notation.
C stands for implication, i.e. –>
N stand for negation, i.e. ~

Axiom 1: CCpqCCqrCpr [Hypothetical Syllogism]
Axiom 2: CCNppp [Clavis Law, i.e. Reductio Ad Absurdum]
Axiom 3: CpCNpq [Dun Scotus Law, i.e. Law of Denying Antecedent]

Inference Rule:
Rule of Detachment (MP): Φ & CΦΩ implies Ω

Lemma 4: CCCCqrCprsCCpqs

1.            CCpqCCqrCpr [sub. p/Cpq, q/CCqrCpr, r/s in Axiom 1]

2.            CCCpqCCqrCprCCCCqrCprsCCpqs

3.            CCCCqrCprsCCpqs [(1)/(2) MP] Q.E.D.

Lemma 5: CCpCqrCCsqCpCsr

1.            CCCCqrCprsCCpqs [sub. q/Cqr, r/Csr, s/CCsqCpCsr in L4]

2.            CCCCCqrCsrCpCsrCCsqCpCsrCCpCqrCCsqCpCsr

3.            CCCCqrCprsCCpqs [sub. p/s, s/CpCsr in L4]

4.            CCCCCqrCsrCpCsrCCsqCpCsr

5.            CCpCqrCCsqCpCsr [(2)/(4) MP] Q.E.D.

Lemma 6: CCpqCCCprsCCqrs

1.            CCCCqrCprsCCpqs [sub. s/CCCprsCCqrs in L4]

2.            CCCCqrCprCCCprsCCqrsCCpqCCCprsCCqrs

3.            CCpqCCqrCpr [sub. p/Cqr, q/Cpr, r/s in Axiom 1]

4.            CCCqrCprCCCprsCCqrs

5.            CCpqCCCprsCCqrs [(2)/(4) MP] Q.E.D.

Lemma 7: CCtCCprsCCpqCtCCqrs

1.            CCpCqrCCsqCpCsr [sub. p/Cpq, q/CCprs, r/CCqrs, s/t in L5]

2.            CCCpqCCCprsCCqrsCCtCCprsCCpqCtCCqrs

3.            CCtCCprsCCpqCtCCqrs [(2)/(L6) MP] Q.E.D.

Lemma 9: CCCNpqrCpr

1.            CCpqCCqrCpr [sub. q/CNpq in Axiom 1]

2.            CCpCNpqCCCNpqrCpr

3.            CCCNpqrCpr [(2)/(Axiom 3) MP] Q.E.D.

Lemma 10: CpCCCNpppCCqpp

1.            CCCNpqrCpr [sub. r/CCCNpppCCqpp in L9]

2.            CCCNpqCCCNpppCCqppCpCCCNpppCCqpp

3.            CCpqCCCprsCCqrs [sub. p/Np, r/p, s/p in L6]

4.            CCNpqCCCNpppCCqpp

5.            CpCCCNpppCqpp [(2)/(4) MP] Q.E.D.

Lemma 11: CCqCCNpppCCNppp

1.            CpCCCNpppCCqpp [sub. p/CCNppp in L10]

2.            CCCNpppCCCNpCCNpppCCNpppCCqCCNpppCCNppp

3.            CCCNpCCNpppCCNpppCCqCCNpppCCNppp [(2)/(Axiom 2) MP]

4.            CCNppp [sub. p/CCNppp in Axiom 2]

5.            CCNpCCNpppCCNppp

6.            CCqCCNpppCCNppp [(3)/(5) MP] Q.E.D.

Lemma 12: CtCCNppp

1.            CCCNpqrCpr [sub. p/t, q/CCNppp, r/CCNppp in L9]]

2.            CCCNtCCNpppCCNpppCtCCNppp

3.            CCqCCNpppCCNppp [sub. q/Nt, in L11]

4.            CCNtCCNpppCCNppp

5.            CtCCNppp [(2)/(4) MP] Q.E.D.

Lemma 13: CCNpqCtCCqpp

1.            CCtCCprsCCpqCtCCqrs [sub. p/Np, r/p, s/p in L7]

2.            CCtCCNpppCCNpqCtCCtCCqpp

3.            CCNpqCtCCqpp [(2)/(L12) MP] Q.E.D.

Lemma 14: CCCtCCqpprCCNpqr

1.            CCpqCCqrCpr [sub. p/CNpq, q/CtCCqpp in Axiom 1]

2.            CCCNpqCtCCqppCCCtCCqpprCNpqr

3.            CCCtCCqpprCNpqr [(2)/(L13) MP] Q.E.D.

Lemma 15: CCNpqCCqpp

1.            CCCtCCqpprCCNpqr [sub. t/NCCqpp, r/Cqpp in L14]

2.            CCCNCCqppCCqppCCqppCCNpqCCqpp

3.            CCNppp [sub. p/CCqpp in Axiom 2]

4.            CCNCCqppCCqppCCqpp

5.            CCNpqCCqpp [(2)/(4) MP] Q.E.D.

Lemma 17: CpCCqpp

1.            CCCNpqrCpr [sub. r/CCqpp in L9]

2.            CCCNpqCCqppCpCCqpp

3.            CpCCqpp [(2)/(L15) MP] Q.E.D.

Lemma 18: CqCpq [Law of Affirming Consequent/Law of Simplification]

1.            CCpCqrCCsqCpCsr [sub. p/q, q/CNpq, r/q, s/p in L5]

2.            CCqCCNpqqCCpCNpqCqCpq

3.            CpCCqpp [sub. p/q, q/Np in L17]

4.            CqCCNpqq

5.            CCpCNpqCqCpq [(2)/(4) MP]

6.            CqCpq [(5)/(Axiom 3) MP] Q.E.D.

Lemma 19: CCCpqrCqr

1.            CCpqCCqrCpr [sub. p/q, q/Cpq in Axiom 1]

2.            CCqCpqCCCpqrCqr

3.            CCCpqrCqr [(2)/(L18) MP] Q.E.D.

Modus Ponens: CpCCpqq

1.            CCCpqrCqr [sub. p/Nq, q/p, r/ CCpqq in L19]

2.            CCCNqpCCpqqCpCCpqq

3.            CCNpqCCqpp [sub. p/q, q/p in L15]

4.            CCNqpCCpqq

5.            CpCCpqq [(2)/(4) MP] Q.E.D.

Axiomatic Proof of Modus Ponens using standard notation

Axiom 1: (P–>Q)–>((Q–>R)–>(P–>R))
Axiom 2: ~P–>(P–>P)
Axiom 3: P–>(~P–>Q)

Lemma 4: ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S))

1. (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/(P–>Q), Q/((Q–>R)–>(P–>R)), R/S in Axiom 1]
2. ((P–>Q)–>((Q–>R)–>(P–>R)))–>((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S))
3. ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [(1)/(2) MP] Q.E.D.

Lemma 5: ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R))))

1. ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. Q/ (Q–>R), R/(S–>R), S/((S–>Q)–>(P–>(S–>R))) L4]
2. (((((Q–>R)–>(S–>R))–>(P–>(S–>R)))–>((S–>Q)–>(P–>(S–>R))))–>((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))))
3. ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. P/S, S/ (P–>(S–>R)) in L4]
4. ((((Q–>R)–>(S–>R))–>(P–>(S–>R)))–>((S–>Q)–>(P–>(S–>R))))
5. ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [(2)/(4) MP] Q.E.D.

Lemma 6: ((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S)))

1. ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. s/ (((P–>R)–>S)–>((Q–>R)–>S)) in L4]
2. ((((Q–>R)–>(P–>R))–>(((P–>R)–>S)–>((Q–>R)–>S)))–>((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S))))
3. (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/ (Q–>R), Q/ (P–>R), R/S in Axiom 1]
4. ((Q–>R)–>(P–>R))–>(((P–>R)–>S)–>((Q–>R)–>S))
5. ((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S))) [(2)/(4) MP] Q.E.D.

Lemma 7: (T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S)))

1. ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [sub. P/ (P–>Q), Q/ ((P–>R)–>S), R/ ((Q–>R)–>S), S/T in L5]
2. (((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S)))–>((T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S)))))
3. (T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S))) [(2)/(L6) MP] Q.E.D.

Lemma 9: (((~P–>Q)–>R)–>(P–>R))

1. (P–>Q)–>((Q–>R)–>(P–>R)) [sub. Q/(~P–>Q) in Axiom 1]
2. (P–>(~P–>Q))–>(((~P–>Q)–>R)–>(P–>R))
3. (((~P–>Q)–>R)–>(P–>R)) [(2)/Axiom 3 MP] Q.E.D.

Lemma 10:  (P–>(((~P–>P)–>P)–>((Q–>P)–>P)))

1. (((~P–>Q)–>R)–>(P–>R)) [sub. R/ (((~P–>P)–>P)–>((Q–>P)–>P)) in L9]
2. (((~P–>Q)–>(((~P–>P)–>P)–>((Q–>P)–>P)))–>(P–>(((~P–>P)–>P)–>((Q–>P)–>P))))
3. ((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S))) [sub. P/~P, R/P, S/P in L6]
4. ((~P–>Q)–>(((~P–>P)–>P)–>((Q–>P)–>P)))
5. (P–>(((~P–>P)–>P)–>((Q–>P)–>P))) [(2)/(4) MP] Q.E.D.

Lemma 11: ((Q–>((~P–>P)–>P))–>((~P–>P)–>P))

1. (P–>(((~P–>P)–>P)–>((Q–>P)–>P)))) [sub. P/ ((~P–>P)–>P) in L10]
2. (((~P–>P)–>P)–>(((~P–>((~P–>P)–>P))–>((~P–>P)–>P))–>((Q–>((~P–>P)–>P))–> ((~P–>P)–>P))))
3. (((~P–>((~P–>P)–>P))–>((~P–>P)–>P))–>((Q–>((~P–>P)–>P))–> ((~P–>P)–>P)))) [(2)/(Axiom 2)MP]
4. ((~P–>P)–>P) [sub. P/ ((~P–>P)–>P) in Axiom 2]
5. (((~P–>((~P–>P)–>P))–>((~P–>P)–>P)))
6. ((Q–>((~P–>P)–>P))–>((~P–>P)–>P)) [(2)/(4) MP] Q.E.D.

Lemma 12: (T–>((~P–>P)–>P))

1. (((~P–>Q)–>R)–>(P–>R)) [sub. P/T, Q/ ((~P–>P)–>P), R/ ((~P–>P)–>P) in L9]
2. (((~T–>((~P–>P)–>P))–>((~P–>P)–>P))–>(T–>((~P–>P)–>P)))
3. ((Q–>((~P–>P)–>P))–>((~P–>P)–>P)) [sub. Q/~T in L11]
4. ((~T–>((~P–>P)–>P))–>((~P–>P)–>P))
5. (T–>((~P–>P)–>P)) [(2)/(4) MP] Q.E.D.

Lemma 13: (~P–>Q)–>(T–>((Q–>P)–>P))

1. (T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S))) [sub. P/~P, R/P, S/P in L7]
2. (T–>((~P–>P)–>P))–>((~P–>Q)–>(T–>((Q–>P)–>P)))
3. ((~P–>Q)–>(T–>((Q–>P)–>P))) [(2)/(L12) MP] Q.E.D.

Lemma 14: (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R))

1. (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/(~P–>Q), Q/(T–>((Q–>P)–>P)) in Axiom 1]
2. ((~P–>Q)–>(T–>((Q–>P)–>P)))–>(((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R))
3. (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R)) [(2)/(L13) MP] Q.E.D.

Lemma 15: ((~P–>Q)–>((Q–>P)–>P))

1. (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R)) [sub. T/ ~((Q–>P)–>P), R/((Q–>P)–>P) in L14]
2. (((~((Q–>P)–>P)–>((Q–>P)–>P))–>((Q–>P)–>P))–>((~P–>Q)–>((Q–>P)–>P)))
3. ((~P–>P)–>P) [sub. P/((Q–>P)–>P) in Axiom 2]
4. ((~((Q–>P)–>P)–>((Q–>P)–>P))–>((Q–>P)–>P))
5. ((~P–>Q)–>((Q–>P)–>P)) [(2)/(4) MP] Q.E.D.

Lemma 17: (P–>((Q–>P)–>P))

1. (((~P–>Q)–>R)–>(P–>R)) [sub. R/((Q–>P)–>P) in L9]
2. (((~P–>Q)–> ((Q–>P)–>P))–>(P–>((Q–>P)–>P)))
3. (P–>((Q–>P)–>P)) [(2)/(L15) MP] Q.E.D.

Lemma 18: (Q–>(P–>Q))

1. ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [P/Q, Q/ (~P–>Q), R/Q, S/P in L5]
2. ((Q–>((~P–>Q)–>Q))–>((P–>(~P–>Q))–>(Q–>(P–>Q))))
3. (P–>((Q–>P)–>P)) [sub. P/Q, Q/~P in L17]
4. (Q–>((~P–>Q)–>Q))
5. ((P–>(~P–>Q))–>(Q–>(P–>Q))) [(2)/(4) MP]
6. (Q–>(P–>Q)) [(5)/(Axiom 3) MP] Q.E.D.

Lemma 19: ((P–>Q)–>R)–>(Q–>R)

1. (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/Q, Q/(P–>Q) in Axiom 1]
2.  (Q–>(P–>Q))–>(((P–>Q)–>R)–>(Q–>R))
3. (((P–>Q)–>R)–>(Q–>R)) [(2)/(L18) MP] Q.E.D.

Modus Ponens:  (P–>((P–>Q)–>Q))

1. ((P–>Q)–>R)–>(Q–>R) [sub. P/~Q, Q/P, R/((P–>Q)–>Q) in L19]
2. ((~Q–>P)–> ((P–>Q)–>Q))–>(P–>((P–>Q)–>Q))
3. ((~P–>Q)–>((Q–>P)–>P)) [sub. P/Q, Q/P in L15]
4. ((~Q–>P)–>((P–>Q)–>Q))
5. (P–>((P–>Q)–>Q)) [(2)/(4) MP] Q.E.D.