Does the following language do the same thing as PAK?

PAS = PA + schema over Formulas of one variable:
- For all N, for all P:
-- if P proves-in-PAS 'Formula(N+1)', then Formula(N)

(Actually, on second thought, I retract that, you do want the special symbol so that proving 4 > 3 doesn't get you 3 > 3. But now I need to see if the same problem applies to the original logic as soon as you add K=3...)