#NAME FO.
Term : Type.
Prop : Type.
def prf : Prop -> Type.
true : Prop.
false: Prop.
not : Prop -> Prop.
and : Prop -> Prop -> Prop.
or : Prop -> Prop -> Prop.
imp : Prop -> Prop -> Prop.
forall: (Term -> Prop) -> Prop.
exists: (Term -> Prop) -> Prop.
equals: Term -> Term -> Prop.
def equiv: Prop -> Prop -> Prop := A:Prop => B:Prop => and (imp A B) (imp B A).
tt: prf true.
[] prf false --> P:Prop -> prf P
[A] prf (not A) --> prf A -> prf false
[A,B] prf (and A B) --> P:Prop -> (prf A -> prf B -> prf P) -> prf P
[A,B] prf (or A B) --> P:Prop -> (prf A -> prf P) -> (prf B -> prf P) -> prf P
[A,B] prf (imp A B) --> prf A -> prf B
[A] prf (forall A) --> x:Term -> prf (A x)
[A] prf (exists A) --> P:Prop -> (x:Term -> prf (A x) -> prf P) -> prf P
[x,y] prf (equals x y) --> P:(Term -> Prop) -> prf (P x) -> prf (P y).
lem: A:Prop -> prf (or A (not A)).
(; *** Theorems ;)
(; implication ;)
def imp_elim : A:Prop -> B:Prop -> prf (imp A B) -> prf A -> prf B
:= A:Prop => B:Prop => p:prf (imp A B) => p.
def imp_intro : A:Prop -> B:Prop -> (prf A -> prf B) -> prf (imp A B)
:= A:Prop => B:Prop => p:(prf A -> prf B) => p.
(; disjunction ;)
def or_intro_1 : A:Prop -> B:Prop -> prf A -> prf (or A B)
:= A:Prop => B:Prop => p:prf A =>
P:Prop => f:(prf A -> prf P) => g:(prf B -> prf P) => f p.
def or_intro_2 : A:Prop -> B:Prop -> prf B -> prf (or A B)
:= A:Prop => B:Prop => p:prf B =>
P:Prop => f:(prf A -> prf P) => g:(prf B -> prf P) => g p.
def or_elim : A:Prop -> B:Prop -> prf (or A B) -> C:Prop -> prf (imp A C) -> prf (imp B C) -> prf C
:= A:Prop => B:Prop => p:prf (or A B) => p.
(; conjunction ;)
def and_intro : A:Prop -> B:Prop -> prf A -> prf B -> prf (and A B)
:= A:Prop => B:Prop => a:prf A => b:prf B => P:Prop => f:(prf A -> prf B -> prf P) => f a b.
def and_elim_1 : A:Prop -> B:Prop -> prf (and A B) -> prf A
:= A:Prop => B:Prop => p:prf (and A B) => p A (a:prf A => b:prf B => a).
def and_elim_2 : A:Prop -> B:Prop -> prf (and A B) -> prf B
:= A:Prop => B:Prop => p:prf (and A B) => p B (a:prf A => b:prf B => b).
(; Universal quantificator ;)
def forall_intro: P:(Term->Prop) -> (t:Term -> prf (P t)) -> prf (forall P)
:= P:(Term->Prop) => p:(t:Term -> prf (P t)) => p.
def forall_elim: P:(Term->Prop) -> t:Term -> p:prf (forall P) -> prf (P t)
:= P:(Term->Prop) => t:Term => p:prf (forall P) => p t.
(; Existential quantificator ;)
def exists_intro: P:(Term->Prop) -> t:Term -> prf (P t) -> prf (exists P)
:= P:(Term -> Prop) => t:Term => p:prf (P t) =>
A:Prop => f:(x:Term -> prf (P x) -> prf A) => f t p.
def exists_elim: P:(Term->Prop) -> Q:Prop -> prf (exists P) -> prf (forall (x => imp (P x) Q)) -> prf Q
:= P:(Term->Prop) => Q:Prop => p1:prf (exists P) => p2:prf (forall (x => imp (P x) Q))
=> p1 Q p2.
(; Equality ;)
def eq_refl: prf (forall (x:Term => equals x x))
:= x:Term => P:(Term -> Prop) => p:prf (P x) => p.
def eq_sym: prf( forall (x:Term => forall (y:Term => (imp (equals x y) (equals y x)))) )
:= x:Term => y:Term => p:prf (equals x y) => p (z:Term => equals z x) (eq_refl x).
def eq_trans: prf ( forall (x:Term => forall (y:Term => (forall (z:Term => imp (and (equals x y) (equals y z)) (equals x z))))) )
:= x:Term => y:Term => z:Term => p:prf (and (equals x y) (equals y z)) => P:(Term -> Prop) => q:prf (P x) =>
and_elim_2 (equals x y) (equals y z) p P (and_elim_1 (equals x y) (equals y z) p P q).