namespace http://mathhub.info/Tutorials/Mathematicians ❚

theory PL : ur:?LF =
	prop : type ❙
	
	and : prop ⟶ prop ⟶ prop ❘ # 1 ∧ 2 prec -5 ❙ // jwedge ❙
	not : prop ⟶ prop ❘ # ¬ 1 prec -1 ❙ // jneg ❙
	or : prop ⟶ prop ⟶ prop ❘ # 1 ∨ 2 prec -10 ❙ // jvee ❙
	implies : prop ⟶ prop ⟶ prop ❘ # 1 ⟹ 2 prec -15 ❙ // jrAA ❙
	false : prop ❘ # ⊥ ❙ // jbot ❙
	true : prop ❘ # ⊤ ❙ // jtop ❙
	equiv : prop ⟶ prop ⟶ prop ❘ = [x,y] x ⟹ y ∧ y ⟹ x ❘ # 1 ⟺ 2 prec -20 ❙

	// test : prop ❘ = ⊤ ∨ ¬ ⊤ ❙
❚

theory PLNatDed : ur:?LF =
	include ?PL ❙
	proof : prop ⟶ type ❘ # ⊦ 1 prec -100 ❙
	
	andEliminationRight : {A, B} ⊦ A ∧ B ⟶ ⊦ B ❘# andEr 3 ❙
	andEliminationLeft : {A, B} ⊦ A ∧ B ⟶ ⊦ A ❘ # andEl 3 ❙
	andIntroduction : {A,B} ⊦ A ⟶ ⊦ B ⟶ ⊦ A ∧ B ❘ # andI 3 4 ❙
	ImplicationElimination : {A,B} ⊦ A ⟹ B ⟶ ⊦ A ⟶ ⊦ B ❘ # implE 3 4❙
	orIntroductionLeft : {A,B} ⊦ A ⟶ ⊦ A ∨ B ❘ # orIl 2 3 ❙
	orIntroductionRight : {A,B} ⊦ B ⟶ ⊦ A ∨ B ❘ # orIr❙
	
	ImplicationIntroduction : {A,B} (⊦ A ⟶ ⊦ B) ⟶ ⊦ A ⟹ B ❘ # implI 3 ❙
	orElimination : {A,B,C} ⊦ A ∨ B ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C ❘ # orE 4 5 6❙
	NegationElimination : {A} ⊦ ¬¬A ⟶ ⊦ A ❘ # negE 2❙
	NegationIntroduction : {A} (⊦ A ⟶ ⊦ ⊥) ⟶ ⊦ ¬ A ❘ # negI 2❙
	FalseIntroduction : {A} ⊦ A ⟶ ⊦ ¬ A ⟶ ⊦ ⊥ ❘ # falseI 2 3❙
	FalseElimination : {A} ⊦ ⊥ ⟶ ⊦ A ❘ # falseE 1 2❙
	
	standardExample : {A,B} ⊦ A ∧ B ⟹ B ∧ A ❘
		= [A,B] implI [p1]  andI (andEr p1) (andEl p1)❙
❚

theory FOL : ur:?LF =
	include ?PL ❙
	
	individuals : type ❘ # ι❙ // jiota	❙
	equality : ι ⟶ ι ⟶ prop ❘ # 1 ≐ 2 ❙
	forall : (ι ⟶ prop) ⟶ prop ❘ # ∀ 1 ❙
	exists : (ι ⟶ prop) ⟶ prop ❘ # ∃ 1 ❘
		= [P] ¬∀[x] ¬(P x)❙
	exists_unique : (ι ⟶ prop) ⟶ prop ❘ # ∃! 1 ❘
		= [P] ∃[x] P x ∧ ∀[y] (P y ⟹ y ≐ x) ❙
❚

theory FOLNatDed : ur:?LF =
	include ?FOL ❙
	include ?PLNatDed ❙
	
	forallIntroduction : {P : ι ⟶ prop} ({x : ι} ⊦ P x) ⟶ ⊦ ∀[x] P x ❙
	forallElimination : {P: ι ⟶ prop}⊦ (∀[x] P x) ⟶ {y:ι} ⊦ P y ❙
	
❚