namespace http://cds.omdoc.org/examples❚

//   intuitionistic first-order logic with natural deduction rules and a few example proofs ❚

theory FOL : http://cds.omdoc.org/urtheories?LF =
  include ?PL❙
  term  : type❙
  forall : (term ⟶ prop) ⟶ prop❘# ∀ 1 ❘## ∀ V1 2❙
  exists : (term ⟶ prop) ⟶ prop❘# ∃ 1 ❘## ∃ V1 2❙
❚

theory FOLNatDed : http://cds.omdoc.org/urtheories?LF =
  include ?FOL❙
  include ?PLNatDed  ❙
  forallI  : {A} ({x} ⊦ (A x)) ⟶ ⊦ ∀ A ❙
  forallE  : {A} ⊦ (∀ A) ⟶ {x} ⊦ (A x)❘ role ForwardRule❙

  existsI  : {A} {c} ⊦ (A c) ⟶ ⊦ ∃ [x] (A x) ❘# existsI 2 3❙
  existsE  : {A,C} ⊦ (∃ [x] A x) ⟶ ({x} ⊦ (A x) ⟶ ⊦ C) ⟶ ⊦ C❙
❚

theory FOLEQ : http://cds.omdoc.org/urtheories?LF =
  include ?FOL❙
  equal  : term ⟶ term ⟶ prop❘# 1 ≐ 2 prec 30❙
❚

theory FOLEQNatDed : http://cds.omdoc.org/urtheories?LF =
  include ?FOLEQ❙
  include ?FOLNatDed  ❙
  refl     : {x} ⊦ x ≐ x❙
  congT    : {x,y} ⊦ x ≐ y ⟶ {T: term ⟶ term} ⊦ (T x) ≐ (T y) ❘# congT 3 4❙
  congF    : {x,y} ⊦ x ≐ y ⟶ {F: term ⟶ prop} ⊦ (F x) ⟶ ⊦ (F y)❘# congF 3 4 5❙
  sym      : {x,y} ⊦ x ≐ y ⟶ ⊦ y ≐ x❙
  trans    : {x,y,z} ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ x ≐ z❙
  
  trans3   : {w,x,y,z} ⊦ w ≐ x ⟶ ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ w ≐ z❘
           = [w,x,y,z,p,q,r] trans (trans p q) r❙
  trans4   : {v,w,x,y,z} ⊦ v ≐ w ⟶⊦ w ≐ x ⟶ ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ v ≐ z❘
           = [v,w,x,y,z,p,q,r,s] trans3 (trans p q) r s❙
❚