Argonne National Laboratory

Shortest Axiomatizations of Implicational S4 and S5

TitleShortest Axiomatizations of Implicational S4 and S5
Publication TypeReport
Year of Publication2002
AuthorsErnst, Z, Fitelson, B, Harris, K, Wos, L
Series TitleNotre Dame J. Formal Logic
Date Published01/2002
Other NumbersANL/MCS-P919-0201

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.