# Question about the undecidability of $A_{TM}$

You probably know this one (or at least a version of it).
Let $P$ be a program code, and $w$ be an input string.
Define $A_{TM}=\left\{(P,w)| P(w)=1\right\}$.
Meaning: $A_{TM}$ is the set of all ordered pairs $(P,w)$ s.t. $P$ accepts $w$.
$A_{TM}$ is undecidable.

The brief of the proof (by contradiction) looks something like this:
Suppose there exist $D_{A_{TM}}$ - a computer program that answers 'yes' if $(P,w)\in A_{TM}$, and 'no' if $(P,w)\notin A_{TM}$.
Let us consider the following program:

$Q(w):$
1. run $D_{A_{TM}}$ on $(w,w)$
2. if $D_{A_{TM}}$ returned 'yes', then return 'no'. if $D_{A_{TM}}$ returned 'no', return 'yes'.

Now running $Q(w);$ with the input $Q$, contradicts the existence of such $D_{A_{TM}}$

This is a brief, since I assume most of you already know this problem (and its proof).

Now what makes me wonder is this: when I looked at $A_{TM}$, and needed to determine if it's decidable or not, the first thing that came to my mind when I tried to imagine a machine that accepts $A_{TM}$, is how can machine like that handle inputs $(P,w)$ s.t. $P$ doesn't halt on $w$? How can it 'predicts', beforehand, that $P(w)$ goes to an infinite loop, without actually running $P$ on $w$?
That intuition, as it turns out, wasn't wrong.
The thing is: How come the proof, as clever as it is, has nothing to do with that fact?
You'd expect it to lean - and even in the slightest way - on that leverage, but instead, the proof looks like something that was taken from the realm of paradoxes.

Basically, what I'm asking is: why does this proof work?

If you know what the program is doing, you can predict its outcome even without running it. For example, consider the following program.

INPUT: a polynomial P with integer coefficients
n = 0
while P(n) is different from zero:
n = n + 1


This program halts if the input polynomial $P(x)$ has a non-negative integer root. It turns out that this problem is decidable - there is a clever shortcut that determines the outcome of the program. How can we rule out the existence of such shortcuts in general? The proof you describe is one clever way of doing that.

• That's not exactly what I meant. You can (most of the time) easily predict if an algorithm will produce an infinite loop regardless of its input - just by looking at it. A machine cannot - it has to run the algorithm on a given input to find out. – so.very.tired Dec 20 '13 at 10:33
• BTW, thanks for commenting... again. :-) – so.very.tired Dec 20 '13 at 10:34
• Why do you think that the only way a machine can predict whether an algorithm terminates or not is by running the algorithm? That's not at all clear. Here is another suggestion: the machine searches for proofs that the algorithm terminates or doesn't terminate. If there is such a proof, the machine will find it. For all "useful" inputs, this will probably succeed. – Yuval Filmus Dec 20 '13 at 14:17
• This proof you're referring to, is also an algorithm, written by humans - who knows what will be considered as credible proof. I guess I should have been more clear about what I meant. there is know way for a machine to understand, in some point in a loop "well, this process is running long enough now, it must be going to infinity then." of course there are ways to bypass this by creating more and more sophisticated algorithms to prevent infinite loops, but that not where I'm going with it. – so.very.tired Dec 20 '13 at 17:09
• You can define a notion of formal proof which makes perfect sense for computers. For example, you can consider proofs in the sequent calculus from the axioms of ZFC. If you can prove that the program terminates or doesn't terminate, then the computer will find a proof (eventually). – Yuval Filmus Dec 20 '13 at 21:53