Classical Logic

This section introduces the classical logic connectives, "classical or" and "classical exists" through their double negation translation. Induction principles are given that allow you to destruct these formulas as you would their constructive counter parts, so long as the conclusion is double negataion stable.

No classical axioms are assumed.

Classical or

Section ClassicOr.

Definition orC (P Q:Prop) := ~((~P)/\(~Q)).

Lemma orWeaken : forall P Q, ({P}+{Q}) -> orC P Q.

Lemma orC_ind : forall (P Q G:Prop),
(~~G -> G) -> (P -> G) -> (Q -> G) -> (orC P Q) -> G.

Lemma orC_stable : forall P Q, ~~(orC P Q) -> orC P Q.

End ClassicOr.

Classical Existential

Section ClassicExists.

Variable A : Type.
Variable P : A->Prop.

Definition existsC : Prop :=
~forall x:A, ~P x.

Lemma existsWeaken : (exists x:A, P x) -> existsC.

Lemma existsC_ind : forall (Q:Prop),
(~~Q -> Q) -> (forall x:A, P x -> Q) -> existsC -> Q.

Lemma existsC_stable : ~~existsC -> existsC.

End ClassicExists.

Pidgeon Hole Principle

Here we show the classical result of the pigenon hole principle using the classical quantifiers.

Given a finite list of elements and a relation P(n,x) saying when items from the list are selected, there classically exists an item that is selected a classically infinite number of times.

Lemma infinitePidgeonHolePrinicple :
forall (X:Type) (l:list X) (P:nat -> X -> Prop),
(forall n, existsC X (fun x => ~~In x l /\ P n x)) ->
existsC X (fun x => In x l /\ forall n, existsC N (fun m => (n <= m)%nat /\ (P m x))).

This weaker version of the pidgen hole principle uses a function to select elements from a list instead of a releation. It may be more convienent to use at times.

Lemma infinitePidgeonHolePrinicpleB :
forall (X:Type) (l:list X) (f:nat -> X),
(forall n, In (f n) l) ->
existsC X (fun x => In x l /\ forall n, existsC N (fun m => (n <= m)%nat /\ (f m)=x)).