S4.01

[Goldblatt, 1973a]

Notes

S4.01 is contained in every known extension of S4 except S4.02 and S4.03 [Goldblatt, 1973a, p567]

S4.01 is decidable [Goldblatt, 1973a, p571]

Based on

S4.01 = S4 plus the axiom MLp > (LMp > LMLp) [Goldblatt, 1973a, p567]

S4.01 = S4 plus the axiom MLp > L(LMp > MLp) [Goldblatt, 1973a, p567]

S4.01 = S4 plus the axiom ML(p>Lp) > L(LMp > MLp) [Goldblatt, 1973a, p567]

S4.01 = S4 plus the axiom (LMp>MLp) > L(LMp>MLp) [Goldblatt, 1973a, p567]

Basis for

(See the notes section.)


Go to ...


This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/s4.01.html
This page was last modified on October 11th, 2005.