In article <5nn10b$hdb@drn.zippo.com>, Daryl McCullough <daryl@cogentex.com> wrote: >kubo@abel.harvard.edu (Tal Kubo) says... > >>C is not assumed to be recursively enumerable, so it need not have a code. >>Instead, C is some definable set of sentences, and for each of its >>sentences X, the claim is that A proves relative consistency of A+X. >>As you note, the correct conclusion is only that A proves >> >> (Con(A) and (X in C)) --> Con (A+X). > >I agree. Therefore, Matt's conclusion that C has no greater consistency >strength than A doesn't seem warranted (regardless of what 0-1 laws apply >to C). > >>Definability alone in no way limits the consistency strength of C's >>statements. > >Right. That's what I thought. > >>For instance, PA can define the set of sentences X that >>give consistent extensions PA+X, and such X can be arbitrarily strong.
On the other hand, definability bounds on the _elements_ of X make themselves felt if we aim for more than consistency results. E.g. if, say, PA + Y is a consistent extension, and all formulas in the set Y are Sigma-n for some fixed n, then PA + Y cannot prove Reflection for PA (" phi provable in PA => phi"). Consis() is just Reflection for Pi-1 phi.
So some jobs require arbitrarily complicated formulas. Induction in PA, or Replacement in ZF, are stronger than any infinite set of their instances, if the latter has a bound n. (Because PA proves Reflection for the Predicate Calculus). And sometimes they are not strong enough anyway.
Presumably we are interested in proving more than just Pi-1 sentences. Otherwise, PA is overkill. No need to invoke it; we can do as well in PRA (Primitive Recursive Arithmetic) + Consis(PA)... The consistency asser- tion in a sense carries the full force of the theory for level Pi-1. But we usually need to go way beyond that.
