Classical reasoning
Lemma neg_or_and_neg : ∀(P Q : Prop),
¬ (P ∨ Q) ↔ ((¬ P) ∧ (¬ Q)).
Lemma de_morgan_neg_and : ∀(P Q : Prop),
classical_logic →
¬ (P ∧ Q) → ¬ P ∨ ¬ Q.
Lemma double_neg_or : ∀(P Q : Prop),
classical_logic →
((P ∨ Q) ↔ ~(~P ∧ ¬Q)).
Lemma excluded_middle : ∀(P : Prop),
classical_logic → P ∨ ¬ P.
Lemma classic_axiom_neg_and_or :
(∀(P Q : Prop), ~(~P ∧ ¬Q) → P ∨ Q) → classical_logic.
Lemma classic_axiom_neg_disjunction_other_case :
(∀(P Q : Prop), ~(~P ∧ ¬Q) → ¬P → Q) → classical_logic.
Lemma classic_axiom_sound_cut_left :
(∀(P Q : Prop), (P ∧ ~(~~P ∧ ¬Q)) → Q) → classical_logic.
Lemma classic_axiom_sound_cut_right :
(∀(P Q : Prop), (¬P ∧ ~(~P ∧ ¬Q)) → Q) → classical_logic.
Lemma classic_axiom_sound_contraction :
(∀(P : Prop), ~(~P ∧ ¬P) → P) → classical_logic.
Section Classical_sets.
Variable A : Type.
Lemma union_complement : ∀(P : set A)(a : A),
classical_logic →
union P (set_inverse P) a.
Lemma union_set_inverse : ∀(P Q : set A)(a : A),
classical_logic →
set_inverse (intersection P Q) a →
union (set_inverse P) (set_inverse Q) a.
Lemma double_set_inverse_rev : ∀(P : set A)(a : A),
classical_logic →
set_inverse (set_inverse P) a →
P a.
Lemma union_double_neg_intersection : ∀(P Q : set A),
classical_logic →
set_equal
(union P Q)
(set_inverse (intersection (set_inverse P) (set_inverse Q))).
End Classical_sets.