namespace http://mathhub.info/ALMANAC/Context-Graph ❚
import found http://mathhub.info/MitM/Foundation ❚

/T How about a first-order-metatheory?❚

theory background_knowledge =
	include found:?Logic ❙
	include found:?InformalProofs ❙
	human: type ❙
	black: human ❙
	fetus: human ❙
	is_person: human ⟶ prop ❙
	has_rights: human ⟶ prop ❙
	is_born: human ⟶ prop ❙
	is_conceived: human ⟶ prop ❙
	is_black: human ⟶ prop ❙
	is_caucasian: human ⟶ prop ❙
	def_fetus: ⊦ is_conceived fetus ∧ ¬ is_born fetus ❙
	def_black: ⊦ is_conceived black ∧ ¬ is_caucasian black ❙
	
	
❚

// theory attack =
	tag ❙
// ❚

theory constitution_pro_choice =
	include ?background_knowledge ❙
	// person: ⊦ ∀[x] (is_person x ⇔ is_born x ∧ is_human x) ❙
	person: ⊦ ∀[x:human] (is_person x ⇒ is_born x) ❙
❚
                                                   
theory constitution_pro_slavery =
	include ?background_knowledge ❙
	// person: ⊦ ∀[x] is_person x ⇔ is_conceived x ∧ is_human x ∧ ¬ is_black x ❙
	person: ⊦ ∀[x:human] (is_person x ⇒ is_caucasian x)  ❙
❚

theory constitution_pro_life =
	include ?background_knowledge ❙
	person: ⊦ ∀[x:human] (is_conceived x ⇒ is_person x) ❙
❚

view constitution_pro_choice_attacks_constitution_pro_slavery : ?constitution_pro_choice → ?constitution_pro_slavery =
	include ?background_knowledge = ?background_knowledge ❙
	// tag ?attack ❙
	/T person = person ❙

❚

view constitution_pro_slavery_attacks_constitution_pro_choice : ?constitution_pro_slavery → ?constitution_pro_choice =
	// tag ?attack ❙
	include ?background_knowledge = ?background_knowledge ❙
	/T person = person ❙

❚

view constitution_pro_life_attacks_constitution_pro_choice : ?constitution_pro_life → ?constitution_pro_choice =
	// tag ?attack ❙
	include ?background_knowledge = ?background_knowledge ❙
 /T person = person ❙

❚

view constitution_pro_life_attacks_constitution_pro_slavery : ?constitution_pro_life → ?constitution_pro_slavery =
	// tag ?attack ❙
	include ?background_knowledge = ?background_knowledge ❙
	/T person = person ❙

❚

view constitution_pro_slavery_attacks_constitution_pro_life : ?constitution_pro_slavery → ?constitution_pro_life =
	// tag ?attack ❙
	include ?background_knowledge = ?background_knowledge ❙
	/T person = person ❙

❚

view constitution_pro_choice_attacks_constitution_pro_life : ?constitution_pro_choice → ?constitution_pro_life =
	// tag ?attack ❙
	include ?background_knowledge = ?background_knowledge ❙
	/T person = person ❙

❚

theory fourteenth_amendment =
	include ?background_knowledge❙
	person: ⊦ is_person black ❙

❚	
	
view fourteenth_amendment_attacks_constitution_pro_slavery : ?fourteenth_amendment → ?constitution_pro_slavery =
	// tag ?attack ❙
	include ?background_knowledge = ?background_knowledge ❙
	/T person = person ❙

❚

theory legal_common_ground =
	include ?background_knowledge ❙
	personhood_and_rights: ⊦ ∀[x] ¬ is_person x ⇒ ¬ has_rights x ❙
❚

theory dredd_scott_v_sanford =
	include ?constitution_pro_slavery ❙
	include ?legal_common_ground ❙
	blacks_have_no_rights: ⊦  ¬ has_rights black ❘ = sketch 
									"				
								  background knowledge.def_black: Blacks are not caucasian. 
									constitution_pro_slavery.person: Whoever is not caucasian is not a person to the constitution. 
									Hence blacks are not persons to the constitution. 
									legal_common_ground.personhood_and_rights: If you're not a person then you have no rights. 
									Ergo blacks have no rights
									" ❙
❚

view dredd_scott_v_sanford_attacks_constitution_pro_life : ?dredd_scott_v_sanford → ?constitution_pro_life =
	include ?background_knowledge = ?background_knowledge ❙
	// tag ?attack ❙
	person = person ❙

❚

view dredd_scott_v_sanford_attacks_constitution_pro_choice : ?dredd_scott_v_sanford → ?constitution_pro_choice =
	include ?background_knowledge = ?background_knowledge ❙
	// tag ?attack ❙
	person = person ❙

❚

view fourteenth_amendment_superseds_dredd_scott_v_sanford : ?dredd_scott_v_sanford → ?constitution_pro_choice =
	// tag ?attack ❙
	include ?background_knowledge = ?background_knowledge ❙
	/T person = person ❙

❚


view fourteenth_amendment_superseds_dredd_scott_v_sanford : ?fourteenth_amendment → ?dredd_scott_v_sanford =
	// tag ?attack ❙
	include ?background_knowledge = ?background_knowledge ❙
	/T person = person ❙

❚

// view constitution_pro_choice_attacks_dredd_scott_v_sanford : ?constitution_pro_choice → ?dredd_scott_v_sanford =
	include ?background_knowledge = ?background_knowledge ❙
	// tag ?attack ❙
	/T person1 = person1 ❙
	/T person2 = person2 ❙
❚

theory roe_v_wade =
	include ?constitution_pro_choice ❙
	include ?legal_common_ground ❙
	fetusses_have_no_rights: ⊦ ¬ has_rights fetus ❘ = sketch 
									"				
								  background knowledge.def_fetus: fetusses are not born. 
									constitution_pro_slavery.person: Whoever is not born is not a person to the constitution. 
									Hence fetusses are not persons to the constitution. 
									legal_common_ground.personhood_and_rights: If you're not a person then you have no rights. 
									Ergo fetusses have no rights
									" ❙
❚


view if_not_dredd_scott_v_sanford_then_not_roe_v_wade : ?dredd_scott_v_sanford → ?roe_v_wade =
	include ?background_knowledge = ?background_knowledge ❙
	black = fetus ❙
	blacks_have_no_rights = fetusses_have_no_rights ❙
	/T person1=person1 ❙
	/T person2=person2 ❙
❚

view roe_v_wade_attacks_constitution_pro_life : ?roe_v_wade → ?constitution_pro_life =
	include ?background_knowledge = ?background_knowledge ❙
	// tag ?attack ❙
	person = person ❙

❚