perga/examples/logic.pg

-- False

false : * := forall (A : *), A;

-- no introduction rule

-- elimination rule
false_elim (A : *) (contra : false) : A := contra A;

-- --------------------------------------------------------------------------------------------------------------

-- Negation

not (A : *) : * := A -> false;

-- introduction rule (kinda just the definition)
not_intro (A : *) (h : A -> false) : not A := h;

-- elimination rule
not_elim (A B : *) (a : A) (na : not A) : B := na a B;

-- can introduce double negation (can't eliminate it as that isn't constructive)
double_neg_intro (A : *) (a : A) : not (not A) :=
    fun (notA : not A) => notA a;

-- --------------------------------------------------------------------------------------------------------------

-- Conjunction

and (A B : *) : * := forall (C : *), (A -> B -> C) -> C;

-- introduction rule
and_intro (A B : *) (a : A) (b : B) : and A B :=
    fun (C : *) (H : A -> B -> C) => H a b;

-- left elimination rule
and_elim_l (A B : *) (ab : and A B) : A :=
    ab A (fun (a : A) (b : B) => a);

-- right elimination rule
and_elim_r (A B : *) (ab : and A B) : B :=
    ab B (fun (a : A) (b : B) => b);

-- --------------------------------------------------------------------------------------------------------------

-- Disjunction

-- 2nd order disjunction
or (A B : *) : * := forall (C : *), (A -> C) -> (B -> C) -> C;

-- left introduction rule
or_intro_l (A B : *) (a : A) : or A B :=
    fun (C : *) (ha : A -> C) (hb : B -> C) => ha a;

-- right introduction rule
or_intro_r (A B : *) (b : B) : or A B :=
    fun (C : *) (ha : A -> C) (hb : B -> C) => hb b;

-- elimination rule (kinda just the definition)
or_elim (A B C : *) (ab : or A B) (ha : A -> C) (hb : B -> C) : C :=
    ab C ha hb;

-- --------------------------------------------------------------------------------------------------------------

-- Existential

-- 2nd order existential
exists (A : *) (P : A -> *) : * := forall (C : *), (forall (x : A), P x -> C) -> C;

-- introduction rule
exists_intro (A : *) (P : A -> *) (a : A) (h : P a) : exists A P :=
    fun (C : *) (g : forall (x : A), P x -> C) => g a h;

-- elimination rule (kinda just the definition)
exists_elim (A B : *) (P : A -> *) (ex_a : exists A P) (h : forall (a : A), P a -> B) : B :=
    ex_a B h;

-- --------------------------------------------------------------------------------------------------------------

-- Universal

-- 2nd order universal (just ∏, including it for completeness)
all (A : *) (P : A -> *) : * := forall (a : A), P a;

-- introduction rule
all_intro (A : *) (P : A -> *) (h : forall (a : A), P a) : all A P := h;

-- elimination rule
all_elim (A : *) (P : A -> *) (h_all : all A P) (a : A) : P a := h_all a;

-- --------------------------------------------------------------------------------------------------------------

-- Equality

-- 2nd order Leibniz equality
eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;

-- equality is reflexive
eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;

-- equality is symmetric
eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
    Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;

-- equality is transitive
eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
    Hyz P (Hxy P Hx);

-- equality is a universal congruence
eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
  fun (P : B -> *) (Hfx : P (f x)) =>
      H (fun (a : A) => P (f a)) Hfx;

-- --------------------------------------------------------------------------------------------------------------

-- Some logic theorems

-- ~(A ∨ B) => ~A ∧ ~B
de_morgan1 (A B : *) (h : not (or A B)) : and (not A) (not B) :=
    and_intro (not A) (not B)
        (fun (a : A) => h (or_intro_l A B a))
        (fun (b : B) => h (or_intro_r A B b));

-- ~A ∧ ~B => ~(A ∨ B)
de_morgan2 (A B : *) (h : and (not A) (not B)) : not (or A B) :=
    fun (contra : or A B) => 
        or_elim A B false contra
            (and_elim_l (not A) (not B) h)
            (and_elim_r (not A) (not B) h);

