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