supremecourt.mmt

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 ❙
❚