# Posts Tagged ‘Modus Ponens’

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

## Proof of Modus Ponens

Posted by allzermalmer on August 29, 2013

There is a rule of Inference known as Modus Ponens. It is also sometimes known as rule of Detachment.

When it comes to rules of inference, some rules are taking as primitive and some are taken as derived. A primitive rule is one in which no proof is given for the rule, and a derived rule is one that is derived from the primitive rule.

The proof of Modus Ponens, which is to be given here, takes Modus Ponens as a derived rule and will use Disjunctive Syllogism as a primitive rule. So from Two premises and the primitive rule of Disjunctive Syllogism, Modus Ponens as a rule of inference can be derived.

Before we go through the proof, Modus Ponens form of argumentation shall be shown.

(1.) P–>Q [Premise]
(2.) P         [Premise]
(3.) Q         [Conclusion]

Here is an example of Disjunctive Syllogism.

(1.) ~PvQ [Premise]
(2.) P        [Premise]
(3.) Q       [Conclusion]

So Disjunctive Syllogism shall be used as the primitive rule, and from this primitive rule will be able to derive the inference rule of Modus Ponens.

Now there is one point that needs to be gone over first, which is that of Modus Ponens works with conditional statements, or if…then statements. Disjunctive Syllogism works with disjunctive statements, or ‘or’ statements. Conditional statements have equivalent forms of disjunctive statements. This is how conditional statements are known as material implications statements.

So, P–>Q is a material implication, and thus can be switched into it’s disjunctive form. So P–>Q, as a material implication, states that ~PvQ. This equivalence shall be used in the proof of modus ponens.

(1.) P–>Q [Premise]
(2.) P         [Premise]
(3.) ~PvQ [Definition of (1)]
(4.) Q       [(2)-(3) by Disjunctive Syllogism] [Conclusion]

Posted by allzermalmer on July 29, 2013

There was a paper called “Computer Implication and the Curry Paradox”. It was authored by both Wayne Aitken and Jeffery A. Barrett, which appears in Journal of Philosophical Logic vol. 33 in 2004.

Suppose an Implication Program has two input statements that are about the behavior of the program, then it tries to deduce the second statement from the first statement by some specified rules in it’s library.

If program finds a deduction of the second statement from the first statement, then the program halts and has output of 1 to signal proof has been found.

The Implication Program can prove statements involving the Implication Program itself.

It is assumed throughout the paper that programs are written in a fixed language for a computer with unlimited memory.

The Impossibility Theorem basically states that “no sufficiently powerful implication program can incorporate an unrestricted form of modus ponens.”

One of the consequences of this Impossibility Theorem is that “modus ponens is an example of a valid rule of inference that can be defined algorithmically, but cannot be used by the implication program.”

Assume (1) that property C(X) is defined to hold if and only if X having property X implies Goldbach’s Conjecture. Furthermore, suppose (2) that C (C). Thus, by the definition of C (X) it implies that C (C) implies Goldbach’s Conjecture. Since C (C) is true by assumption, then it follows by Modus Ponens that Goldbach’s Conjecture is true.

This doesn’t prove Goldbach’s Conjecture yet. However, it does prove that C (C) implies Goldbach’s Conjecture. So by the definition of C (X), it follows that C (C) is true. And by the use of Modus Ponens, Goldbach’s Conjecture is true.

A statement is a list, i.e.  [prog, in, and out]. Prog is a program considered as data, and in is an input for prog, and out is an anticipated output.

A statement is called true if the program prog halts with input in and output out. A statement that isn’t true is called false.

“There is a program to check if but not to test whether [prog, in, out] is a true statement. Given [prog, in, out] as an input, it ﬁrst runs prog as a sub-process with input in. If and when prog halts, it compares the actual output with out. If they match then the program outputs 1; if they do not match, the program does something else (say, outputs 0). This program will output 1 if and only if [prog, in, out] is true, but it might not halt if [prog, in, out] is false. Due to the halting problem, no program can check for falsity.”

So there is a program that check whether [prog, in, out] is a true statement, but the program can’t test whether [prog, in, out] is a true statement. From the Halting problem, no program can check for falsity. So the program can’t check for it’s own falsity, but can check for it’s truth.

It will use 1 as a signal of positive result, and 0 to signal a negative results. However, failure to halt also indicates, but is not a signal to a real use,  a negative result. So failure of the program to halt doesn’t signal a negative result, but it does indicate a negative result.

