Shortest Axiomatizations of Implicational S4 and S5
|Title||Shortest Axiomatizations of Implicational S4 and S5|
|Year of Publication||2002|
|Authors||Ernst, Z, Fitelson, B, Harris, K, Wos, L|
|Series Title||Notre Dame J. Formal Logic|
Shortest possible axiomatizations for the implicational fragments of the modal logics S4 and S5 are reported. Among these axiomatizations is included a shortest single axiom for implicational S4 (which is unprecedented in the literature), and several new shortest single axioms for implicational S5. A variety of automated reasoning techniques were essential to our discoveries.