## 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: Jun 24 2024 at 01:01 UTC