K was just said to be a constant symbol, but fine.

PA_K is supposed to be a new name, not some vector PA indexed by K. But that's just notation, and I agree it was a bad choice.

PAK has just been defined, allegedly, but if PA(K) != PAK then I have no idea what PA(K) is, for it was not defined.

PA(.) is a function that takes a number and returns an axiom system (formalized presumably in the form of a recursive enumeration the axioms). On the metalevel, writing PA(K) makes no sense, since you can only apply PA(.) to a number, and on the metalevel, K doesn't denote a number, only a symbol.

However, you can formalize the function PA(.) in the language of Peano Arithmetic, and if you extend that language by a constant symbol K, you can apply this formalized version of the function to this constant symbol. PA_K is Peano Arithmetic (in the language with K) extended by the axiom schema "If PA(K) proves 'C', then C." Here C ranges over the statements of the base language, and 'C' is its Gödel number (written as a unary literal). PA(K) is the object-level recursive enumeration given by the formalized function PA(.) applied to the constant symbol K; it should be standard that given a recursive enumeration of axioms, you can formalize in the language of PA the assertion that a particular number ('C') is the Gödel number of a theorem that follows from these axioms.

I don't see how you can have a constant language, containing one constant symbol, that becomes equal to PA(SSS0) the moment you add one axiom that says SSS0=K.

[Nit: A language cannot be equivalent to a proof system, but I assume that you can't see how you can have a proof system P in the extended language that becomes equivalent to PA(SSS0) the moment that axiom is added.] That challenge is trivial: let P be the set of axioms {"SSS0=K implies A" | A an axiom of PA(SSS0)}. I'm doing something different, but still.

Would anyone care to write out a concrete example of what this language is supposed to do when generating new AIs? As it stands I can't visualize the language itself.

I think if the above didn't help, it might be more helpful for me to first do a writeup of my now-hopefully-fixed proof, since the new version is simpler and IMO provides much better intuition (I at least now feel like I understand what's going on here in a way that I didn't quite before); I'll have to replace PA_K by yet another proof system, and I'll make my metalanguage more explicit about quoting/unquoting when writing it up, so it might be more useful to have that as the starting base before digging into details.

ETA:

Details are often important in reflective reasoning, I've found. In particular there are questions like whether the expression (K-1) can appear in a proof, and so on.

The more precise metalanguage will hopefully also help with this.