[Coq-Club] : is ∀A: Prop, ∼∼(A∨∼A) provable in Coq?

[shengyu shen]

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

[Pierre Casteran]

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

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

[Arnaud Spiwack]

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.

Post by Pierre Casteran
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

Post by shengyu shen
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

[shengyu shen]

This explanation is much more elaborate, thanks


Shen

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.
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
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

[Dominique Larchey-Wendling]

intro; tauto.

Dominique

Envoyé avec AquaMail pour Android
http://www.aqua-mail.com

Post by shengyu shen
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