# Posts Tagged ‘Proof’

## 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.

## Aristotle’s Formal Deductive Theory

Posted by allzermalmer on October 25, 2013

This is an axiomatic presentation of Aristotle’s Formal Deductive System. This was formalized by polish logician Jan Lukasiewicz in his book Elements of Mathematical Knowledge.

Aristotelian Formal Deductive System has the condition that “empty names may not be the values of our name variables, i.e., such as “square circle”.” This is another way of stating that the subject must actually exist. This is known as Existential Assumption, which modern deductive systems in logic don’t hold to.  So some of the theorems in this system aren’t acceptable in modern logic.

I have used polish notation, which was used by Lukasiewicz.
C= Conditional Implication (–>)
K= Conjunction (&)
N= Negation (~)

A= Universal Affirmative
E= Universal Negative
I= Particular Affirmative
O= Particular Negative

Axioms

S1: Aaa
All a are a
S2 Iaa
Some a are a
S3: CKAmbAamAab
If all m are b & all a are m then all a are b
S4: CKAmbImaIab
If all m are b & some m are a then some a are b

Definitions

D1: Oab=NAab
Some a are not b= Not all a are b
D2: Eab= NIab
No a are b= Not some a are b.

Postulates

T1: Cpp
p implies p
T2: CCpqCCqrCpr
If p implies q then if q implies r then p implies r
T3: CCpqCNqNp
If p implies q then not q implies not p
T4: CCpNqCqNp
If p implies not q then q implies not p
T5: CCNpqCNqp
If not p implies q then not q implies p
T6: CCKpqrCpCqr
If p & q implies r then if p then q implies r
T7: CCKpqrCqCpr
If p & q implies r then if q then p implies r
T8: CCKpqrCKpNrNq
If p & q implies r then p & not r implies not q
T9: CCKpqrCKNrqNp
If p & q implies r then not r & q implies not p
T10: CCKpqrCCspCKsqr
If p & q implies r then if s implies p then s & q implies r
T11: CCKpqrCCsqCKpsr
If p & q implies r then if s implies q then p & s implies r
T12: CCKpqrCCrsCKqps
If p & q implies r then if r implies s then q & p implies s

Theorems

Law of the Square of Opposition

S5 COabNAab
1. Cpp [sub p/NAab in T1]
2. CNAabNAab
3. COabNAab [by D1 of antecedent in 2]
Q.E.D.

S6 CNAabOab
1.Cpp [sub p/NAab in T1]
2. CNAabNAab
3. CNAabOab [D1 of consequent in 2]
Q.E.D.

S7 CAabNOab
1. CCpNqCqNp [sub. p/Oab, q/Aab in T4]
2. CCOabNAabCAabNOab
3. CAabNoab [by (2)/(S5) & MP]
Q.E.D.

S8 CNOabAab
1. CCNpqCNqp [sub. p/Aab, q/Oab in T5]
2. CCNAabOabCNOabAab
3. CNOabAab [by (2)/(S6) & MP]
Q.E.D.

S9 CEabNIab
1. Cpp [sub. p/NIab in T1]
2. CNIabNIab
3. CEabNIab [by D2 of antecedent in 2]
Q.E.D.

S10 CNIabEab
1. Cpp [sub. p/NIab in T1]
2. CNIabNIab
3. CNIabEab [by D2 of consequent in 2]
Q.E.D.

S11 CIabNEab
1. CCpNqCqNp [sub. p/Eab, q/Iab, in T4]
2. CCEabNIabCIabNEab
3. CIabNEab [by (2)/(S9) & MP]
Q.E.D.

S12 CNEabIab
1. CCNpqCNqp [sub. p/Iab, q/Eab in T5]
2. CCNIabEabCNEabIab
3. CNEabIab [by (2)/(S10) & MP]
Q.E.D.

Laws of Subalternation

S13 CAabIab
1. CCKpqrCqCpr [sub. p/Aab, q/Iaa, r/Iab in T7]
2. CCKAabIaaIabCIaaCAabIab
3. CKAmbImaIab [sub. m/a in S4]
4. CKAabIaaIab
5. CIaaCAabIab [by (2)/4) & MP]
6. CAabIab [by (5)/(S2) & MP]
Q.E.D.

