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.

I just read the proof for it, that made me wonder about something.
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.