What's the "real" reason that IP=PSPACE is non-relativizing? IP=PSPACE is listed as the canonical example of a non-relativizing result, and the proof for this is that there exists an oracle $O$ such that ${\sf coNP}^O \not\subseteq {\sf IP}^O$, while ${\sf coNP}^O \subseteq {\sf PSPACE}^O$ for all oracles $O$.

However, I've seen only a few people give a "direct" explanation for why the ${\sf IP} = {\sf PSPACE}$ result does not relativize, and the usual answer is "arithmetization". Upon inspection of the proof of IP=PSPACE, that answer isn't false, but it isn't satisfactory to me. It seems that the "real" reason traces itself back to the proof that the problem TQBF - true quantified boolean formula - is complete for PSPACE; to prove that, you need to show that you can encode configurations of a PSPACE machine in a polynomial-sized format, and (this seems to be the non-relativizing part) you can encode "correct" transitions between configurations in a polynomial-sized boolean formula - this uses a Cook-Levin-style step.

The intuition that I've developed is that non-relativizing results are ones that poke around with the nitty gritty of Turing Machines, and the step where TQBF is shown to be complete for PSPACE is where this poking around happens - and the arithmetization step could've only happened because you had an explicit boolean formula to arithmetize.

This appears to me to be the fundamental reason that IP=PSPACE is non-relativizing; and the folklore mantra that arithmetization techniques don't relativize seems to be a byproduct of that: the only way to arithmetize something is if you have a boolean formula that encodes something about TMs in the first place! 

Is there something I'm missing? As a subquestion - does this mean all results that use TQBF in some way also do not relativize?
Any answer to a question of the form, "What is the real reason that..." will necessarily be somewhat subjective.  However, for the particular case of IP = PSPACE, I think that a pretty good case can be made that arithmetization is indeed the key, by observing that while IP = PSPACE does not relativize, it does algebrize in the sense of Aaronson and Wigderson.  As they explain in their paper, roughly speaking, a complexity class inclusion ${\cal C} \subseteq {\cal D}$ algebrizes if ${\cal C}^A \subseteq {\cal D}^{\tilde A}$ for all oracles $A$ and all low-degree extensions $\tilde A$ of $A$.  In particular, they show that the inclusion PSPACE $\subseteq$ IP algebrizes, even though it doesn't relativize.


  The intuition that I've developed is that non-relativizing results are ones that poke around with the nitty gritty of Turing Machines


This is not a bad intuition, but I think that the Aaronson-Wigderson result shows that the IP = PSPACE proof pokes around in a rather limited way, and certainly not in a sophisticated enough way to prove P $\ne$ NP, since Aaronson and Wigderson also show that non-algebrizing techniques will be required to separate P from NP.