Strict Implication

From Symbolic Logic by Clarence Irving Lewis and Cooper Harold Langford, 1932/1959. Primitive connectives, ~, , and . Disjunction is defined as usual, and strict implication is defined by (P Q) abbreviates ~(P~ Q). (The notation here is not the same as the original.) Also define strict equivalence by P = Q abbreviates (P Q) (Q P).

Rules:

1. If P = Q has been proved, replacing P in an expression with Q produces an equivalent expression.
2. From P and Q conclude P Q
3. From P and P Q conclude Q

Axioms:

1. (P Q) (Q P)
2. (P Q) P
3. P (P P)
4. ((P Q) R) (P (Q R))
5. P ~~ P
6. ((P Q) (Q R)) (P R)
7. (P (P Q)) Q

This much gives system S1. Adding the following gives S2. (P Q) P

S4 is the set 1-7, together with P P It includes S2.

Material implication can be introduced by setting P Q to mean ~ (P~ Q). It will have its classical properties, but is different than strict implication.