“A rule is a program that takes as input a list of statements and outputs a list of statements…A valid rule is a rule with the property that whenever the input list consists of only true statements, the output list also consists of only true statements.”

The output list will include the input list as a sublist, and that the rule halt for all input lists.

Take the program AND. This specific program expects as an input a list of two statements. These two statements are [A,B]. The AND Program first checks the truth of A in manner indicated above. If the program determines A is true, then it checks the truth of B. If B is true, then it outputs 1. Now if either A or B is false, the AND program fails to halt.

“A library is a list of rules used by an implication program in its proofs. We assume here that the library is finite at any given time. A valid library is one that contains only valid rules.”

“Consider the implication program ⇒ deﬁned as follows. The program ⇒ expects as input a list of two statements [A, B]. Then it sets up and manipulates a list of sentences called the consequence list. The consequence list begins as a singleton list consisting only of A. The program ⇒ then goes to the library and chooses a rule. It applies the rule to the consequence list, and the result becomes the new consequence list. Since rules are required to include the input list as a sublist of the output list, once a statement appears on any consequence list it will appear on all subsequent consequence lists. After applying a rule, the program ⇒checks whether the consequent B is on the new consequence list. If so, it outputs 1; otherwise it chooses another rule, applies it to update the consequence list, and checks for B on the new consequence list. It continues to apply the rules in an exhaustive way until B is found, in which case ⇒outputs 1. If the consequent B is never found, the implication program ⇒does not halt.”

Take the Modus Ponens Program. This program expects an input list of statements, and from this it starts by forming empty result list. It searches the input list for any statement of the form [–>,[A,B],1] where A and B are statements. From all the statements, it searches to check if A is a statement on the input list. If A is found, then Modus Ponens Program adds B to the result list. The Program outputs a list that shows all the statements in the input list that are followed by all the statements of the result list (if any statements).

“The Modus Ponens program is a rule. A rule is valid if, for an input list of true statements, it only adds true statements. From the definition of –>, if [–>, [A,B],1] and A are on the input list and if they are both true and if the library is valid, then B will be true. So, MP is a valid rule if the library used by –> is valid. “

The EQ program expects an input list that contains [m,n], which are two natural numbers. Supposing m=n, then the EQ outputs 1, or outputs O. This is an example that some statements are clearly false. So let false be the false statement [EQ,[0,1],1]. If 0=1, then the EQ outputs 1, which is truth. This shows some statements are clearly false.

“Consider the program CURRY defined as follows. It expects a program X as input. Then it runs ⇒ as a subprocess with input [[X, X, 1], false]. The output of the subprocess (if any) is then used as the output of CURRY. If X checks for a particular property of programs, then the statement [X, X, 1] asserts that the program X has the very property for which it checks. The program CURRY when applied to program X can be thought of as trying to ﬁnd a proof by contradiction that the statement [X, X, 1] does not hold.”

There is only way that CURRY can output 1 with input X. This is done by if –> outputs 1 with input [[X,X,1}, false].  This is what lies behind the Ad Hoc Rule (AH).

