## Stream: Coq users

### Topic: LEM and de-Morgan's law

#### Julin S (Apr 08 2023 at 09:36):

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.

#### Julin S (Apr 08 2023 at 09:37):

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

#### Pierre Castéran (Apr 08 2023 at 09:50):

The de_Morgan variant `forall P Q:Prop, ~(~P/\~Q)->P\/Q.` is equivalent to the excluded-middle.

#### Laurent Théry (Apr 08 2023 at 09:57):

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.

#### Julin S (Apr 08 2023 at 10:04):

Pierre Castéran said:

The de_Morgan variant `forall P Q:Prop, ~(~P/\~Q)->P\/Q.` is equivalent to the excluded-middle.

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

#### Julin S (Apr 08 2023 at 10:05):

Sorry I guess this is it: `de_morgan_not_and_not` in the github file

#### Dominique Larchey-Wendling (Apr 08 2023 at 10:07):

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

#### Pierre Castéran (Apr 08 2023 at 10:08):

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.

#### Julin S (Apr 08 2023 at 10:16):

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?

#### Julin S (Apr 08 2023 at 10:16):

`simpl` and `cbv zeta` reduces both lem and deM.

#### Gaëtan Gilbert (Apr 08 2023 at 10:44):

`intros deM lem; subst lem; revert deM`

#### Gaëtan Gilbert (Apr 08 2023 at 10:44):

or maybe `red` since its the codomain

#### Pierre Castéran (Apr 08 2023 at 10:47):

@Julin S You forgot a negation in `deM`...

Last updated: Oct 04 2023 at 23:01 UTC