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

From: Charlie-Boo on
On Jun 29, 11:56 am, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jun 29, 8:06 am, Charlie-Boo <shymath...(a)gmail.com> wrote:
>
> > On Jun 29, 8:28 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
>
> > > George Greene <gree...(a)email.unc.edu> writes:
> > > > I really don't think that the model existence theorem is going to leap
> > > > out at him here.
>
> > > Pretty much any elementary text contains an account of the set theoretic
> > > construction of the various number systems.
>
> E.g., Enderton's 'Elements Of Set Theory'.
>
> > > It's a trivial exercise to
> > > verify the axioms of PA hold in the structure of naturals.
>
> The only slightly non-trivial part is the induction schema, but it
> falls right into place if one simply starts to do it.
>
> > >Combined with
> > > the soundness of first-order logic this immediately yields the
> > > consistency of PA.
>
> Soundness, e.g. demonstrated in Enderton's 'A Mathematical
> Introduction To Logic'.

Enderton only makes a comment that ZFC can prove the consistency of PA
(pg. 270) with no details given.

Is this why people are up in arms claiming that ZFC can prove PA
consistent, even with no references to it - because it is conventional
wisdom among academia? Then you really do have a mess - a claim that
nobody has ever demonstrated.

> > Can that be carried out in ZFC?  
>
> YES!
>
> > Who has?
>
> I have! Many people have.
>
> But am I going to type ALL the formulas that go into this? No, I'm
> not, since I'm not being paid for that kind of thing.

How about telling me the title of a book or article in which PA is
proved consistent using only ZFC?

> If you wish to think I'm merely claiming that I've done such proofs,
> then fine, you may believe as you wish. But, on the other hand, if you
> wish to do just a basic investigation to see how you could do such a
> proof yourself, then you only need to read a basic textbook in set
> theory and one in mathematical logic.

I've read numerous but none have a proof of PA consistency using only
ZFC.

> Just look at Enderton's two books.

Not there.

> If you wish to consider that evasion, then so be it. But a reasonable
> person would understand that when such basic material is in the basic
> textbooks of the subject,

Then why can no one (including yourself) name one?

> then posters may be reasonable in not
> peforming the labor of typing out of textbooks when the person
> inquiring could just get a book himself and read it.

How can I do that when the only references are bogus?

C-B

> MoeBlee

From: MoeBlee on
On Jun 29, 11:01 am, Charlie-Boo <shymath...(a)gmail.com> wrote:
> 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.

It's not itself a mathematical assertion. It's an assertion about how
mathematicians write and speak.

By 'ordinarily', I would include the journal articles, books,
textbooks, and lectures given by mathematicians working in classical
mathematics. I've never seen one of those that consisted merely of
displays of purely formal derivations in ZFC. Rather, the proofs given
consist of combinations of mathematical symbols and English such that
said proofs can be formalized in ZFC.

If you read a good book on first order predicate calculus then a good
book on set theory, you will understand. I can't impart all of the
knowledge of a couple of books in a few posts.

MoeBlee