The AH expects a list of statements as input. From there it begins producing an empty result list. It than checks its input for statements that take the form of [CURRY, X, 1] where X is a program. For all such statements on input list, AH adds the statement [–>,[[X,X,1], false] to the result list. The AH will than construct a result list, which contains statements in the input list followed by the statements of the result list (if any).

AH is a valid rule because the statements on the input list are true and AH only adds true statements to form the output list. AH is ad hoc because it is specifically designed for the CURRY program.

“We now describe an algorithmic version of the Curry paradox. We assume that the library is valid and contains MP and AH. Consider what happens when we run ⇒ with input [[ CURRY, CURRY, 1], false]. First a consequence list containing the statement [ CURRY, CURRY, 1] is set-up. Next rules from the library are applied to the consequence list. At some point the Ad Hoc Rule AH is applied and, since [ CURRY, CURRY, 1] is on the consequence list, [⇒, [[CURRY, CURRY, 1], false], 1] is added to the consequence list. Because of this, when MP is next applied to the consequence list, false will be added to the list. Since the initial input had the statement false as the second item on the input list, ⇒will halt with output 1 when false appears on the consequence list.”

So the Implication Program outputs 1 with input of [[CURRY, CURRY, 1], false]. Based on the definition of CURRY Program, it implies that CURRY outputs 1 as CURRY is given as an input. Basically, the statement [CURRY, CURRY, 1] is true. A false statement is true.

Suppose that –> is applied to [[CURRY, CURRY, 1], false]. Because the antecedent [CURRY, CURRY, 1] is true, all statements added to the consequence list will also be true. But the statement false is added to the consequences list, which means that false is true, which is a contradiction.

The Curry Paradox has occurred in a concrete setting of a perfectly well-defined program and careful reasoning about the expected behavior.

The Curry Paradox proves that any library containing the Modus Ponens program and Ad Hoc Rule are not valid. AH is unconditionally valid, so we can conclude that MP is not valid in the case where all the other rules in the library are valid.

“We conclude from this that there are valid inference rules (including MP) that are valid only so long as they are not included in the library of rules to be used. Informally, we can say that there are valid rules that one is not allowed to use (in an unrestricted manner) in one’s proofs. It is the very usage of the rule in inference that invalidates it.”

In order to maintain a valid open library, one must check that the rule is valid itself and that it remains valid when added to the library. A rule is independently valid if it is valid regardless of which library is used by the implication library. The Ad Hoc Rule is an example of an independently valid rule. Any library consistent of only independently valid rules is valid.

The Mods Ponens rule isn’t independently valid. The Modus Ponens rule is contingent on the nature of the library. The Curry Paradox itself provides an example of libraries which MP is not valid.

It is thought that the source of the paradox can be considered to be the misuse of MP. It is suggested that modus ponens is the source of the classical Curry paradox

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

## The Logic of Discussions

Posted by allzermalmer on June 7, 2013

This blog will be based on a logical system developed by Polish logician Stanislaw Jakowski. It was published in the journal Studia Logica: An International Journal for Symbolic Logic, T. 24 (1969), pp. 143-1960

Implication (–> or C), Conjunction (& or K), Disjunction (v or A), Equivalence (<–> or E), Negation (~ or N, Possibility (<> or M), Necessity ([] or L),  and Variables (P or p, Q or q, R or r).

P = <>P or p = Mp
<>P = ~[]~P or Mp = NLNp

Discussive Implication (D): P–>Q = <>P–>Q or Dpq = CMpq
Discussive Equivalence (T): P<–>Q = (<>P–>Q) & (<>Q–><>P) or Tpq = KCMpqCMqMp

D1: P–>P = Dpp
D2: (P<–>Q) <–> (Q<–>P) = TTpqTqp
D3: (P–>Q) –> ((Q–>P)–>(P<–>Q)) = DDpqDDqpTpq
D4: ~(P&~P) = NKpNp [Law of Contradiction]
D5: (P&~P) –>Q = DKpNpq [Conjunction Law Overfilling]
D6: (P&Q) –>P = DKpqp
D7: P –> (P&Q) = DpKpq
D8: (P&Q) <–> (Q&P) = TKpqKqp
D9: (P&(Q&R)) <–> ((P&Q)&R) = TKpKqrKKpqr
D10: (P–>(Q–>R)) –> ((P&Q)–>R) = DDpDqrDKpqr [law importation]
D11: ((P–>Q)&(P–>R)) <–> (P–>(Q&R)) = TKDpqDprDpKqr
D12: ((P–>R)&(Q–>R)) <–> ((PvQ)–>R) = TKDprDqrDApqr
D13: P <–> ~~P = TpNNp
D14: (~P–>P) –> P = DDNppp
D15: (P–>~P) –>~P = DDpNpNp
D16: (P<–>~P) –> P = DTpNpp
D17: (P<–>~P) –>~P = DTpNpNp
D18: ((P–>Q)&~Q) –>~P = DKDpqNqNp

D19: ((P–>)&(P–>~Q)) –>~P = DKDpqDpNqNp
D20:  ((~P–>Q)&(~P–>~Q)) –> P = DKDNpqDNpNqp
D21:  (P–>(Q&~Q)) –>~P = DDpKqNqNp
D22:  (~P–>(Q&~Q)) –> P = DDNpKqNqp

D23: ~(P<–>~P) = NTpNp
D24: ~(P–>Q) –> P = DNDpqp
D25: ~(P–>Q) –> ~Q = DNDpqNq
D26: P–> (~Q–>~(P–>Q)) = DpDNqNDpq

A formulation of Aristotle’s Principle of Contradiction would be: “Two contradictory sentences are not both true in the same language” or “Two contradictory sentences are not both true, if the words occurring in those sentences have the same meanings”.

In Two Valued Logic, there is a Theorem known as the Law of Overfilling, or Implicational Law of Overfilling, or Dun Scotus Law, or L2 Theorem 1.

L2 Theorem 1: P—> (~P—>Q)

If an assertion implies its contradiction, then that assertion implies any and all statements.

“A deductive system…is called inconsistent, if its theses include two such which contradict one another, that is such that one is the negation of the other, e.g., (P) and (~ P) . If any inconsistent system is based on a two valued logic, then by the implicational law of overﬁlling one can obtain in it as a thesis any formula P which is meaningful in that system. It suffices…to apply the rule of modus ponens twice[ to P—> (~P—>Q)]. A system in which any meaningful formula is a thesis shall be termed overﬁlled.”

1. Assume: P—> (~P—>Q)
2. Modus Ponens: P
3. Conclusion: ~P—>Q
4. Modus Ponens: ~P
5. Conclusion: Q

“[T]he problem of the logic of inconsistent systems is formulated here in the following manner: the task is to find a system of the sentential calculus which: (1) when applied to the inconsistent systems would not always entail overfilling, (2) would be rich enough to enable practical inference, (3) would have an intuitive justification. “

This means that Discussive Logic does not have the theorem of implicational law of overfilling. The theorem is not always true in Discussive Logic. Discussive Logic does not entail that a contradiction does not always entail any and all assertions. So Discussive Logic rejects the truth of the theorem P—> (~P—> Q), which is a theorem is two value logic, i.e. been proven true under conditions of two value logic.

Kolmogorov’s System

Here are Four axioms from Hilbert’s positive logic, and one axiom introduced by Kolmogorov.

K 1: P—> (Q—>P)
K 2: (P—> (P—>Q))—> (P—>Q)
K 3: (P—> (Q—>R))—> ((Q—> (P—>R))
K 4: (Q—>R)—> ((P—>Q)—> (P—>R))
K 5: (P—>Q)—> ((P—>~Q)—>~P)

Under these axioms, Two valued logic cannot be proved. Implicational Law of Overfilling not being provable in Discussive Logic implies that Two Valued logic cannot be proved in Discussive Logic. This entails that there might be overlap between Two Valued logic and Discussive Logic, but there is not a total overlap between Two Valued logic and Discussive Logic. Not all theorems of Two Valued logic will be theorems in Discussive logic (like law of overfilling), but some theorems of two valued logic are theorems in Discursive logic.

From these Axioms and the rule of inference known as Modus Ponens, there is one theorem which has some similarities to implicational law of overfilling.

K 9: P—> (~P—>~Q)

It is not the only Theorem that can be derived from the Axioms and Modus Ponens. Here is a list of some Theorems that can be derived by using  Modus Ponens on the Axioms.

K 6 : (P—>Q)—> ((Q—R)—> (P—>R))
K 7:  ((Q—>P)—>R)—> (P—>R)
K 8:  P—> ((Q—>~P)—> ~Q)
K 9:  P—> (~P—>~Q)

Proof of how K 6 – K 9 are derived are ignored for here. All that needs to be known is that K3 and applications of Modus Ponens is equal to If K4 then K 6. K 6 and applications of Modus Ponens is equal to If K 1 then K 7. K 7 and applications of Modus Ponens is equal to If K 5 then K 8. K 6 and applications of Modus Ponens is equal to If K 8 then K 7 implies K 9.

This forms Kolmogorov’s System.

Lewis System of Strict Implication

Strict Implication is defined by modal operator of “it is possible that P” or <>P. So “P strictly implies Q” is equal to “It is not possible that both P and not Q”. But taking the conditional statement —> as strict implication means that the implicational law of overfilling is not a theorem.

Material Implication as a conditional is usually defined by the logical relationship of a conjunction.

Material Conditional: P—>Q = ~(P & ~Q)
“P implies Q” is equal to “Not both P and not Q”
Strict Conditional: P—» Q = ~<>(P & ~Q)
“P strictly implies Q” is equal to “It is not possible that both P and not Q”

Under Strict Implication, Law of Overfilling is not a theorem. Under Material Implication, Law of Overfilling is a theorem. And set of theorems which include only strict implication and not material implication is very limited.

Many Valued Logics

Based on a certain Three Value logical matrix, which shall be ignored, the Law of Overfilling is not a theorem. But there is another theorem in the Three Value logic which has some similarity to the Law of Overfilling.

L 1: P—> (~P—> (~~P—> Q))

Based on the theorem (stated above) of this specific three valued logic, it holds the overfilling of a system when it includes the inconsistent thesis of P, ~P, and ~~P. And the implicational theses of two valued calculus remains valued in the three valued logic. But the three valued logic also holds other theorems that are not in two valued logic, which are as follows.

L 2: P—> ~~P
L 3: ~~~P—> P
L 4: ~P—> ~(P—> P)

So in the three valued logic, which is ignoring the logical matrix of this three valued logic, we cannot obtain the Law of Overfilling. The Law of Overfilling will thus be a theorem in two valued logic but not a theorem in this three valued logic. But the three valued logic has a theorem that is similar to the Law of Overfilling but is not equivalent to the Law of Overfilling. This three value logic also has some theorems that are not theorems in two valued logic. Besides the Law of Overfilling not being a theorem in the three valued logic, the rest of implicational theorems in two valued logic are theorems in the three valued logic.

Calculus of Modal Sentences (M2)

The Modal Sentences of (M2) will assume that modal assertions are either true or false, or simply that the Modal sentences are two valued. But now suppose that there are factors that do not allow for the assertion P to be determined strictly to be either true or false.

For example: Suppose that you are flipping a coin. Suppose that you make the assertion that “During the game heads will turn up more times than tails will” and this is represented by the variable of P. There will be certain sequences that turn up so that P is true, and there will be certain sequences that turn up so that P is false. So P may take on both true and false.

“It is necessary that P” = []P

Taking the example above, we can say that “P occurs for all possible events”.

Q is any formula that includes (1) operators —>, V, &, <—>, ~ and [], (2) and variables p,q,r,s..etc. R is any formula that is already a Q formula and is replacements of variables in Q by interpreting them as P(x), Q(x), R(x), S(x)…etc, and interpreting [] by universal quantifiers “for every x”. Every Q satisfies (1) and (2) and every R satisfies (1) and (2), and additionally satisfying (3).

The operators are implication, disjunction, conjunction, equivalence, and necessity. These are applied to variables or connects variables. When those conditions are met, then it is a formula of Q. The replacement of the variables and [] are formula of R. (1) and (2) can be recognized as P–>Q, or []P—>Q, or []P—>P. We can replace those variables to formulas in R: P(x) —> Q(x), or For every x, P(x) —> Q(x), or For every x, P(x) —> P(x).

“It is possible that P” = <>P

<>P can be taken as “it is not necessary that not P”.

<>P = ~[]~P

Like we could change []P into “for every x”, we may also change <>P into “for some x”.

Definition of Discussive Implication and Discussive Equivalence

As is known, even sets of those inscriptions which have no intuitive meaning at all can be turned into a formalized deductive system. In spite of this theoretical possibility, logical researches so far have been taking into consideration such deductive systems which are symbolic interpretations of consistent theories, so that theses in each such system are theorems in a theory formulated in a single symbolic language free from terms whose meanings are vague.

But suppose that theses which do not satisfy those conditions are included into a deductive system. It suffices, for instance, to deduce consequences from several hypotheses that are inconsistent with one another in order to change the nature of the theses, which thus shall no longer reﬂect a uniform opinion. The same happens if the theses advanced by several participants in a discourse are combined into a single system, or if one person’s opinions are so pooled into one system although that person is not sure whether the terms occurring in his various theses are not slightly differentiated in their meanings. Let such a system which cannot be said to include theses that express opinions in agreement with one another, be termed a discussive system. (Italics is authors and Bold is mine)

Each the theses in discussive logic are preceded so that each thesis has the speaker has the reservation such that each assertion means  “in accordance with the opinion of one of the participants in the discussion” or “for a certain admissible meaning of the terms used”. So when you add an assertion to a discussive system, that assertion will have a different intuitive meaning. Discussive assertions have the implicit condition of the equivalence to <>P.

King Solomon having to decide between two harlots claiming to be the mother of a baby. Woman A claimed to be the mother of the baby and not the mother of the dead baby, and Woman B claimed to be the mother of the baby and not the mother of the dead baby. King Solomon being the arbitrator, under Discussive assertions, would have taken each Woman’s claim as having the prefix of possibility, or “it is possible that Woman A is the mother” or “it is possible that Woman A is not the mother”.

Discussive logic is not based on ordinary two valued logic. Discussive logic would not hold Modus Ponens in all cases if it did.

Take the statement P—>Q is asserted in a discussion. It would be understood to mean “It is possible that If P, then Q”. P is asserted in the same discussion. It would be understood to mean “It is possible that P”. Q would not follow from the two assertions in the discussion. For by Q would not follow in the discussion because Q stands for “It is possible that Q”. So it is invalid to infer from “It is possible that if P, then Q” and “It is possible P” that “It is possible that Q”. But people might assume the normal two value logic in which Modus Ponens holds in all cases.

For Discussive Logic, Discussive Implication is defined as such:

Definition of Discussive Implication: P—>Q = <>P—>Q

There is a theorem of M2 based on Discussive Implication.

M2 Theorem 1: <>(<>P—>Q) —> (<>P—><>Q)

So Modus Ponens may be used in Discussrive Logic when we understand that from (<>P—><>Q) and <>P, we may infer that <>Q by Modus Ponens.

For Discussive Logic, Discussive Equivalence is defined as such:

Definition of Discussive Equivalence: P <—> Q = (<>P—>Q) & (<>Q—><>P)

There is a theorem of M2 based on Discussive Implication.

M2 Theorem 2: <> (P<—>Q) —> (<>P—> <>Q)
M2 Theorem 3: <> (P <—> Q) —> (<>Q —> <>P)

Two valued Discussive System of Sentential Calculus: D2

The system of D2 (i.e. Discussive Logic) of two valued discussive sentential calculus is marked by the formula T, and are marked by the following properties: (1) Sentential variables and functors of Discussive Implication, Discussive Equivalence, Disjunction, Conjunction, and Negation. (2)  precedening T with the symbol of <> yields a theorem in two valued sentential calculus of modal sentences M2.

As the author says, “The system defined in this way is discussive, i.e., its theses are provided with discussive assertion which implicitly includes the functor <>/ This is an essential fact, since even such a simple law as P—>P, on replacement of —> with —-> (i.e. discussive implication leads) to a new theorem.”

D2 Theorem 1: P—>P

D2 is not a theorem in M2, specifically because M2 did not have discussive implication. But in order to make D2 theorem 1 into a theorem in M2, you have to add <> to D2 theorem 1 like this:

M2 Theorem 4: <>(P—>P)

System M2 is decidable, so the discussive sentential calculus D2, defined by an interpretation in M2 is decidable too.

Methodological Theorem 1: “Every thesis T in two valued sentential calculus which does not include constant symbols of —>, <—>, V, becomes a thesis in T(d) in discusive sentential calculus D2 when in T the implication symbols is replaced by the [discurssive implication], and the equivalence symbols are replaced by [discusrive equivalence]. “

“Proof. Consider a formula T(d) constructed so as the theorem to be proved describes. It is to be demonstrated that <>T(d) is a thesis in M2. It is claimed that <>T(d) is equivalent to some other formulae; the equivalences will be proved gradually.”

Here are a couple more M2 Theorems.

M2 Theorem 5: <>(P—>Q) <—> (<>P—><>Q)
M2 Theorem 6: <>(P <—> Q) <—> (<>P <—> <>Q)
M2 Theorem 7: <>(P v Q) <—> (<>P v <>Q)

These theorems are about the distribution of <> over the variables. For example, M2 Theorem 5 distributes <> over implication, and M2 Theorem 6 distributes <> over equivalence, and M2 Theorem 7 distributes over Disjunction. M2 Theorem 5 and M2 Theorem 6 have Discussive Implication and Discussive Implication as the antecedents, respectively.

This shows how we can replace Discurssive Implication with regular implication and how we can replace Discurssive Equivalence with regular equivalence. So from <>(P—>Q), which contains Discurssive Implication, can be replaced with regular implication as <>P—><>Q. The form <>(P<—>Q), which contains Discurssive Equivalence, can be replaced with regular implication as <>P,—><>Q. Discurssive assertion like <>(PvQ) has the equivalence in M2, or Modal Logic, as <>P v <>Q.

The procedure yields the formula W, which is equivalent to <>T(d) and includes (1) only the symbols —>, <—>, and V, (2) variables, and (3) symbols <> in certain special positions, like each variable is directly preceded by <> and each symbol <> directly precedes a variable. Forming T(d) from the thesis T belonging to two value logic is possibly be seen that W can be obtained from T by preceding each variable by <>. For example, precede the variable P by <>P or precede the variable Q by <>Q. This procedure would yield the following theorems in M2.

(a) W is a result of the substitution in T
(b) <>T(d) is equivalent to W.
Hence T(d) is a thesis of D2

The theorems just listed above, immediately yields these theorems in Discussive Logic:

D2 Theorem 2: (P<—>Q) <—> (Q<—>P)
D2 Theorem 3: (P—>Q) —> ((Q—>P) —> (P<—>Q))

Each of the connectives in the D2 theorem just listed are Discurssive Equivalence for D2 Theorem 2 and Discurssive Implication for D2 Theorem 3.

Methodological Theorem 2: If T is a thesis in the two valued sentential calculus and includes variables and at the most the functors V, &, ~, then (1) T and (2) ~T —> q, are thesis in D2. The implication of (2) is Discurssive Implication.

Proof: The symbols V, &, and ~ retain respective meanings in M2 and D2, and that (3) []T is a thesis in M2. The symbols V, &, and ~ retain respective meanings in M2 and D2 and that (3) []T is a thesis in M2. Hence (1) by M2 Theorem 8 []P—><>P and (2) by M2 Theorem 9 []P—><>(<>~P—>Q).

M2 Theorem 8: []P—><>P
M2 Theorem 9: []P—> <>(<>~P—>Q)

We may apply the Methodological Theorem 2 to the Two Valued Logic Theorem of ~(Pv~P), i.e. Aristotle’s Principle of Contradiction.

L2 Theorem 3: ~(P&~P)

“Methodological Theorem 2 and Law of Contradiction in Two valued logic yieleds – in view of the law of double negation- the following theorem of Discussive logic.”

D2 Theorem 4: ~(P&~P) [Law of Contradiction]
D2 Theorem 5: (P&~P) —> Q [Conjunctional Law of Overfilling]

What these two theorems are basically stating is this: Suppose that we have an individual in a discussion, and this individual holds to the Discussive assertion of (P&~P), this individual would hold inconsistent opinions. And in Discussive logic, when an individual holds to inconsistent opinion, the persons opinion implies any and all discussive assertions. This basically forbids an individual from holding to discussive assertions that are contradictory to one another by D2 Theorem 4, and if we do hold to contradictory discussive assertions then any discussive assertion follows from the conjunction of contradictory discussive assertions. This is similar to Law of Overfilling in two value logic but not exactly the same.

We also have the following theorems in Discussive Logic.

D2 Theorem 6: (P&Q) —> P
D2 Theorem 7: P—> (P&P)
D2 Theorem 8: (P&Q) <—> (Q&P)
D2 Theorem 9: (P& (Q&R)) <—> ((P&Q) & R)
D2 Theorem 10: (P—> (Q—>R)) —> ((P&Q) —>R) [Law of Importation]
D2 Theorem 11:((P–>Q) & (P—>R)) <—> (P—>(Q & R))
D2 Theorem 12: ((P—>R) & (Q—>R)) <—> ((PvQ) —> R)
D2 Theorem 13:P <—> ~~P
D2 Theorem 14:(~P—>P) —>P
D2 Theorem 15:(P—>~P)>~P
D2 Theorem 16:(P<—>~P) —>P
D2 Theorem 17: (P<—>~P) —>~P
D2 Theorem 18: ((P—>Q) & ~Q) —> ~P

There are laws of inference by reductio ad absurdum that remain valid in Discurssive Logic.

D2 Theorem 19:((P—>Q) & (P—>~Q)) —> ~P
D2 Theorem 20:((~P—>Q) & (~P—>~Q)) > P
D2 Theorem 21:(P> (Q&~Q)) —> ~P
D2 Theorem 22: (~P —> (Q&~Q)) —>P

Here are some other theorems of Discurssive Logic.

D2 Theorem 23:~(P <—> ~P)
D2 Theorem 24:~(P—>Q) —>P
D2 Theorem 25: ~(P—>Q) —>~Q
D2 Theorem 26: P —> (~Q—>~(P—>Q))

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