S14 CNIabNAab
1. CCpqCNqNp [sub. p/Aab, q/Iab in T3]
2. CCAabIabCNIabNab
3. CNIabNAab [by (2)/(S13) & MP]
Q.E.D.

S15 CEabOab
1. CNIabNAab [reiteration of S14]
2. CEabNAab [by D2 of antecedent of 1]
3. CEabOab [by D1 of consequent of 2]
Q.E.D.

Laws of Contrariety

S16 CNOabNEab
1. CCpqCNqNp [sub. p/Eab, q/Oab, in T3]
2. CCEabOabCNOabNEab
3. CNOabNEab [by (2)/(S15) & MP]
Q.E.D.

S17 CEabNAab
1. CNIabNAab [reiteration S14]
2. CEabNAab [D2 of antecedent (1)]
Q.E.D.

S18 CAabNEab
1. CCpNqCqNp [sub. p/Eab, q/Aab in Th 4]
2. CCEabNAabCAabNEab
3. CAabNEab [by (2)/(S17) & MP]
Q.E.D.

Laws of Subcontrariety

S19 CNIabOab
1. CNIabNAab [reiteration S14]
2. CNIabOab [by (1) & D1 consequent]
Q.E.D.

S20 CNOabIab
1. CCNpqCNqp [sub. p/Iab, q/Oab, in Th 5]
2. CCNIabOabCNOabIab
3. CNOabIab [by (S19)/(2) & MP]
Q.E.D.

Laws of Conversion

S21 CIabIba
1. CCKpqrCpCqr [sub p/Aaa, q/Iab, r/Iba in Th 6]
2. CCKAaaIabIbaCAaaCIabIba
3. CKAmbImaIab [sub m/a, b/a, a/b in (S4)]
4. CKAaaIabIba
5. CAaaCIabIba [(2)/(4) & MP]
6. CIabIba [(S1)/(5) & MP]
Q.E.D.

S22 CAabIba
1. CCpqCqrCpr [sub p/Aab, q/Iab, r/Iba in Th 2]
2. CCAabIabCIabIbaCAabIba
3. CIabIbaCAabIba [by (2)/(S3) & MP]
4. CAabIba [by (3)/(S21) & MP]
Q.E.D.

S23 CNIabNIba
1. CCpqCNqNp [sub p/Iba, q/Iab, r/Iab in Th 3]
2. CCIbaIabCNIabNIba
3. CIabIba [sub a/b, b/a in (S21)]
4. CIbaIab
5. CNIabNIba [by (4)/(2) & MP]
Q.E.D.

S24 CEabNIba
1. CNIabNIba [reiteration (S23)]
2. CEabNIba [D2 of antecedent (1)]
Q.E.D.

S25 CEabEba
1. CEabNIba [reiteration (S24)]
2. Eba=NIba [sub a/b, b/a in D2]
3. CEabEba [by (1)/(2) D2 consequent (1)]
Q.E.D.

Syllogisms Figure 1

S26 CKAmbAamIab (Barbari)
1. CCKpqrCCsqCKpsr [sub p/Amb, q/Ima, r/Iab, s/Aam in Th 11]
2. CCKambImaIabCCAamImaCKAmbAamIab
3. CCAamImaCKAmbAamIab [by (2)/(S4) & MP]
4. CAamIma [sub b/m in (S22)]
5. CKAmbAamIab [by (3)/(4) & MP]
Q.E.D.

S27 CKAmbNIabNIma
1. CCKpqrCKpNrNq [sub p/Amb, q/Ima, r/Iab in Th 8]
2. CCKAmbImaIabCKAmbNIabNIma
3. CKAmbNIabNIma [by (2)/(S4) & MP]
Q.E.D.

S28 CKAmbEbaNIma
1. CCKpqrCCsqCKpsr [sub p/Amb, q/NIab, r/NIab, s/Eba in Th 11]
2. CCKAambNIabNImaCCEbaNIabCKAmbEbaNIma
3. CCEbaNIabCKAmbEbaNIam [by (2)/(S27) & MP]
4. CEabNIba [sub a/b, b/a in (S24)]
5. CEbaNIab
6. CKAmbEbaNIam [by (3)/(5) & MP]
Q.E.D

