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?