Wei Dei asked me in email:

Still looking at the proof but here's a question for you in the mean time. Can you think of any problem examples which can't be solved by a quining approach, but can be solved by parametric polymorphism?

Good point and I don't have an answer yet, but while thinking about it it's occurred to me that AI_Q2 with PA instead of PA(n) might be equivalent to Giles' idea.

(The PA(n) stuff in your definition of AI_Q2 doesn't seem to me to add much to the idea -- it's obviously more powerful than using PA, but using PA(omega) is obviously more powerful than using PA(n), so. [ETA: cf. also this discussion.])

If the two really are equivalent, then Giles' idea seems to me to make clearer what is actually happening, and it feels to me like an instance of the parametric polymorphism trick -- maybe my version just isn't the best way to apply the trick to AI. So if I can't quickly find an example where my version does better, I think maybe I'll just table the issue, keep both versions in mind, start working on the next slightly more complex toy problem, and see what turns out to be useful...

[By "quickly find", I mean in much less than 3^^^3 steps.]