@FedorPakhomov: I do not understand your perspective. Unbounded applications of Powerset contribute strength only if you have other strong assumptions such as impredicative Specification and Replacement. How can we 'blame' Powerset for that increase in strength if the real issue is with impredicativity? I know Powerset is not predicative, strictly speaking, but it's not as bad as unbounded quantification over the universe. Also, for you to use proof-theoretic strength as a gauge, you would need to state the p.t.o. of KP(P) and show that it is intrinsically comparable to that of ZFC...

@FedorPakhomov: Why do you consider KP(P) to be strong? It does not have any replacement but simply has inbuilt power-set, which is arguably the correct way to axiomatize bounded ZF.

@PeterLeFanuLumsdaine: Ah sorry I misinterpreted your comment. I had read it as "it { is much less interesting than the question of work that is only debatably mathematics } but { is clearly successful as something }". XD

@PeterLeFanuLumsdaine: What exactly was it successful at? Note that it is easy to bury a fatal logical flaw in hundreds of pages of proof, in which every other line is correct, but it's hard to figure out the flaw if it is not formal enough. Worse still if the purported proof itself uses something that sounds like moving goalposts (""re-initialization" of (mathematical) objects, making their previous "history" inaccessible")...

Hello! You may be interested in including this as an example of "some academic mathematical interest in 'bible codes'".

@TimothyChow: That's right; my P^0 was exactly your P[T^∅]. And yes you could solve the issue by making very clear (to students) that P is merely abbreviation for "P^0". The more radical alternative I suggested was just a fun way that allows us to actually retain the usual appearance of these notations except for changing "=" to "≡". XD

Another possible solution is that P and NP and other such terms should be defined as models(!) rather than complexity classes, and then the question of equal classes must be expressed differently, say via "P ≡ NP". It is then clear that it may be that P ≡ NP but P^A ≢ NP^A for some A, just like 6 ≡ 10 (mod 4) but 6/2 ≢ 10/2 (mod 4).

Hmm, I don't like $P_{T^A}$ even more. It doesn't solve the issue you raised... The reason I suggested "P^0" is that as long as you think of "P" as the base model and "P^A" as the result of adding "A" to the base model "P" to get a complexity class, then everything is fine, since "^0" is equivalent to no oracle. Unfortunately, "^0" is really cumbersome.

Do you have a preferred solution to this? What about P^0 and NP^0?

[cont] Define a tower to be a function f on some W[<m] such that f(k) is the next level after { f(j) : j∈W[<k] } for each k∈W[<m]. What you want is the union of all such towers, but the iterative conception cannot generate all the towers; you cannot justify a generation process that is long enough for this.

@Goldstern: Just because we can write down a ZFC-based definition of V[W] for any well-ordering W does not imply that it makes philosophical sense. This is the same reason that writing down an impredicative definition does not automatically make philosophical sense. The iterative conception can philosophically somewhat justify low levels of the cumulative hierarchy, but simply fails to justify the existence of V[W] when W is too long. [cont]

@NateEldredge: Always reminds me of Chopra and Derrida.