> It is formalizable, yes; for simplicity, there is an arithmetical > predicate R(n) <=> "n is the least code of a consistent r.e. theory". > And, of course, T_n _is_ consistent; that's true. But "true" is one > thing and "provable in PA" is another... I don't see any grounds > for PA being able to actually _prove_ Consis(T_n)!
Let Th(n,x) be a formalization in PA of the statement "x is a code for a theorem of theory T_n". Let T(x) be the formula (for some n, R(n) and Th(n,x)). Let #false be a code for some provably false statement of PA (say "0=1"). Then in PA we can formalize Consis(T) as follows:
