Only if we redefine PA(n) so that e.g. PA(3) is defined in terms of a PA(.) schema and contains an axiom schema stating provable(PA(3), ‘x’)->x; and then redefine PAK accordingly.
But that’s not a redefinition—that was the definition! [ETA: except you need PA(2) instead of PA(3) in the provable(_,_) predicate, of course.]
But that’s not a redefinition—that was the definition! [ETA: except you need PA(2) instead of PA(3) in the provable(_,_) predicate, of course.]