The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Let me complete Pierre's answer a little. Because it is easy to find this proof a bit mysterious.

First, excluded middle is `∀A:Prop, A∨¬A`. It is evidently at least as strong as `∀A:Prop, ¬¬(A∨¬A)`. And since the latter is provable in Coq, excluded middle is actually stronger. It is a general principle in constructive mathematics that adding double-negations in a statement can be used to make it weaker: an equivalent principle to excluded middle is double-negation elimination `∀A:Prop, ¬¬A→A`, since it doesn't hold in constructive mathematics, adding double-negation makes it, in general, easier to prove a statement.

The principle behind the proof of `∀A:Prop, ¬¬(A∨¬A)` is as follows.

First remark that `∀A:Prop, ¬(A∧¬A)` is provable. The definition of `¬A` being "a contradiction can be derived from `A`", it should be reasonably clear that this property holds in Coq.

The next step is to prove that `∀A B:Prop, ¬(A∨B) → ¬A∧¬B` (in fact it is an equivalence). This is a de Morgan law which holds even without excluded middle. It is true because given a proof of `A`, I can build a proof of `A∨B` which together with `¬(A∨B)` is contradictory, so `¬A` follows from `¬(A∨B)`. Symmetrically, so does `¬B`.

Now, suppose `¬(A∨¬A)`, by the above property, we have `¬A∧¬¬A`. By the first remark, we have a contradiction. Qed.

On 3 September 2015 at 11:03, Pierre Casteran <pierre.casteran AT labri.fr> wrote:

Hi,

 Assuming ~(A \/ ~A), you first prove ~A, then find a contradiction.


Goal  forall A:Prop, ~ ~(A \/ ~A).
intros A H.
apply H.
right;intro a.
destruct H;now left.
Qed.

Pierre

Le 03/09/2015 10:54, shengyu shen a écrit :

Dear all:

I am trying to prove an exercise in coq art “∀A: Prop, ∼∼(A∨∼A).”


I think this may need exclude middle rule, which is not in “Calculus of
Inductive Constructions“

am I right?

Shen