Definition Church : Prop := forall X : Prop, (X -> X) -> X -> X. Definition church (n : Church) (X : Prop) (s : X -> X) (z : X) : X := n X s z. Definition zero (X : Prop) (s : X -> X) (z : X) : X := z. Definition one (X : Prop) (s : X -> X) (z : X) : X := s z. Definition two (X : Prop) (s : X -> X) (z : X) : X := s (s z). Definition three (X : Prop) (s : X -> X) (z : X) : X := s (s (s z)). Definition succ (n : Church) (X : Prop) (s : X -> X) (z : X) : X := s (n X s z). Inductive nat : Prop := | Z : nat | S : nat -> nat. Fixpoint toChurch (n : nat) : Church := match n with | Z => zero | S n => succ (toChurch n) end. Definition fromChurch (n : Church) : nat := n nat S Z. Compute church (toChurch (S (S (S Z)))). Compute fromChurch three. Definition plus (m : Church) (n : Church) (X : Prop) (s : X -> X) (z : X) := m X s (n X s z). Definition times (m : Church) (n : Church) (X : Prop) (s : X -> X) (z : X) := m X (n X s) z. Definition plus' (m : Church) (n : Church) := m Church succ n. Definition times' (m : Church) (n : Church) := m Church (plus' n) zero. Compute plus two three. Compute times two three. Compute church (plus' two three). Compute church (times' two three). Definition Pair (A B : Prop) : Prop := forall X : Prop, (A -> B -> X) -> X. Definition pair {A B : Prop} (p : Pair A B) (X : Prop) (k : A -> B -> X) := p X k. Definition create {A B : Prop} (a : A) (b : B) (X : Prop) (k : A -> B -> X) := k a b. Definition fst {A B : Prop} (p : Pair A B) : A := p A (fun a : A => fun b : B => a). Definition snd {A B : Prop} (p : Pair A B) : B := p B (fun a : A => fun b : B => b). Compute pair (create one two). Definition pred (n : Church) : Church := fst (n (Pair Church Church) (fun p => create (snd p) (succ (snd p))) (create zero zero)). Compute church (pred three). Definition Boolean : Prop := forall X : Prop, X -> X -> X. Definition boolean (b : Boolean) (X : Prop) (t : X) (f : X) : X := b X t f. Definition true (X : Prop) (t : X) (f : X) : X := t. Definition false (X : Prop) (t : X) (f : X) : X := f. Definition not (b : Boolean) (X : Prop) (t : X) (f : X) := b X f t. Definition and (a : Boolean) (b : Boolean) (X : Prop) (t : X) (f : X) := a X (b X t f) f. Definition not' (b : Boolean) : Boolean := b Boolean false true. Definition and' (a : Boolean) (b : Boolean) : Boolean := a Boolean b false. Definition isZero (n : Church) : Boolean := n Boolean (fun b => false) true. Compute boolean (not true). Compute boolean (and true true). Compute boolean (not' true). Compute boolean (and' true true). Compute boolean (isZero zero). Compute boolean (isZero two).