Feys [Feys, 1965, p45-46] does a matrix based proof of consistency based on Lewis and Langford's Group V matrices. (The Lewis Matrices are from [Lewis and Langford, 1932, Appendex II, p493-494])

The system S1^{0} (Feys) [S1 superscript 0] is:

- Definitions
- L a =def ~M~a
- a + b =def ~(~a & ~b)
- a > b =def ~ (a & ~b)
- a => b =def ~M(a & ~b)
- a <-> b =def (p>q) & (q>p) [Material equivalence]
- a <=> b =def ( (a => b) & (b => a)) [Strict equivalence]

- Rules
- Axioms

[Hughes and Cresswell, 1968, p217] (Presenting S1) Remind us that many of the definitions used were actually strict equivalences in S1 as Lewis originally presented it. -jh]

[Sobociński, 1962, p53] (Quoting [Feys, 1950])

Note that Sobociński presents both this basis, and (parenthetically) the basis above which has become the traditional one.

- Definitions
- L a =def ~M~a
- a + b =def ~(~a & ~b)
- a > b =def ~ (a & ~b)
- a => b =def ~M(a & ~b)
- a <-> b =def (p>q) & (q>p) [Material equivalence]
- a <=> b =def ( (a => b) & (b => a)) [Strict equivalence]

- Rules
- Axioms

[Sobociński, 1962, p53] (Quoting [Feys, 1950, p43], but converting Fey's p=>q; based axioms to their ~M(p&~q) based equivalents.) (*** note: *** Sobociński has a typo in F2, where he has NMKpqNKqp and should have had NMKKpqNKqp. And note that the original is in Polish notation, and I've converted it to infix, as usual.) -JH

- System PC as a base
- Rules
- Ga': If φ is a PC theorem, or φ is an axiom, then infer |- Lφ
- Gb': If |- L(φ > ψ) and |- L(ψ > φ), infer |- L(Lφ > Lψ)
- Gc : If |- Lφ, infer |- φ (Note this is the RULE, not the AXIOM Lp>p)

- Axioms
- G3: (L(p>q) & L(q>r)) > L(p>r)

[Zeman,
1968, p459]
Note that p459 defines P1^{0}, and then he goes on to show that
P1^{0} is equivalent to S1^{0}

Note that the article also builds S1, and the ONLY difference between S1
and S1^{0} is that S1 has the AXIOM (Lp > p),
and S1^{0} has the RULE that given |- Lp, you can produce |- p.

S1 = S1^{0}
+ p => Mp
[Zeman
1973, p281] (Note that
Lp=>p would have also worked as the axiom. --JH)

S2^{0} = S1^{0}
+ M(p&q) => Mp
[Zeman
1973, p281]

S2 = S1^{0}
+ ~M((p&q) & ~Mp)
[Sobociński,
1962, p53]

S2 = S1^{0}
+ M(p&q) => Mp
[Sobociński,
1962, p53]

S3^{0} = S1^{0}
+ (p=>q) => (Mp=>Mq)
[Zeman
1973, p281]
[Sobociński,
1962, p53]

S4^{0} = S1^{0}
+ MMp => Mp
[Zeman
1973, p281],
[Sobociński,
1962, p53]

S5 = S5^{0} = S1^{0}
+ Mp => LMp
[Zeman,
1973, p281]
([Zeman, 1973, p181] documents
S5^{0} == S5)

T^{0} = S1^{0}
+ any thesis of the form LLa where a is a PC tautology.
[Zeman
1973, p281]

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

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

This page was last modified on January 24th, 2007