# System S10 [S1 superscript 0] (Feys)

## Consistancy

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:

• 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
• Uniform substitution (US)
• Strict detachment (MP=>)
• substitution of strict equivalents. (EQS)
• Adjunction (given |- p and |- q, infer |- a&b) (AD)
• Axioms
• M1: (p&q)=>(q&p)
• M2: (p&q)=>p
• M3: ((p&q)&r)=>(p&(q&r))
• M4: p=>(p&p)
• M5: ((p=>q)&(q=>r))=>(p=>r)

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

• 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
• Uniform substitution (US)
• Strict detachment (MP=>)
• substitution of strict equivalents. (EQS)
• Adjunction (given |- a and |- b, infer |- a&b) (AD)
• Axioms
• F1: ~M((p&q) & ~p)
• F2: ~M((p&q) & ~(q&p)
• F3: ~M(((p&q)&r) & ~(p&(q&r))
• F4: ~M(p & ~(p&p))
• F5: ~M((~M(p&~q)&~M(q&~r)) & ~ ~M(p&~r))

[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

## OR

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