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.

Does anyone know the answer?

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.

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

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.

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?

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: Apr 18 2024 at 19:02 UTC