namespace latin:/❚

fixmeta ur:?LF❚

diagram SFOL_via_operator : ?LogicDiagramOperators := TYPIFY FOL DIAG FROM FILE "C:\Users\nroux\Desktop\kwarc-project\code\archives\MathHub\MMT\LATIN2\source\logic\fol.mmt" ❚

theory TypedUniversalQuantification =
  include ?TypedLogic❙
  forall : {A} (tm A ⟶ prop) ⟶ prop❘# ∀ 2❙
❚

theory TypedUniversalQuantificationND =
  include ?TypedUniversalQuantification❙
  forallI  : {A,P} ({x: tm A} ⊦ P x) ⟶ ⊦ ∀ [x] P x❙
  forallE  : {A,P} ⊦ ∀ P ⟶ {x: tm A} ⊦ P x❘# 3 forallE 4❘role ForwardRule❙
❚

theory TypedExistentialQuantification =
  include ?TypedLogic❙
  exists : {A} (tm A ⟶ prop) ⟶ prop❘# ∃ 2❙
❚

theory TypedExistentialQuantificationND =
  include ?TypedExistentialQuantification❙
  existsI  : {A,P} {x: tm A} ⊦ P x ⟶ ⊦ ∃ P❘# existsI 3 4❙
  existsE  : {A,P,C} ⊦ ∃ P ⟶ ({x: tm A} ⊦ P x ⟶ ⊦ C) ⟶ ⊦ C❘# 4 existsE 5❘❙
❚

theory ISFOL =
  include ?TypedTerms❙
  include ?IPL❙
  include ?TypedUniversalQuantification❙
  include ?TypedExistentialQuantification❙
❚

theory ISFOLND =
  include ?ISFOL❙
  include ?IPLND❙
  include ?TypedUniversalQuantificationND❙
  include ?TypedExistentialQuantificationND❙
❚

theory SFOL =
  include ?PL❙
  include ?ISFOL❙
❚

theory SFOLND =
  include ?SFOL❙
  include ?PLND❙
  include ?ISFOLND❙
❚

theory SFOLEQ =
  include ?SFOL❙
  include ?TypedEquality❙
  notequal : {A} tm A ⟶ tm A ⟶ prop❘= [A,x,y]¬x≐y❘# 2 ≠ 3 prec 30❙
❚

theory SFOLEQND =
  include ?SFOLEQ❙
  include ?SFOLND❙
  include ?TypedEqualityND❙
❚

theory TypedUniqueExistentialQuantification =
  include ?TypedExistentialQuantification❙
  include ?TypedEquality❙
  existsUnique  : {A} (tm A ⟶ prop) ⟶ prop❘# ∃¹ 2❙
❚

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

theory TypedDescription =
  include ?TypedLogic❙
  include ?TypedUniqueExistentialQuantification❙
  the : {A} {P:tm A ⟶ prop} ⊦ ∃¹ P ⟶ tm A❘# the 2 3❙
  the_ax : {A,P: tm A ⟶ prop,p} ⊦ P (the P p)❙
❚

theory TypedChoice =
  include ?TypedLogic❙
  include ?TypedExistentialQuantification❙
  some : {A} {P:tm A ⟶ prop} ⊦ ∃ P ⟶ tm A❘# some 2 3❙
  some_ax : {A,P: tm A ⟶ prop,p} ⊦ P (some P p)❙
❚