From e657cc9932337814c814715e3f319c03016efefa Mon Sep 17 00:00:00 2001 From: Michael Kohlhase <michael.kohlhase@fau.de> Date: Sun, 17 Jun 2018 15:23:17 +0200 Subject: [PATCH] new --- source/supremecourt.mmt | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 source/supremecourt.mmt diff --git a/source/supremecourt.mmt b/source/supremecourt.mmt new file mode 100644 index 0000000..99dfc5d --- /dev/null +++ b/source/supremecourt.mmt @@ -0,0 +1,34 @@ +namespace http://mathhub.info/MitM/smglom/arithmetics ⚠+ +import base http://mathhub.info/MitM/Foundation ⚠+ +theory person : base:?Logic = + object : type ♠+ person : object ⟶ bool ♠+ rights : object ⟶ bool ♠+ fetus : object ⟶ bool ♠+ black : object ⟶ bool ♠+⚠+ +theory legal : base:?Logic = + include ?person ♠+ courtDecision : prop ⟶ type ♠+ axiom_personRights : ⊦ ∀[x] rights x ⇒ person x ♠+⚠+ +theory RoeWade : base:?Logic = + include ?legal ♠+ include ?person ♠+ RoeWade1973 : courtDecision (∀[x] fetus x ⇒ ¬ person x) ♠+⚠+ +theory DredScott : base:?Logic = + include ?legal ♠+ include ?person ♠+ DredScott1857 : courtDecision (∀[x] black x ⇒ ¬ person x) ♠+⚠+ +view RW73DS57 : ?RoeWade -> ?DredScott = + fetus = black ♠+ RoeWade1973 = DredScott1857 ♠+⚠-- GitLab