S29 CKEmbAamEab (Celarent)
1. CCKpqrCCrsCKqps [sub p/Aam, q/Emb, r/NIab, s/Eab in Th 12]
2. CCKAamEmbNIabCCNIabEabCKEmbAamEab
3. CKAmbEbaNIma [sub m/a, b/m, a/b in (S28)]
4. CKamEmbNIab
5. CCNIabEabCKEmbAamEab [by (3)/(4) & MP]
6. CKEmbAamEab [by (5)/(S10) & MP]
Q.E.D.

S30 CKEmbAamOab (Celaront)
1. CCpqCCqrCpr [sub p/KEmbAam, q/Eab, r/Oab in Th 2]
2. CCKEmbAamEabCCEabOabCKEmbAamOab
3. CCEabOabCKEmbAamOab [by (2)/(S29) & MP]
4. CKEmbAamOab [by (3)/(S15) & MP]
Q.E.D.

S31 CKEmbIamIab (Darii)
1. CCKpqrCCsqCKpsr [sub p/Amb, q/Ima, r/Iab, s/Iam in Th 11]
2. CCKAmbImaIabCCIamImaCKAmbIamIab
3. CCIamIMaCKAmbIamIab [by (2)/(S4) & MP]
4. CIabIba [reiteration (S21) & sub m/b]
5. CIamIma
6. CKAmbIamIab [by (3)/(5) & MP]
Q.E.D.

S32 CKNIabImaNAmb
1. CCKpqrCKNrqNp [sub p/Amb, q/Ima, r/Iab, in Th 9]
2. CCKAmbImaIabCKNIabImaNAmb
3. CKNIabImaNAmb pby (2)/(S4) & MP]
Q.E.D.

S33 CKEmbIamOab (Ferio)
1. CKNIabImaNAmb [sub a/m, m/a in (S32)]
2. CKNImbIamNAab
3. Emb=NImb [D2 sub a/m]
4. CKEmbIamNAab
5. CKEmbIam Oab [by (4) & D1 on consequent of (4)]
Q.E.D.

Syllogism Figure 2

S34 CKEbmAamEab (Cesare)
1. CCKpqrCCspCKsqr [sub p/Emb, q/Aam, r/Eab, s/Ebm in Th 10]
2. CCKEmbAamEabCCEbmEmbCKEbmAamEab
3. CCEbmEmbCKEbmAamEab [(2)/(S29) & MP]
4. CEabEba [sub a/b, b/m in (S24)]
5. CEbmEmb
6. CKEbmAamEab [by (5)/(3) & MP]
Q.E.D.

S35 CKEbmAamOab
1. CCpqCCqrCpr [sub p/KEbmAam, q/Eab, r/Oab in Th 2]
2. CCKEbmAamEabCCEabOabCKEbmAamOab
3. CCEabOabCKEbmAamOab [(2)/(S34) & MP]
4. CKEbmAamOab [by (3)/(S15) & MP]
Q.E.D.

S36 CKAbmEamEab (Camestres)
1. CCKpqrCCrsCKqps [sub p/Eam, q/Abm, r/Eba, S/Eab in Th 12]
2. CCKEamAbmEbaCCEbaEabCKAbmEamEab
3. CKEbmAamEab [sub b/a, a/b in (S34)]
4. CKEamAbmEba
5. CCEbaEabCKAbmEamEab [by (2)/(4) & MP]
6. CEabEba [sub a/b, b/a in (S25)]
7. CEbaEab
8. CKAbmEamEab [by (5)/(7) & MP]
Q.E.D.

S37 CKAbmEamOab (Camestrop)
1. CCpqCCqrCpr [sub p/KAbmEam, q/Eab, r/Oab in Th 2]
2. CCKAbmEamEabCCEabOabCKAbmEamOab
3. CCEabOabCKAbmEamOab [by (2)/(S36) & MP]
4. CKAbmEamOab [by (3)/(S15) & MP]
Q.E.D.

