bcb4e51a409d94ae670de96afb8483a4f7855294Stephan Bosch%read "../propositional/proof_theory/minimal.elf".

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen%read "syntax.elf".

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen%sig MLPf = {

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen %include ML %open.

a85473f7c11c8734bdee9c2cbe4b767f144a18aaTimo Sirainen %include MPLPf %open.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen ax_◇ : ded ◇ P ⇔ ¬ □ (¬ P).

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen nec : ded P -> ded □ P.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen ax_k : ded □ (P ⇒ Q) ⇒ □ P ⇒ □ Q.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen}.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen%sig D = {

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen %include MLPf %open.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen ax_d : ded □ P ⇒ ◇ P.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen}.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen%sig T = {

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen %include MLPf %open.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen ax_t : ded □ P ⇒ P.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen}.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen%sig S4 = {

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen %include T %open.

3605fb862d3d15e3e747b0cd34729d61acbb332cTimo Sirainen ax_4 : ded □ P ⇒ □ (□ P).

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen}.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen%sig S4b = {

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen %include S4 %open.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen ax_4b : ded P ⇒ □ (◇ P).

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen}.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen%sig S5 = {

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen %include T %open.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen ax_5 : ded ◇ P ⇒ □ (◇ P).

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen}.

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen

7bd5b1c64cc987715bdaf8cc4907c3c37d5d7b29Timo Sirainen%% TODO views from S4 and S4b to S5 and from S5 to S4b.