Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to prove excluded middle is irrefutable in Coq?

I was trying to prove the following simple theorem from an online course that excluded middle is irrefutable, but got stuck pretty much at step 1:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
Proof.
  intros P. unfold not. intros H.

Now I get:

1 subgoals
P : Prop
H : P \/ (P -> False) -> False
______________________________________(1/1)
False

If I apply H, then the goal would be P \/ ~P, which is excluded middle and can't be proven constructively. But other than apply, I don't know what can be done about the hypothesis P \/ (P -> False) -> False: implication -> is primitive, and I don't know how to destruct or decompose it. And this is the only hypothesis.

My question is, how can this be proven using only primitive tactics (as characterized here, i.e. no mysterious autos)?

Thanks.

like image 966
thor Avatar asked Sep 27 '15 21:09

thor


People also ask

How to prove excluded middle?

The law of excluded middle can be expressed by the propositional formula p_¬p. It means that a statement is either true or false. Think of it as claiming that there is no middle ground between being true and being false. Every statement has to be one or the other.

Is the law of excluded middle true?

In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradiction, and the law of identity.


1 Answers

I'm not an expert on this subject, but it was recently discussed on the Coq mailing-list. I'll summarize the conclusion from this thread. If you want to understand these kinds of problems more thoroughly, you should look at double-negation translation.

The problem falls within intuitionistic propositional calculus and can thus be decided by tauto.

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  tauto.
Qed.

The thread also provides a more elaborate proof. I'll attempt to explain how I would have come up with this proof. Note that it's usually easier for me to deal with the programming language interpretation of lemmas, so that's what I'll do:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  unfold not.
  intros P f.

We are asked to write a function that takes the function f and produces a value of type False. The only way to get to False at this point is to invoke the function f.

 apply f.

Consequently, we are asked to provide the arguments to the function f. We have two choices, either pass P or P -> False. I don't see a way to construct a P so I'm choosing the second option.

  right.
  intro p.

We are back at square one, except that we now have a p to work with! So we apply f because that's the only thing we can do.

  apply f.

And again, we are asked to provide the argument to f. This is easy now though, because we have a p to work with.

  left.
  apply p.
Qed. 

The thread also mentions a proof that is based on some easier lemmas. The first lemma is ~(P /\ ~P).

Lemma lma (P:Prop) : ~(P /\ ~P).
  unfold not.
  intros H.
  destruct H as [p].
  apply H.
  apply p.
Qed.

The second lemma is ~(P \/ Q) -> ~P /\ ~Q:

Lemma lma' (P Q:Prop) : ~(P \/ Q) -> ~P /\ ~Q.
  unfold not.
  intros H.
  constructor.
  - intro p.
    apply H.
    left.
    apply p.
  - intro q.
    apply H.
    right.
    apply q.
Qed.   

These lemmas suffice to the show:

Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
  intros P H.
  apply lma' in H.
  apply lma in H.
  apply H.
Qed.
like image 70
Konstantin Weitz Avatar answered Oct 23 '22 04:10

Konstantin Weitz