From: Marina Gotovchits on
On 30 Okt, 22:13, Rupert <rupertmccal...(a)yahoo.com> wrote:
> On Oct 31, 5:50 am, Marina Gotovchits <renessa...(a)gmail.com> wrote:
>
> > > Let WO be the system WKL(0) + the omega-rule. From what's on the
> > > table, as I understand it, WO prowes that (EX)(X is a model of ZF).
> > > Here the quantifier is over sets, and not numbers, of course. The
> > > question is wheter there, in case ZF is consistent, is a closed set-
> > > term A such that WO proves that A is a model of ZF.
>
> > I now realize that SOA of course does not have the kind of closed set
> > terms I was here asking for, so that (EX)(X is a model of ZF) is as
> > much as we can get in SOA. (My questions are motivated from another
> > context.) Anyway, intuitively this says that a model of ZF exists.
>
> > Is the model transitive?
>
> We can prove that a model exists, but we cannot prove that a well-
> founded model exists, for the reasons Aatu has discussed.

I think I see that, (even though the regularity axiom will hold true
in the model...).

If an omega model is not secured, it raises the question whether
minimal models can be obtained using stronger principles like Bar
Induction and Iterated Inductive Definitions beyond ACA.

From: Sergei Tropanets on
On Oct 30, 11:55 pm, Marina Gotovchits <renessa...(a)gmail.com> wrote:
> On 30 Okt, 21:59, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
>
> > Rupert <rupertmccal...(a)yahoo.com> writes:
> > > Assuming that ZF is consistent, in WKL_0+the omega rule we can prove
> > > that there exists a model of ZF. We probably can't prove that the
> > > natural numbers are standard in this model.
>
> > We can't prove in WKL_0 + all arithmetical truths that WKL_0 + all
> > arithmetical truths is consistent, and hence certainly not that ZFC +
> > all arithmetical truths is consistent (which is just another way of
> > saying: ZFC has an omega-model).
>
> I am a bit bewildered at this point. We agreed that if ZF is
> consistent, then an arithmetical sentence CON(ZF) will hold true, and
> so is provable in WKL(0)+the omega-rule(=WO in the following). An
> appeal to the fact that WKL(0) is equivalent, under RCA(0), to Gödel's
> completeness theorem, then licenses the inference that WO proves that
> there is a model of ZF.
>
> OF course, WO cannot prove its own consistency. But is CON(WO) at all
> a well-formed sentence? For a recursively axiomatizable theory like ZF
> we indeed have an arithmetical provability predicate and so can define
> CON(ZF). But it seems to me that we do not have an arithmetical
> provability predicate for WO. So it is not clear to my mind what the
> statement "WO is consistent" should mean in arithmetical terms, and
> how it relates to my starting point with CON(ZF).
>
> In my original query I also related a similar query to the 1-
> consistency of certain strong theories. Let us strengthen this to
> their omega consistency. We may as well concentrate on ZF. Is not OCON
> (ZF) (a statement to the effect that ZF is omega consistent) also
> representable as an arithmetical sentence? If so, will it not produce
> an omega consistent model e.g. in WO? (If it is not so representable,
> there is something crucial in one at points heated discussion between
> Harvey Friedman and Solomon Feferman which I miss out on. Is it that 1-
> consistency is so representable while omega-consistency is not,
> perhaps?)

I think this your bewilderment is the result of applying such a
meaningless notions as "the set of all true arithmetical
sentences" (or "arithmetical truths"). What is this? For sure, even
set theorists working in classical logic can not define what those
words mean. As a result - theories like WO with strange set of axioms.
I think it is more reasonable to talk about decidable arithmetical
sentences in one or another sense.

Sergei Tropanets