S38 CKEbmIamOab (Festino)
1. CCKpqrCCspCKsqr [sub p/Emb, q/Iam, r/Oab, s/Ebm in Th 10]
2. CCKEmbIamOabCCEbmEmbCKEbmIamOab
3. CCEbmEmbCKEbmIamOab [by (2)/(S33) & MP]
4. CEabEba [sub a/b, b/m by (S25)]
5. CEbmEmb
6. CKEbmIamOab [by (3)/(5) & MP]
Q.E.D.

S39 CKAmbNAabNAam
1. CKpqrCKpNrNq [sub p/Amb, q/Aam, r/Aab in Th 8]
2. CCKAmbAamAabCKAmbNAabNAam
3. CKAmbNAabNAam [by (2)/(S3) & MP]
Q.E.D.

S40 CKAbmOamOab (Baroco)
1. CKAmbNAabNAam [sub m/b, b/m in (S39)]
2. CKAbmNAamNAab
3. Oab=NAab [sub b/m in D1]
4. Oam=NAam
5. CKAbmOamOab [D1 of consequent (2)]
Q.E.D.

Syllogism Figure 3

S41 CKAmbAmaIab (Darapti)
1. CCKpqrCCsqCKpsr [sub p/Amb, q/Ima, r/Iab, s/Ama in Th 11]
2. CCKAmbImaIabCCAmaImaCKAmbAmaIab
3. CCAmaImaCKAmbAmaIab [by (2)/(S4) & MP]
4. CAabIab [sub a/m, b/a in (S13)]
5. CAmaIma
6. CKAmbAmaIab [by (5)/(3) & MP]
Q.E.D.

S42 CKEmbAmaOab (Felapton)
1. CCKpqrCCsqCKpsr [sub p/Emb, q/Iam, r/Oab, s/Ama in Th 11]
2. CCKEmbIamOabCCAmaIamCKEmbAmaOab
3. CCAmaIamCKEmbAmaOab [by (2)/(S33) & MP]
4. CAabIba [sub a/m, b/a in (S22)]
5. CAmaIam
6. CKEmbAmaOab [by (5)/(3) & MP]
Q.E.D.

S43 CKImbAmaIab (Disamis)
1. CCKpqrCCrsCKqps [sub p/Ama, q/Imb, r/Iba, s/Iab in Th 12]
2. CCKAmaImbIbaCCIbaIabCKImbAmaIab
3. CKAmbImaIab [sub b/a, a/b in (S4)]
4. CKAmaImbIba
5. CCIbaIabCKImbAmaIab [by (4)/(2) & MP]
6. CIabIba [sub a/b, b/a in (S21)]
7. CIbaIab
8. CKImbAmaIab [by (5)/(7) & MP]
Q.E.D.

S44 CKNAabAamNAmb
1. CCKpqrCKNrqNp [sub p/Amb, q/Aam, r/Aab in Th 9]
2. CCKAmbAamAabCKNAabAamNAmb
3. CKNAabAamNAmb [by (2)/(S3) & MP]
Q.E.D.

S45 CKOmbAmaOab (Bocardo)
1. CKNabAamNAmb [sub a/m, m/a in (S44)]
2. CKNAmbAmaNAab
3. Oab=NAab [sub a/m in D1]
4. Omb=NAmb
5. CKOmbAmaNAab
6. CKOmbAmaOab [by D1 of consequent in (5)]
Q.E.D.

S46 CKEmbImaOab (Fersion)
1. CCKpqrCCsqCKpsr [sub p/Emb, q/Iam, r/Oab, s/Ima in Th 11]
2. CCKEmbIamOabCCImaIamCKEmbImaOab
3. CCImaIamCKEmbImaOab [by (2)/(S33) & MP]
4. CIabIba [sub a/m, b/a in (S21)]
5. CImaIam
6. CKEmbImaOab [by (5)/(3) & MP]
Q.E.D.

Syllogism Figure 4

