# Cutest proof that PA proves its finitely axiomatised subtheories are consistent?

Back in 1952, Mostowski proved that PA proves the consistency of its finitely axiomatised sub-theories.

Any pointers to particularly nice later proofs of this lovely result? Or indeed particular nice presentations of the same basic proof idea? Thanks!

-
One technique is to show that we can define the truth of the formulas for finite level of arithmetic formulas containing that subset and then use induction on the truth predicate for them over the size of the proofs to show that the final formula in a proof is true. Obviously we also need to prove cut-elimination for proofs of that formulas in that finite level. –  Kaveh Aug 3 '12 at 23:43