diff --git a/source/supremecourt.mmt b/source/supremecourt.mmt new file mode 100644 index 0000000000000000000000000000000000000000..99dfc5d2b0ff0843565f50c387e9585abfa405e6 --- /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 â™ +âš