S47 CKAbmAmaIab (Bamalip)
1. CCKpqrCCspCKsqr [sub p/Imb, q/Ama, r/Iab, s/Abm in Th 10]
2. CCKImbAmaIabCCAbmImbCKAbmAmaIab
3. CCAbmImbCKAbmAmaIab [by (2)/(S43) & MP]
4.CAabIba [sub a/b, b/a in (S22)]
5. CAbmImb
6. CKAbmAmaIab [by (5)/(3) & MP]
Q.E.D.

S48 CKAbmEmaEab (Calemes)
1. CCKpqrCCsqCKpsr [sub p/Abm, q/Eam, r/Eab, s/Ema in Th 11]
2. CCKAbmEamEabCCEmaEamCKAbmEmaEab
3. CCEmaEamCKAbmEmaEab [by (2)/(S36) & MP]
4. CEabEba [sub a/m, b/a in (S25)]
5. CEmaEam
6. CKAbmEmaEab [by (5)/(3) & MP]
Q.E.D.

S49 CKAbmEmaOab (Calemop)
1. CCpqCCqrCpr [sub p/KAbmEma, q/Eab, r/Oab in Th 2]
2. CCKAbmEmaEabCCEabOabCKAbmEmaOab
3. CCEabOabCKAbmEmaOab [by (2)/(S48) & MP]
4. CKAbmEmaOab [by (3)/(S15) & MP]
Q.E.D.

S50 CKIbmAmaIab (Diamtis)
1. CCKpqrCCspCKsqr [sub p/Imb, q/Ama, r/Iab, s/Ibm in Th 10]
2. CCKImbAmaIabCCIbmImbCKIbmAmaIab
3. CCIbmImbCKIbmAmaIab [by (2)/(S43) & MP]
4. CIabIba [sub a/b, b/m in (S21)]
5. CIbmImb
6. CKIbmAmaIab [by (3)/(5) & MP]
Q.E.D.

S51 CKEbmAmaOab
1. CCKpqrCCspCKsqr [sub p/Emb,q/Ama, r/Oab, s/Ebm]
2. CCKEmbAmaOabCCEbmEmbCKEbmAmaOab
3. CCEbmEmaCKEbmAmaOab [by (2)/(S46) & MP]
4. CEabEba [sub a/b, b/m in (S25)]
5. CEbmEmb
6. CKEbmAmaOab [by (5)/(3) & MP]
Q.E.D.

S52 CKEbmImaOab (Fression)
1. CCKpqrCCspCKsqr [sub p/Emb, q/Ima, r/Oab, s/Ebm in Th 10]
2. CCKEmbImaOabCCEbmEmbCKEbmImaOab
3. CCEbmEmbCKEbmImaOab [by (2)/(S46) & MP]
4. CEabEba [sub a/b, b/m in (S25)]
5. CEbmEmb
6. CKEbmImaOab [by (5)/(3) & MP]
Q.E.D.

## Proof of Disjunctive Syllogism

Posted by allzermalmer on July 28, 2013

anguage

(I) Symbols: Ø = contradiction, → = conditional, and [] = Modal Operator
(II) Variables: p, q, r, p’, q’, r’. (Variables lower case)

Well Formed Formula for Language

(i) Ø and any variable is a modal sentence.
(ii) If A is a modal sentence, then []A is a modal sentence.
(iii) If A is a modal sentence and B is a modal sentence, then A implies B (A→B) is a modal sentence.

* A, B, and C are modal sentences, i.e. upper case letters are modal sentences. These upper case letters are “variables as well”. They represent the lower case variables in conjunction with contradiction, conditional, or modal operator.

So A may possibly stand for p, or q, or r. It may also possibly stand for a compound of variables and symbols. So A may stand for q, or A may stand for p→Ø, and etc.

Negation (~) = A→Ø
Conjunction (&) = ~(A→B)
Disjunction (v) = ~A→B
Biconditional (↔) = (A→B) & (B→A)

Because Ø indicates contradiction, Ø is always false. But by the truth table of material implication, A → Ø is true if and only if either A is false or Ø is true. But Ø can’t be true. So A → Ø is true if and only if A is false.

This symbol ∞ will stand for something being proved.

(1) Hypothesis (HY) : A new hypothesis may be added to a proof anytime, but the hypothesis begins a new sub-proof.

