4
$\begingroup$

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!

  • 1
    O$n$e tech$n$ique is to show that we can define the truth of the formulas for finite level of arithmetic formulas containing that su$b$set 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.2012-08-03

0 Answers 0