Classical reasoning

There are a few results in the formalization that are only valid in classical logic. This module defines the necessary property classical_logic that I use instead of an axiom, because the property is easier to track in the source code. This module also derives a few classical standard results that are not valid in Coq.
There are also some lemmas that prove that certain classical tautologis are not provable in Coq. Technically this is done by proving that classical_logic follows from these classical tautologies. I use these lemmas to convince myself that certain results really depend on classical reasoning.

Require Export sets.

Definition classical_logic : Prop := ∀(P : Prop), ~~P → P.

standard results


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.

Unprovability in intuitionistic logic


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.

Some classical results for sets


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.