System S10 [S1 superscript 0] (Feys)



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

Based on (Feys)

The system S10 (Feys) [S1 superscript 0] is:

[Feys, 1950, p43]

[Zeman, 1973, p281]

[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])

OR (Sobociński)

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

[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


[Zeman, 1968, p459] Note that p459 defines P10, and then he goes on to show that P10 is equivalent to S10

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

Basis for

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

S20 = S10 + M(p&q) => Mp [Zeman 1973, p281]

S2 = S10 + ~M((p&q) & ~Mp) [Sobociński, 1962, p53]

S2 = S10 + M(p&q) => Mp [Sobociński, 1962, p53]

S30 = S10 + (p=>q) => (Mp=>Mq) [Zeman 1973, p281] [Sobociński, 1962, p53]

S40 = S10 + MMp => Mp [Zeman 1973, p281], [Sobociński, 1962, p53]

S5 = S50 = S10 + Mp => LMp [Zeman, 1973, p281] ([Zeman, 1973, p181] documents S50 == S5)

T0 = S10 + any thesis of the form LLa where a is a PC tautology. [Zeman 1973, p281]

Go to ...

© Copyright 2006, by John Halleck, All Rights Reserved.
This page is
This page was last modified on January 24th, 2007