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!