Law of excluded middle can't be proven without extra axiom in coq, right?

That makes the de-Morgan law: `~(A /\ B) -> (~A) \/ (~B)`

unprovable.

I was recently asked why absence of LEM makes this law unprovable and I couldn't answer it.

Does anyone know the answer?

Or how can the presence of LEM prove this de-Morgan law?

The de_Morgan variant `forall P Q:Prop, ~(~P/\~Q)->P\/Q.`

is equivalent to the excluded-middle.

See for instance https://github.com/coq-community/coq-art/blob/master/ch5_everydays_logic/SRC/class.v

Without LEM, when you have to prove `(A \/ B)`

you need to be able to decide which of the two alternatives is true. In the case of the de-Morgan law, it is impossible to make this decision. Note that if `~(A /\ B) -> (~A) \/ (~B)`

is not provable, `~~(~(A /\ B) -> (~A) \/ (~B))`

is provable.

Pierre Castéran said:

The de_Morgan variant

`forall P Q:Prop, ~(~P/\~Q)->P\/Q.`

is equivalent to the excluded-middle.See for instance https://github.com/coq-community/coq-art/blob/master/ch5_everydays_logic/SRC/class.v

Does the two of them being equivalent mean that we can derive LEM from that de-Morgan law?

Sorry I guess this is it: `de_morgan_not_and_not`

in the github file

In general any *negated* propositional statement which is provable using LEM is also provable in plain intuitionistic logic (ie w/o LEM).

Well, I'm sure that the "usual" De Morgan's law implies a weak version of LEM : `forall P, ~ P \/ ~~P`

.

I'm not sure it implies the classic LEM.

I had been trying to copy the proof shown in the github file like this:

```
Theorem foo:
let deM := forall A B:Prop, (~A /\ ~B) -> (A \/ B) in
let lem := forall A:Prop, A \/ ~A in
deM -> lem.
```

Is there a way to zeta-reduce only lem?

`simpl`

and `cbv zeta`

reduces both lem and deM.

`intros deM lem; subst lem; revert deM`

or maybe `red`

since its the codomain

@Julin S You forgot a negation in `deM`

...

Last updated: Jun 24 2024 at 01:01 UTC