28 lines
855 B
Text
28 lines
855 B
Text
|
@include logic.pg
|
|||
|
|
|
|||
|
|
-- excluded middle!
|
|||
|
|
-- P ∨ ~P
|
|||
|
|
em (P : *) : or (P) (not P) := axiom;
|
|||
|
|
|
|||
|
|
-- ~~P => P
|
|||
|
|
dne (P : *) (nnp : not (not P)) : P :=
|
|||
|
|
or_elim P (not P) P (em P)
|
|||
|
|
(fun (p : P) => p)
|
|||
|
|
(fun (np : not P) => nnp np P);
|
|||
|
|
|
|||
|
|
-- ((P => Q) => P) => P
|
|||
|
|
peirce (P Q : *) (h : (P -> Q) -> P) : P :=
|
|||
|
|
or_elim P (not P) P (em P)
|
|||
|
|
(fun (p : P) => p)
|
|||
|
|
(fun (np : not P) => h (fun (p : P) => np p Q));
|
|||
|
|
|
|||
|
|
|
|||
|
|
-- ~(A ∧ B) => ~A ∨ ~B
|
|||
|
|
de_morgan4 (A B : *) (h : not (and A B)) : or (not A) (not B) :=
|
|||
|
|
or_elim A (not A) (or (not A) (not B)) (em A)
|
|||
|
|
(fun (a : A) =>
|
|||
|
|
or_elim B (not B) (or (not A) (not B)) (em B)
|
|||
|
|
(fun (b : B) => h (and_intro A B a b) (or (not A) (not B)))
|
|||
|
|
(fun (nb : not B) => or_intro_r (not A) (not B) nb))
|
|||
|
|
(fun (na : not A) => or_intro_l (not A) (not B) na);
|