Is possible to prove undecidability of the halting problem in Coq?

Question

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.

Answer 1

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).