**[Lewis and Langford, 1932]**(Original [but skimpy] source)- [Hughes and Cresswell, 1996]
- [Zeman, 1973]

James Dugundji [Dugundji, 1940, p150-151] proved that there is no finite Characteristic Matrix for S2.

Feys [Feys, 1965, p77] (Quoting McKinsey ) points out that there is an infinite Characteristic Matrix for S2.

M. Wajsberg showed ("*Ein erweiterter Klassenkalkül*" in
Monatshefte für Mathematik und Physik, vol 40 (1933), p 118f) that
if a>b is a (PC) tautology, then a=gt;b is a
theorem in S3.
[Simons,
1953, p310].
He goes on to say that Parry extended this to S1.
[Parry,
1939, p143, last paragraph,
and the footnote.] (The paragraph says that his proof is only valid for
S3 and above, but the footnote says how to prove it
for S1 and above from Wajsberg's original paper.

Feys [Feys, 1965, p68] gives a quick matrix based consistency proof of S2.

McKinsey [McKinsey, 1941, p117] gives a decision procedure for S2. ([Feys, 1964, p77] which repeats the procedure in full.)

The system S2 is: Systems S1 + axiom S2 M(p&q)=>(Mp&Mq) [Hughes and Cresswell, 1996, p200] [Lewis and Langford, 1932, p500] Systems S1 through S5 are defined in the last few pages of the last appendex of Lewis and Langford (p500-502). The common axiom list is on page 493. Adjunction, Modus Ponens (Called the "rule of inference"), and "substitution of equivalents" are on pg. 494. Uniform substitution is implicitly included, as introduced on page 125. The definitions above are introduced in Chapter 11, P123-124 (As syntatic equalities, but the '=' sign was stated (p123) to mean logical equivalences.)

The system S2 is system S1 + the axiom M(p&q)=>Mp [Lemmon, 1957, p177] [Hughes and Cresswell 1968, p230]

The system S2 is: System PC + Axiom T Lp>p + K [L(p>q)>(Lp>Lq)] + Becker's Rule [if |- L(p>q), infer |- Lp>Lq ] [Hughes and Cresswell, 1996, p200]

In other words, S2 is:

- PC
- Rule Uniform Substitution
- Rule Modus Ponens

- Rules
- Becker's Rule: from |- L(p>q) infer |- Lp>Lq

- Axioms
- Axiom K: L(p>q)>(Lp>Lq)
- Axiom T: Lp>p

[Hughes and Cresswell, 1996, p200]

S2 is S2^{0}
+ M6: p => Mp
[Zeman,
1973, p281]

In other words, S2 is:

- Definitions
- ?

- Rules
- Axioms

The system S2 is S0.9 (Lemmon) plus the rule "if |- L(a>b) infer |- L(La>Lb)":

- System PC Including
- Definitions
- =>, a=>b =def L(a>b)
- <=>, a<=> =def L(a=b)

- Rules
- If |-
_{PC}a infer |- La - If |- L(a>b) infer |- L(La > Lb)

- If |-
- Axioms

System S6 = System S2 + Axiom S: MMp [Hughes and Cresswell, 1996, p364] [[Halldén, 1950, p230]

© Copyright 2006, by John Halleck, All Rights Reserved.

This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/s2.html

This page was last modified on June 12th, 2008