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