27 lines
859 B
Text
27 lines
859 B
Text
@include logic.pg
|
||
|
||
-- excluded middle!
|
||
-- P ∨ ~P
|
||
axiom em (P : ★) : P ∨ not P;
|
||
|
||
-- ~~P => P
|
||
def 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
|
||
def 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
|
||
def de_morgan4 (A B : ★) (h : not (A ∧ B)) : not A ∨ not B :=
|
||
or_elim A (not A) (not A ∨ not B) (em A)
|
||
(fun (a : A) =>
|
||
or_elim B (not B) (not A ∨ not B) (em B)
|
||
(fun (b : B) => h (and_intro A B a b) (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);
|