# Posts Tagged ‘Hypothetical Syllogism’

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

## Logically Valid Arguments

Posted by allzermalmer on April 8, 2013

Categorically Valid Syllogisms

M stands for Middle Term; P stands for Major Term; S stands for Minor Term

Figure 1

(1) Barabara:If all M are P and all S are M, then all S are P
P. All M are P
P. All S are M
C. All S are P

(2) Celarent: If no M are P and all S are M, then no S are P
P. No M are P
P. All S are M
C. No S are P

(3) Darii: If all M are P and some S are M, then some S are P
P. All M are P
P. Some S are M
C. Some S are P

(4) Ferio: If no M are P and some S are M, then some S are not P
P. No M are P
P. Some S are M
C. Some S are not P

Figure 2

(1) Camestres: If all P are M and no S are M, then no S are P
P. All P are M
P. No S are M
C. No S are P

(2) Cesare: If no P are M and all S are M then no S are P
P. No P are M
P. All S are M
C. No S are P

(3) Baroko: If all P are M and some S are not M, then some S are not P
P. All P are M
P. Some S are not M
C. Some S are not P

(4) Festino: If no P are M and some S are M, then some S are not P
P. No P are M
P. Some S are M
C. Some S are not P

Figure 3

(1) Datisi: If all M are P and some M are S, then some S are P
P. All M are P
P. Some M are S
C. Some S are P

(2) Disamis: If some M are P and all M are S, then some S are P
P. Some M are P
P. Some M are S
C. Some S are P

(3) Ferison: if no M are P and some M are S, then some S are not P
P. No M are P
P. Some M are S
C. Some S are not P

(4) Bokardo: If some M are not P and all M are S, then some S are not P
P. Some M are not P
P. All M are S
C. Some S are not P

Figure 4

(1) Camenes: If all P are M and no M are S, then no S are P
P. All P are M
P. No M are S
C. No S are P

(2) Dimaris: If some P are M and all M are S, then Some S are P
P. Some P are M
P. All M are S
C. Some S are P

(3) Fresison: If no P are M and some M are S, then some S are not P
P. No P are M
P. Some M are S
C. Some S are not P

Propositional Logic

Modus Ponens: Given the conditional claim that the consequent is true if the antecedent is true, and given that the antecedent is true, we can infer the consequent.
P. If S then P
P. S
C. Q

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.
P. If S then P
P. Not P
C. Not S

Hypothetical Syllogism: Given two conditional such that the antecedent of the second is the consequent of the first, we can infer a conditional such that its antecedent of the first premise and its consequent is the same as the consequent of the second premise.
P. If S then M
P. If M then P
C. If S then P

Constructive Dilemma: Given two conditionals, and given the disjunction of their antecedents, we can infer the disjunction of their consequents.
P. If S then P                 P. If S then P
P. If M then N               P. If M then P
P. S or M                        P. S or M
C. P or N                        C. P or P

Destructive Dilemma: Given two conditionals, and given the disjunction of the negation of their consequents, we can infer the disjunction of the negation of their antecedents.
P. If S then P                P. If S then P
P. If M then N              P. If S then N
P. Not P or Not N        P. Not P or Not N
C. No S or Not M        C. Not S or Not S

Biconditional Argument: Given a biconditional and given the truth value of one side is known, we can infer that the other side has exactly the same truth value.
P. S<–>P    P. S<–>P   P. S<–>P   P. S<–>P
P. S               P. P              P. Not S      P. Not P
C. P              C. S               C. Not P     C. Not S

Disjunctive Addition: Given that a statement is true, we can infer that a disjunct comprising it and any other statement is true, because only one disjunct needs to be true for the disjunctive compound to be true.
P. S
C. S or P

Disjunctive Syllogism: Because at least one disjunct must be true, by knowing one is false we can infer tat the other is true.
P. S or P   P. S or P
P. Not P   P. Not S
C. S          C. P

Simplification: Because both components of a conjunctive argument are true, it is permissible to infer that either of its conjuncts is true.
P. S & P   P. S & P
C. S          C. P

Adjunction: Because both premises are presumed true, we can infer their conjunction.
P. S
P. P
C. S & P

Conjunctive Argument: Because the first premise says that at least one of the conjuncts is false and the second premise identifies a true conjunct, we can infer that the other conjunct is false.
P. ~(S & P)   P. ~(S & P)
P. S                P. P
C. Not P        C. Not S