From: Charlie-Boo on
On Jun 29, 11:48 am, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jun 29, 7:58 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
>
> > Charlie-Boo <shymath...(a)gmail.com> writes:
> > > How about when you said that Gentzen proved PA consistent using ZFC?
>
> > No one ever proves anything using ZFC in the sense of producing formal
> > derivations. Rather, they prove mathematical theorems using mathematical
> > principles formalized in ZFC. By certain elementary considerations we
> > know the formalizations of such theorems are formally derivable in ZFC.
>
> One quibble: There are people who do produce (even if only exercises)
> displays of certain formal ZFC derivations, as well as those who
> generate such derivations with computer programs, etc.

That's right - or so goes the party line. It's not a quibble - it
contradicts his "No one" claim.

> Other than that, I think what you wrote is a well stated needed
> summary that should be part of a standing FAQ:
>
> Ordinarily,

What do you mean by "ordinarily"? When would it be ordinary and when
is it no? If this is well stated, then that should be well defined.

C-B

> mathematicians "prove mathematical theorems using
> mathematical principles formalized in ZFC. By certain elementary
> considerations we know the formalizations of such theorems are
> formally derivable in ZFC."
>
> MoeBlee

From: MoeBlee on
On Jun 29, 8:27 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> MoeBlee <jazzm...(a)hotmail.com> writes:
> > In the ordinary context, EVERY theory is infinite. Every theory is an
> > infinite set of sentences.
>
> So in a theory with no infinitary objects we need to adopt some more
> suitable representation for theories. A standard choice in case of PA,
> say, is to consider indices of Sigma-n sets of sentences for some n.

I don't know much about that, but I trust your knowledge. So then we
would need to adjust all of Srinivasan's remarks too in that way.

MoeBlee

From: MoeBlee on
On Jun 29, 9:16 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Charlie-Boo <shymath...(a)gmail.com> writes:
> > Ok.  What is the reference to the proof in ZFC of PA consistency doing
> > it that way?
>
> It's in Shelah's _Cardinal Arithmetic_ p.3245 - 4325238532. Basically,
> you just do a triple-fold transfinite recursion over a coherent extender
> sequence to obtain a suitable premouse, and iterate the upward Mostowski
> collapsing lemma a few times. To remove the extendible cardinal
> introduce some Aronszjan trees using Sacks forcing.

Why, you nasty boy.

MoeBlee


From: MoeBlee on
On Jun 29, 10:25 am, Charlie-Boo <shymath...(a)gmail.com> wrote:
> On Jun 29, 10:55 am, MoeBlee <jazzm...(a)hotmail.com> wrote:
>
> > On Jun 28, 9:07 pm, Charlie-Boo <shymath...(a)gmail.com> wrote:
>
> > > On Jun 28, 12:24 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> > >  > And it's easy enough to see that if a theory has a model then that
> > >  > theory is consistent.
>
> > > Is that an axiomatic proof in ZFC?
>
> > Plain Z-regularity proves that if a theory has a model then the theory
> > is consistent. It's quite simple; you would come up with it yourself
> > on just a moment's reflection.
>
> Sorry, but I don't know what proof you have in mind, so I can't
> determine how the Axiom of Regularity would play a role.

It DOESN'T play a role, which is why I took it out. In other words, we
can prove in Z set theory even without the axiom of regularity
(possibly without certain other axioms? but I've never done such
detailed bookkeeping, as my only claim is that Z-R is SUFFICIENT).

As to the proof. Would you just TRY to do it in your mind one time? If
you still can't see it, then, if I'm feeling generous, I'll outline it
for you. As to showing an exact sequence of primitive formulas of the
language of Z, no, that's just a chore. We don't do that. Instead we
study enough first order logic so that we know how to convert informal
mathematical arguments into a primitive language and to see (by taking
progressively larger and larger chunks of argument) how one would
formalize into primitive language if one had to do such a thing; but
actually writing the pure formal primitive formulas is not required
for purposes of mathematical communication among adequately informed
people.

If you wish to take that as evasion, then so be it. Meanwhile, though,
I have trained myself to see how to formalize, as have many other
people with whom I may talk about these matters; I'm not going to
perform unpaid labor of typing formula after formula for you, when you
could just as easily see that it can be done if you only studied a
book on first order logic and one on set theory.

> What is the proof and how is Regularity essential?

You're mixed up. Regularity is NOT needed. That's why I put Z-
regularity, which means "Z without the axiom of regularity".

MoeBlee
From: MoeBlee on
On Jun 29, 10:42 am, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jun 29, 6:57 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
>
> > Without the axiom of infinity we can't prove that if a theory has no
> > model it is inconsistent. Indeed, we can prove in ZF-Inf+~Inf that some
> > consistent theories have no model.
>
> Under the ordinary definition of 'theory' (T is a theory <-> T is a
> set of sentences closed under entailment), and with the usual kind of
> languages and systems we're talking about here, in ZF-Inf~~Inf, we
> prove "there does not exist a theory".
>
> Of course, under some possible wider definition of 'theory' (so that
> there are theories that aren't infinite (i.e. are not an infinite set
> of sentences)), then something else may hold about theories.

Note: This was posted before I saw your remark about workaround
involving Sigma-n etc.

By the way, would you recommend a good (hopefully, fairly easy)
reference on the workaround you mentioned?

MoeBlee