namespace latin:/❚

fixmeta ur:?LF❚

theory UniversalQuantification =
  include ?UntypedLogic❙
  forall : (term ⟶ prop) ⟶ prop❘# ∀ 1❘## ∀ V1 2❙
❚

theory UniversalQuantificationNDI =
  include ?UniversalQuantification❙
  forallI  : {P} ({x} ⊦ (P x)) ⟶ ⊦ ∀ P❙
❚

theory UniversalQuantificationNDE =
  include ?UniversalQuantification❙
  forallE  : {P,X} ⊦ ∀ P ⟶ ⊦ (P X)❘# 3 forallE 2❘role ForwardRule❙
❚

theory UniversalQuantificationND =
  include ?UniversalQuantificationNDE❙ 
  include ?UniversalQuantificationNDI❙ 
❚

theory ExistentialQuantification =
  include ?UntypedLogic❙
  exists : (term ⟶ prop) ⟶ prop❘# ∃ 1❘## ∃ V1 2❙
❚

theory ExistentialQuantificationNDI =
  include ?ExistentialQuantification❙
  existsI  : {P,X} ⊦ P X ⟶ ⊦ ∃ P❘# existsI 2 3❙
❚

theory ExistentialQuantificationNDE =
  include ?ExistentialQuantification❙
  existsE  : {P,C} ⊦ ∃ P ⟶ ({x} ⊦ (P x) ⟶ ⊦ C) ⟶ ⊦ C❘# 3 existsE 4❘role EliminationRule❙
❚

theory ExistentialQuantificationND =
  include ?ExistentialQuantificationNDI❙ 
  include ?ExistentialQuantificationNDE❙ 
❚

theory IFOL =
  include ?IPL❙
  include ?UniversalQuantification❙
  include ?ExistentialQuantification❙
❚

theory IFOLND =
  include ?IFOL❙
  include ?IPLND❙
  include ?UniversalQuantificationND❙
  include ?ExistentialQuantificationND❙
❚

theory IFOLEQ =
  include ?IPL❙
  include ?Equality❙
  include ?UniversalQuantification❙
  include ?ExistentialQuantification❙
❚

theory IFOLEQND =
  include ?IFOLEQ❙
  include ?IPLND❙
  include ?EqualityND❙
  include ?UniversalQuantificationND❙
  include ?ExistentialQuantificationND❙
❚

theory FOL =
  include ?PL❙ 
  include ?IFOL❙
❚

theory FOLND =
  include ?FOL❙
  include ?PLND❙
  include ?IFOLND❙
❚

theory FOLEQ =
  include ?FOL❙
  include ?Equality❙
❚

theory FOLEQND =
  include ?FOLEQ❙
  include ?FOLND❙
  include ?EqualityND❙
❚

theory RelativizedUniversalQuantification =
  include ?SoftTypedTerms❙
  include ?FOLEQ❙
  rforall : tp ⟶ (term ⟶ prop) ⟶ prop❘= [A,P] ∀[x] x⦂A ⇒ P x❘# ∀' 1 2❙
❚

theory RelativizedUniversalQuantificationND =
  include ?RelativizedUniversalQuantification❙
  include ?FOLEQND❙
  rforallI : {A,F} ({x} ⊦x⦂A ⟶ ⊦ F x) ⟶ ⊦ ∀' A F❘= [A,F,P] forallI [x] impI [xa] P x xa❙
  rforallE : {A,F} ⊦ ∀' A F ⟶ {x} ⊦x⦂A ⟶ ⊦ F x❘= [A,F,p,x,xa] p forallE x impE xa❙
❚

theory RelativizedExistentialQuantification =
  include ?SoftTypedTerms❙
  include ?FOLEQ❙
  rexists : tp ⟶ (term ⟶ prop) ⟶ prop❘= [A,P] ∃[x] x⦂A ∧ P x❘# ∃' 1 2❙
❚

theory RelativizedExistentialQuantificationND =
  include ?RelativizedExistentialQuantification❙
  include ?FOLEQND❙
  rexistsI : {A,F} {x} ⊦x⦂A ⟶ ⊦ F x ⟶ ⊦ ∃' A F❘= [A,F,x,xa,p] existsI x andI xa p❙
  rexistsE : {A,F,C} ⊦ ∃' A F ⟶ ({x} ⊦x⦂A ⟶ ⊦ F x ⟶ ⊦ C) ⟶ ⊦ C❘= [A,F,C,p,P] p existsE [x,q] P x (q andEl) (q andEr)❙
❚

theory UniqueExistentialQuantification =
  include ?ExistentialQuantification❙
  include ?Equality❙
  existsUnique  : (term ⟶ prop) ⟶ prop❘# ∃¹ 1❙  
 ❚

theory UniqueExistentialQuantificationND =
  include ?UniqueExistentialQuantification ❙
  existsUniqueI : {P} {x} ⊦ P x ⟶ ({y} ⊦ P y ⟶ ⊦ x ≐ y) ⟶ ⊦ ∃¹ P❘# existsUniqueI 3 4 5❙
  existsUniqueE : {P,C} ⊦ ∃¹ P ⟶ ({x} ⊦ P x ⟶ ({y} ⊦ P y ⟶ ⊦ x ≐ y) ⟶ ⊦ C) ⟶ ⊦ C❘# 4 existsUniqueE 5❘❙
❚

theory Description =
  include ?Logic❙
  include ?UniqueExistentialQuantification❙
  the : {P} ⊦ ∃¹ P ⟶ term❘# the 1 2❙
  the_ax : {P,p} ⊦ P (the P p)❙
❚

theory Choice =
  include ?Logic❙
  include ?ExistentialQuantification❙
  some : {P} ⊦ ∃ P ⟶ term❘# some 1 2❙
  some_ax : {P,p} ⊦ P (some P p)❙
❚

theory FOLEQDesc = 
  include ?FOLEQ❙
  include ?Description❙
❚

theory FOLEQDescND =
  include ?FOLEQDesc❙
  include ?FOLEQND❙
❚