In article <firstname.lastname@example.org>, Tal Kubo <email@example.com> wrote: >Matthew P Wiener <firstname.lastname@example.org> wrote: >>>Actually Matthew is claiming much more: that whatever system S (definitely >>>weaker than PA) proves the 0-1 law, >> >>Minor point: I have hedged on whether the 0-1 law would be weaker than PA. >>I think it would be, yes, but it's not particularly important. > >You were emphatic about PA being overkill, but as you say, it's not so >important. What is important is that you've apparently assented >to a specific interpretation of your claim about the consistency >implications of a 0-1 law: > > >>Matthew is claiming that whatever system S proves the 0-1 law, > >>also proves Con(A)-->Con(A+X) for all sufficiently strong > >>"alpha" theories A and all statements X in the "omega" theory of A. > >------------------------------------------------------------------------- >>>Recall that A=ZF was the intended "very plausible upper bound" for this >>>argument. So we are being told that that through a "relatively simple" 0-1 >>>law, a system below PA would somehow acquire a "uniform" way of proving >>>equiconsistencies on the order of Con(ZF)-->Con(ZFC) and much more. >>>Dubious. >> >>How so? It is EXTREMELY WELL-KNOWN that Goedel's and Cohen's arguments can >>be carried through in very weak forms of arithmetic, way below PA. > >This is because Goedel and Cohen's arguments on AC rely on a highly >developed metatheory of a standard known theory ZF. What you're proposing >would amount to an all-purpose PA proof to govern unspecified extensions of >arbitrary (and arbitrarily stronger than ZF) starting theories. PA can >control certain aspects of provability for very specific configurations >such as ZF--ZFC, but in a generic setup by waving a 0-1 law magic wand?? >
In most cases of T |- Consis(T) -> Consis(T+X), the proof is more than just "if there is a model of this, there is a model of that"; one can extract from the proof an effective procedure for converting any deduction of a contradiction from T+X into a deduction of a contradiction from T. This procedure usually isn't complicated; it is easily primitive recursive (maybe Kalmar-elementary). If so, then PRA (Primitive recursive arithmetic) already suffices: PRA |- Consis(T) -> Consis(T+X).