c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../propositional/proof_theory/minimal.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "syntax.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig MLPf = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include ML %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include MPLPf %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_◇ : ded ◇ P ⇔ ¬ □ (¬ P).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder nec : ded P -> ded □ P.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_k : ded □ (P ⇒ Q) ⇒ □ P ⇒ □ Q.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig D = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include MLPf %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_d : ded □ P ⇒ ◇ P.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig T = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include MLPf %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_t : ded □ P ⇒ P.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig S4 = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include T %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_4 : ded □ P ⇒ □ (□ P).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig S4b = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include S4 %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_4b : ded P ⇒ □ (◇ P).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig S5 = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include T %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ax_5 : ded ◇ P ⇒ □ (◇ P).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%% TODO views from S4 and S4b to S5 and from S5 to S4b.