(2) Modus Ponens (MP) : If A implies B and A, then B must lie in exactly the same sub-proof.

(3) Conditional Proof (CP): When proof of B is derived from the hypothesis A, it follows that A implies B, where A implies B lies outside hypothesis A.

(4) Double Negation (DN): Removal of double negation ~~A & A lie in the same same sub-proof.

(5) Reiteration (R): Sentence A may be copied into a new sub-proof.

Proof of Disjunctive Syllogism: Because at least one disjunct must be true, by knowing one is false we can infer tat the other is true.

If either p or q and not p, then necessarily true q.

Premise (1) p v q (Hypothesis)
Premise (2) ~p (Hypothesis)
(3) ~p implies q ((1) and Definition v)
Conclusion (4) q (Modus Ponens by (2) and (3))

## Proof of Modus Tollens

Posted by allzermalmer on July 28, 2013

Language

(I) Symbols: Ø = contradiction, → = conditional, and [] = Modal Operator
(II) Variables: p, q, r, p’, q’, r’. (Variables lower case)

Well Formed Formula for Language

(i) Ø and any variable is a modal sentence.
(ii) If A is a modal sentence, then []A is a modal sentence.
(iii) If A is a modal sentence and B is a modal sentence, then A implies B (A→B) is a modal sentence.

* A, B, and C are modal sentences, i.e. upper case letters are modal sentences. These upper case letters are “variables as well”. They represent the lower case variables in conjunction with contradiction, conditional, or modal operator.

So A may possibly stand for p, or q, or r. It may also possibly stand for a compound of variables and symbols. So A may stand for q, or A may stand for p→Ø, and etc.

Negation (~) = A→Ø
Conjunction (&) = ~(A→B)
Disjunction (v) = ~A→B
Biconditional (↔) = (A→B) & (B→A)

Because Ø indicates contradiction, Ø is always false. But by the truth table of material implication, A → Ø is true if and only if either A is false or Ø is true. But Ø can’t be true. So A → Ø is true if and only if A is false.

This symbol ∞ will stand for something being proved.

(1) Hypothesis (HY) : A new hypothesis may be added to a proof anytime, but the hypothesis begins a new sub-proof.

(2) Modus Ponens (MP) : If A implies B and A, then B must lie in exactly the same sub-proof.

(3) Conditional Proof (CP): When proof of B is derived from the hypothesis A, it follows that A implies B, where A implies B lies outside hypothesis A.

(4) Double Negation (DN): Removal of double negation ~~A & A lie in the same same sub-proof.

(5) Reiteration (R): Sentence A may be copied into a new sub-proof.

Proof of Modus Tollens: Given the conditional claim that the consequent is true if the antecedent is true, and given that the consequent is false, we can infer that the antecedent is also false.

(If p implies q & ~q, then necessarily true that ~p)

Premise (1) p implies q (Hypothesis)
Premise (2) ~q (Hypothesis)
(3) q implies Ø ((2) and of Definition ~)
(4) p (Hypothesis)
(5) p implies q (Reiteration of (1))
(6) q (Modus Ponens by (4) and (5))
(7) q implies Ø (Reiteration of (3))
(8) Ø (Modus Ponens by (6) and (7))
(9) p implies Ø ( Conditional Proof by  (5) through (8))
Conclusion (10) ~p ((9) and Definition of ~)

Shortened version, with some steps omitted, would go as follows.

P (1) p implies q
P (2) ~q
(3) q implies Ø ((2) and Definition of ~)
(4) p (Hypothesis)
(5) q (Modus Ponens by (1) and (4))
(6) Ø (Modus Ponens by (3) and (5))
(7) p implies Ø (Conditional Proof by (3) through (6))
C (8)  ~p ((7) and Definition ~)

Here is an even shorter proof of Modus Tollens, and it only requires the rule of inference of Hypothetical Syllogism:

(1) p implies q (Hypothesis)
(2) q implies Ø (Hypothesis)
(3) p implies Ø (Hypothetical Syllogism by (1) and (2))
(4) ~p (Reiteration of (3) by Definition of ~)

So we have proved that If p implies q and ~q, then ~p is necessarily true.