propositional/proof_theory/minimal.elf

239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%read "../syntax/minimal.elf".
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%read "../../first-order/proof_theory/fol.elf".
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova%sig MPLPf = {
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova  %include MPL %open.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova  syllog : ded (P ⇒ Q) ⇒ (Q ⇒ R) ⇒ (P ⇒ R).
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova  peirce : ded ((P ⇒ Q) ⇒ P) ⇒ P.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova  weaken : ded P ⇒ (Q ⇒ P).
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova  contra : ded ⊥ ⇒ P.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova  mp     : ded (P ⇒ Q) -> ded P -> ded Q.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova}.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova