minimal.elf revision 239352d9aec4bc3823511873533fa812cbe259c7
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova minimal propositional logic
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova following Tarski, Bernays, and Wajsberg with primitive ⇒ and ⊥
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova %include Base %open.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ⇒ : o -> o -> o. %infix right 5 ⇒.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ¬ : o -> o = [x] x ⇒ ⊥. %prefix 20 ¬.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ∧ : o -> o -> o = [x][y] ¬ (x ⇒ ¬ y). %infix left 10 ∧.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ∨ : o -> o -> o = [x][y] ¬ x ⇒ y. %infix left 10 ∨.
239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova ⇔ : o -> o -> o = [x][y] (x ⇒ y) ∧ (y ⇒ x). %infix none 5 ⇔.