System S0.9 (Lemmon)

• [Lemmon, 1957] (Original source)

Notes

Based on (Lemmon)

The system S0.9 is Lemmon's basis for S2, minus the rule "From |- L(a>b) infer L(La>Lb)":

• System PC Including
  • Uniform substitution (US)
  • Modus Ponens (MP>)
• Definitions
  • a=>b =def L(a>b)
  • a<=>b =def L(a=b)
• Rules
  • From Tautology_pc(a) infer |- La
  • From |- a<=>b infer |- La<=>Lb
• Axioms
  • Lp > p
  • L(p>q) > L(Lp>Lq)

[Lemmon, 1957, p180]

Go to ...

• Systems Page
• Structures Page
• Logic Page
• John Halleck's home page

© Copyright 2006, by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/s0.9.html
This page was last modified on September 11th, 2006