Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- -- you can add extra negations if you want
- def extra_negations {A : Prop} (a : A) : ¬¬A :=
- show ¬¬A, from not.intro (λ (na: ¬A), na a)
- -- You can remove extra negations beyond 2,
- def triple_elim {A : Prop} (nnna : ¬¬¬A) : ¬A :=
- show ¬A, from not.intro (λ a, nnna (extra_negations a))
- -- LEM is not negated,
- def nnlem {A : Prop} : ¬ ¬(A ∨ ¬A) :=
- show ¬¬(A ∨ ¬A), from not.intro (λ (nlem : ¬ (A ∨ ¬A)),
- have na : ¬ A, from not.intro (λ a, nlem (or.inl a)),
- have a : A, from false.elim (nlem (or.inr na)),
- show false, from na a
- )
- -- We can imagine that LEM is going to be valid through the identity
- def ident {A : Prop} (a : A) : A := a
- def lem_identity {A : Prop} (lem : A ∨ ¬A) : A ∨ ¬A := lem
- def lem_identity2 {A : Prop} (lem : A ∨ ¬A) : A ∨ ¬A := ident lem
- def bar {A B : Prop} (h : ¬ (A ∧ B)) : (A -> ¬ B) ∧ (B -> ¬ A) :=
- and.intro (λ a, (λ b, h (and.intro a b))) (λ b, (λ a, h (and.intro a b)))
- -- So, you can imagine that you can use LEM then without taking it as an axiom.
- def demorgans {A B : Prop} (lem : A ∨ ¬ A) (nab : ¬(A ∧ B)) : ¬A ∨ ¬B :=
- or.elim lem
- (λ a : A, or.inr ((bar nab).left a))
- (λ na : ¬A, or.inl na)
- -- Sometimes this leads to constructive proofs which are similar to classical ones
- def weird_demorgans {A B : Prop} (a_or_b : A ∨ B) (nab : ¬(A ∧ B)) : ¬A ∨ ¬B :=
- or.elim a_or_b
- (λ a,
- have nb : ¬B, from ((bar nab).left) a,
- or.inr nb)
- (λ b, have na : ¬A, from ((bar nab).right b),
- or.inl na)
Add Comment
Please, Sign In to add comment