-- ~A ∨ ~B => ~(A ∧ B)
de_morgan3 (A B : *) (h : or (not A) (not B)) : not (and A B) :=
    fun (contra : and A B) =>
        or_elim (not A) (not B) false h
            (fun (na : not A) => na (and_elim_l A B contra))
            (fun (nb : not B) => nb (and_elim_r A B contra));

-- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively

-- A ∧ B => B ∧ A
and_comm (A B : *) (h : and A B) : and B A :=
    and_intro B A
        (and_elim_r A B h)
        (and_elim_l A B h);

-- A ∨ B => B ∨ A
or_comm (A B : *) (h : or A B) : or B A :=
    or_elim A B (or B A) h
        (fun (a : A) => or_intro_r B A a)
        (fun (b : B) => or_intro_l B A b);

-- A ∧ (B ∧ C) => (A ∧ B) ∧ C
and_assoc_l (A B C : *) (h : and A (and B C)) : and (and A B) C :=
    let (a := (and_elim_l A (and B C) h))
        (bc := (and_elim_r A (and B C) h))
        (b := (and_elim_l B C bc))
        (c := (and_elim_r B C bc))
    in
        and_intro (and A B) C (and_intro A B a b) c
    end;

-- (A ∧ B) ∧ C => A ∧ (B ∧ C)
and_assoc_r (A B C : *) (h : and (and A B) C) : and A (and B C) :=
    and_intro A (and B C)
        (and_elim_l A B (and_elim_l (and A B) C h))
        (and_intro B C
            (and_elim_r A B (and_elim_l (and A B) C h))
            (and_elim_r (and A B) C h));

-- A ∨ (B ∨ C) => (A ∨ B) ∨ C
or_assoc_l (A B C : *) (h : or A (or B C)) : or (or A B) C :=
    or_elim A (or B C) (or (or A B) C) h
        (fun (a : A) => or_intro_l (or A B) C (or_intro_l A B a))
        (fun (g : or B C) =>
            or_elim B C (or (or A B) C) g
                (fun (b : B) => or_intro_l (or A B) C (or_intro_r A B b))
                (fun (c : C) => or_intro_r (or A B) C c));

-- (A ∨ B) ∨ C => A ∨ (B ∨ C)
or_assoc_r (A B C : *) (h : or (or A B) C) : or A (or B C) :=
    or_elim (or A B) C (or A (or B C)) h
        (fun (g : or A B) => 
            or_elim A B (or A (or B C)) g
                (fun (a : A) => or_intro_l A (or B C) a)
                (fun (b : B) => or_intro_r A (or B C) (or_intro_l B C b)))
        (fun (c : C) => or_intro_r A (or B C) (or_intro_r B C c));

-- A ∧ (B ∨ C) => A ∧ B ∨ A ∧ C
and_distrib_l_or (A B C : *) (h : and A (or B C)) : or (and A B) (and A C) :=
    or_elim B C (or (and A B) (and A C)) (and_elim_r A (or B C) h)
        (fun (b : B) => or_intro_l (and A B) (and A C)
            (and_intro A B (and_elim_l A (or B C) h) b))
        (fun (c : C) => or_intro_r (and A B) (and A C)
            (and_intro A C (and_elim_l A (or B C) h) c));

-- A ∧ B ∨ A ∧ C => A ∧ (B ∨ C)
and_factor_l_or (A B C : *) (h : or (and A B) (and A C)) : and A (or B C) :=
    or_elim (and A B) (and A C) (and A (or B C)) h
        (fun (ab : and A B) => and_intro A (or B C)
            (and_elim_l A B ab)
            (or_intro_l B C (and_elim_r A B ab)))
        (fun (ac : and A C) => and_intro A (or B C)
            (and_elim_l A C ac)
            (or_intro_r B C (and_elim_r A C ac)));

-- Thanks Quinn!
-- A ∨ B => ~B => A
disj_syllog (A B : *) (nb : not B) (hor : or A B) : A :=
    or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A);

-- (A => B) => ~B => ~A
contrapositive (A B : *) (f : A -> B) (nb : not B) : not A :=
    fun (a : A) => nb (f a);