namespace http://cds.omdoc.org/examples❚
// like fol.mmt but for sorted first-order logic ❚
theory TypedTerms : ur:?LF =
tp: type❙
tm: tp ⟶ type❘# tm 1 prec -5❙
❚
theory SFOL : http://cds.omdoc.org/urtheories?LF =
include ?PL❙
include ?TypedTerms❙
forall : {S} (tm S ⟶ prop) ⟶ prop❘# ∀ 2❙
exists : {S} (tm S ⟶ prop) ⟶ prop❘# ∃ 2❙
❚
theory SFOLEQ : http://cds.omdoc.org/urtheories?LF =
include ?SFOL❙
equal : {S} tm S ⟶ tm S ⟶ prop❘# 2 ≐ 3 prec 30❙
❚
theory SFOLNatDed : http://cds.omdoc.org/urtheories?LF =
include ?SFOL❙
include ?PLNatDed ❙
forallI : {S,A} ({x: tm S} ⊦ (A x)) ⟶ ⊦ ∀ A ❙
forallE : {S,A} ⊦ (∀ A) ⟶ {x: tm S} ⊦ (A x)❘ role ForwardRule❙
existsI : {S,A} {c} ⊦ (A c) ⟶ ⊦ ∃ [x: tm S] (A x) ❘# existsI 2 3❙
existsE : {S,A,C} ⊦ (∃ [x: tm S] A x) ⟶ ({x} ⊦ (A x) ⟶ ⊦ C) ⟶ ⊦ C❙
❚
theory Declarative_SFOL =
include ?SFOLNatDed❙
include ?DeclarativeProofs❙
decl_forallI = forallI❘ # ASSUME 3❙
decl_existsI = existsI❘ # TAKE 3 4❙
❚
theory SFOLEQNatDed : http://cds.omdoc.org/urtheories?LF =
include ?SFOLEQ❙
include ?SFOLNatDed ❙
refl : {S,x: tm S} ⊦ x ≐ x❙
congT : {S, T, x,y} ⊦ x ≐ y ⟶ {F: tm S ⟶ tm T} ⊦ (F x) ≐ (F y) ❘# congT 3 4❙
congF : {S, x,y: tm S} ⊦ x ≐ y ⟶ {F: tm S ⟶ prop} ⊦ (F x) ⟶ ⊦ (F y)❘# congF 3 4 5❙
sym : {S, x,y: tm S} ⊦ x ≐ y ⟶ ⊦ y ≐ x❙
trans : {S, x,y,z: tm S} ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ x ≐ z❙
trans3 : {S, w,x,y,z: tm S} ⊦ w ≐ x ⟶ ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ w ≐ z❘
= [S, w,x,y,z,p,q,r] trans (trans p q) r❙
trans4 : {S, v,w,x,y,z: tm S} ⊦ v ≐ w ⟶⊦ w ≐ x ⟶ ⊦ x ≐ y ⟶ ⊦ y ≐ z ⟶ ⊦ v ≐ z❘
= [S, v,w,x,y,z,p,q,r,s] trans3 (trans p q) r s❙
❚