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))
- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/(P–>Q), Q/((Q–>R)–>(P–>R)), R/S in Axiom 1]
- ((P–>Q)–>((Q–>R)–>(P–>R)))–>((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S))
- ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [(1)/(2) MP] Q.E.D.
Lemma 5: ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R))))
- ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. Q/ (Q–>R), R/(S–>R), S/((S–>Q)–>(P–>(S–>R))) L4]
- (((((Q–>R)–>(S–>R))–>(P–>(S–>R)))–>((S–>Q)–>(P–>(S–>R))))–>((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))))
- ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. P/S, S/ (P–>(S–>R)) in L4]
- ((((Q–>R)–>(S–>R))–>(P–>(S–>R)))–>((S–>Q)–>(P–>(S–>R))))
- ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [(2)/(4) MP] Q.E.D.
Lemma 6: ((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S)))
- ((((Q–>R)–>(P–>R))–>S)–>((P–>Q)–>S)) [sub. s/ (((P–>R)–>S)–>((Q–>R)–>S)) in L4]
- ((((Q–>R)–>(P–>R))–>(((P–>R)–>S)–>((Q–>R)–>S)))–>((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S))))
- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/ (Q–>R), Q/ (P–>R), R/S in Axiom 1]
- ((Q–>R)–>(P–>R))–>(((P–>R)–>S)–>((Q–>R)–>S))
- ((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)))
- ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [sub. P/ (P–>Q), Q/ ((P–>R)–>S), R/ ((Q–>R)–>S), S/T in L5]
- (((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S)))–>((T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S)))))
- (T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S))) [(2)/(L6) MP] Q.E.D.
Lemma 9: (((~P–>Q)–>R)–>(P–>R))
- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. Q/(~P–>Q) in Axiom 1]
- (P–>(~P–>Q))–>(((~P–>Q)–>R)–>(P–>R))
- (((~P–>Q)–>R)–>(P–>R)) [(2)/Axiom 3 MP] Q.E.D.
Lemma 10: (P–>(((~P–>P)–>P)–>((Q–>P)–>P)))
- (((~P–>Q)–>R)–>(P–>R)) [sub. R/ (((~P–>P)–>P)–>((Q–>P)–>P)) in L9]
- (((~P–>Q)–>(((~P–>P)–>P)–>((Q–>P)–>P)))–>(P–>(((~P–>P)–>P)–>((Q–>P)–>P))))
- ((P–>Q)–>(((P–>R)–>S)–>((Q–>R)–>S))) [sub. P/~P, R/P, S/P in L6]
- ((~P–>Q)–>(((~P–>P)–>P)–>((Q–>P)–>P)))
- (P–>(((~P–>P)–>P)–>((Q–>P)–>P))) [(2)/(4) MP] Q.E.D.
Lemma 11: ((Q–>((~P–>P)–>P))–>((~P–>P)–>P))
- (P–>(((~P–>P)–>P)–>((Q–>P)–>P)))) [sub. P/ ((~P–>P)–>P) in L10]
- (((~P–>P)–>P)–>(((~P–>((~P–>P)–>P))–>((~P–>P)–>P))–>((Q–>((~P–>P)–>P))–> ((~P–>P)–>P))))
- (((~P–>((~P–>P)–>P))–>((~P–>P)–>P))–>((Q–>((~P–>P)–>P))–> ((~P–>P)–>P)))) [(2)/(Axiom 2)MP]
- ((~P–>P)–>P) [sub. P/ ((~P–>P)–>P) in Axiom 2]
- (((~P–>((~P–>P)–>P))–>((~P–>P)–>P)))
- ((Q–>((~P–>P)–>P))–>((~P–>P)–>P)) [(2)/(4) MP] Q.E.D.
Lemma 12: (T–>((~P–>P)–>P))
- (((~P–>Q)–>R)–>(P–>R)) [sub. P/T, Q/ ((~P–>P)–>P), R/ ((~P–>P)–>P) in L9]
- (((~T–>((~P–>P)–>P))–>((~P–>P)–>P))–>(T–>((~P–>P)–>P)))
- ((Q–>((~P–>P)–>P))–>((~P–>P)–>P)) [sub. Q/~T in L11]
- ((~T–>((~P–>P)–>P))–>((~P–>P)–>P))
- (T–>((~P–>P)–>P)) [(2)/(4) MP] Q.E.D.
Lemma 13: (~P–>Q)–>(T–>((Q–>P)–>P))
- (T–>((P–>R)–>S))–>((P–>Q)–>(T–>((Q–>R)–>S))) [sub. P/~P, R/P, S/P in L7]
- (T–>((~P–>P)–>P))–>((~P–>Q)–>(T–>((Q–>P)–>P)))
- ((~P–>Q)–>(T–>((Q–>P)–>P))) [(2)/(L12) MP] Q.E.D.
Lemma 14: (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R))
- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/(~P–>Q), Q/(T–>((Q–>P)–>P)) in Axiom 1]
- ((~P–>Q)–>(T–>((Q–>P)–>P)))–>(((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R))
- (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R)) [(2)/(L13) MP] Q.E.D.
Lemma 15: ((~P–>Q)–>((Q–>P)–>P))
- (((T–>((Q–>P)–>P))–>R)–>((~P–>Q)–>R)) [sub. T/ ~((Q–>P)–>P), R/((Q–>P)–>P) in L14]
- (((~((Q–>P)–>P)–>((Q–>P)–>P))–>((Q–>P)–>P))–>((~P–>Q)–>((Q–>P)–>P)))
- ((~P–>P)–>P) [sub. P/((Q–>P)–>P) in Axiom 2]
- ((~((Q–>P)–>P)–>((Q–>P)–>P))–>((Q–>P)–>P))
- ((~P–>Q)–>((Q–>P)–>P)) [(2)/(4) MP] Q.E.D.
Lemma 17: (P–>((Q–>P)–>P))
- (((~P–>Q)–>R)–>(P–>R)) [sub. R/((Q–>P)–>P) in L9]
- (((~P–>Q)–> ((Q–>P)–>P))–>(P–>((Q–>P)–>P)))
- (P–>((Q–>P)–>P)) [(2)/(L15) MP] Q.E.D.
Lemma 18: (Q–>(P–>Q))
- ((P–>(Q–>R))–>((S–>Q)–>(P–>(S–>R)))) [P/Q, Q/ (~P–>Q), R/Q, S/P in L5]
- ((Q–>((~P–>Q)–>Q))–>((P–>(~P–>Q))–>(Q–>(P–>Q))))
- (P–>((Q–>P)–>P)) [sub. P/Q, Q/~P in L17]
- (Q–>((~P–>Q)–>Q))
- ((P–>(~P–>Q))–>(Q–>(P–>Q))) [(2)/(4) MP]
- (Q–>(P–>Q)) [(5)/(Axiom 3) MP] Q.E.D.
Lemma 19: ((P–>Q)–>R)–>(Q–>R)
- (P–>Q)–>((Q–>R)–>(P–>R)) [sub. P/Q, Q/(P–>Q) in Axiom 1]
- (Q–>(P–>Q))–>(((P–>Q)–>R)–>(Q–>R))
- (((P–>Q)–>R)–>(Q–>R)) [(2)/(L18) MP] Q.E.D.
Modus Ponens: (P–>((P–>Q)–>Q))
- ((P–>Q)–>R)–>(Q–>R) [sub. P/~Q, Q/P, R/((P–>Q)–>Q) in L19]
- ((~Q–>P)–> ((P–>Q)–>Q))–>(P–>((P–>Q)–>Q))
- ((~P–>Q)–>((Q–>P)–>P)) [sub. P/Q, Q/P in L15]
- ((~Q–>P)–>((P–>Q)–>Q))
- (P–>((P–>Q)–>Q)) [(2)/(4) MP] Q.E.D.