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