22
$\begingroup$

I was watching the "Five Stages of Accepting Constructive Mathematics" by Andrej Bauer and he says that there is two kinds of proof by contradiction (or two things that mathematicians call proof by contradiction):

  1. Assume $P$ is false... blah blah blah, contradiction. Therefore $P$ is true.
  2. Assume $P$ is true... blah blah blah, contradiction. Therefore $P$ is false.

The first one is equivalent to the Law of Excluded Middle (LEM) and the second one is to how prove negation.

The proof of the undecidability of the Halting Problem (HP) is a proof by contradiction: assume there is a machine $D$ that can decide the HP... blah blah blah, contradiction. Therefore $D$ does not exist.

So, let $P$ be "$D$ exists and can decide the HP". Assume $P$ is true... blah blah blah, contradiction. Therefore $P$ is false.

This looks like the second kind of proof by contradiction, so is possible to prove the undecidability of the halting-problem in Coq (without assuming LEM)?

EDIT: I would to see some points about proving this using contradiction. I know that this can also be proved using diagonalization.

$\endgroup$
  • 2
    $\begingroup$ @cody Why does a negative statement require contradiction? Or are you restricting to Coq? $\endgroup$ – David Richerby Aug 29 '17 at 15:41
  • 3
    $\begingroup$ @DavidRicherby I'm actually exaggerating a bit, since that's only true in the absence of axioms. In that case, the first (lowest) step of a (cut-free) proof must be Not-Intro in intuitionistic natural deduction. In the case where there are axioms/hypotheses, then it never hurts to apply this step first, since it is invertible, but sometimes it can be avoided. $\endgroup$ – cody Aug 29 '17 at 17:21
  • 2
    $\begingroup$ You know about the paper with the same title? (I think in there I explicitly state that the usual proof of the non-existence of the Halting Oracle is constructive.) $\endgroup$ – Andrej Bauer Aug 29 '17 at 20:36
  • 1
    $\begingroup$ @AndrejBauer, I din't know. Just found it. Yes, you state that "The usual proof of nonexistence of the Halting oracle is yet another example of a constructive proof of negation.". $\endgroup$ – Rafael Castro Aug 29 '17 at 20:57
  • 1
    $\begingroup$ @RafaelCastro: as an undergraduate student you're asking good questions. I am just encouraging you to boldly go where no undergraduate students (or at least not very many) have gone before. $\endgroup$ – Andrej Bauer Aug 30 '17 at 19:34
20
$\begingroup$

You're exactly right that the halting problem is an example of the second kind of "proof by contradiction" - it's really just a negative statement.

Suppose decides_halt(M) is a predicate that says that machine M decides if its input is a machine that halts (that is, M is a program that for some machine m and input i, decides if m halts on input i).

Forgetting for a moment about how to prove it, the halting problem is the statement that there is no machine that decides the halting problem. We might state this in Coq as (exists M, decides_halt M) -> False, or maybe we prefer to say any given machine doesn't solve the halting problem forall M, decides_halt M -> False. It turns out that without any axioms these two formalizations are equivalent in Coq. (I've spelled out the proof so you can see how it works, but firstorder will do the entire thing!)

Parameter machine:Type.
Parameter decides_halt : machine -> Prop.

(* Here are two ways to phrase the halting problem: *)

Definition halting_problem : Prop :=
  (exists M, decides_halt M) -> False.

Definition halting_problem' : Prop :=
  forall M, decides_halt M -> False.

Theorem statements_equivalent :
  halting_problem <-> halting_problem'.
Proof.
  unfold halting_problem, halting_problem'; split; intros.
  - exact (H (ex_intro decides_halt M H0)).
  - destruct H0.
    exact (H x H0).
Qed.

I think either statement isn't too difficult to prove as a diagonalization argument, though formalizing machines, computability, and halting is probably reasonably challenging. For a simpler example, it's not too hard to prove Cantor's diagonalization theorem (see https://github.com/bmsherman/finite/blob/master/Iso.v#L277-L291 for a proof that nat -> nat and nat are not isomorphic).

The diagonalization above gives an example of how you might go about deriving a contradiction from an isomorphism between nat -> nat and nat. Here's the essence of that proof inlined as a self-contained example:

Record bijection A B :=
  {  to   : A -> B
  ; from : B -> A
  ; to_from : forall b, to (from b) = b
  ; from_to : forall a, from (to a) = a
  }.

Theorem cantor :
  bijection nat (nat -> nat) ->
  False.
Proof.
  destruct 1 as [seq index ? ?].
  (* define a function which differs from the nth sequence at the nth index *)
  pose (f := fun n => S (seq n n)).
  (* prove f differs from every sequence *)
  assert (forall n, f <> seq n). {
    unfold not; intros.
    assert (f n = seq n n) by congruence.
    subst f; cbn in H0.
    eapply n_Sn; eauto.
  }
  rewrite <- (to_from0 f) in H.
  apply (H (index f)).
  reflexivity.
Qed.

Even without looking at the details, we can see from the statement that this proof takes the mere existence of a bijection and demonstrates it to be impossible. We first give the two sides of the bijection the names seq and index. The key is that the bijection's behavior at the special sequence f := fun n => S (seq n n) and its index index f is contradictory. The halting problem's proof would derive a contradiction in a similar way, instantiating its hypothesis about a machine that solves the halting problem with a carefully chosen machine (and in particular one that actually depends on the assumed machine).

$\endgroup$
  • $\begingroup$ Welcome to the site! I hope you stick around -- you might like to take our very brief tour to see more about how Stack Exchange works. $\endgroup$ – David Richerby Aug 29 '17 at 14:28
  • 2
    $\begingroup$ I forgot that this problem is also proved by a diagonalization argument. Your answer is interesting but I would like to see some points about if is possible to prove the HM using a contradiction in Coq. I will make this more clear in the question. $\endgroup$ – Rafael Castro Aug 29 '17 at 14:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.