From: MoeBlee on
On Jun 29, 7:34 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Transfer Principle <lwal...(a)lausd.net> writes:
> > 1. Is there a proof in ZF-Inf+~Inf that every set is finite?
>
> It appears I once posted a proof. It relies, in an essential way, if I
> recall correctly, on the axiom of replacement.

Right. I reposted it yesterday.

MoeBlee

From: MoeBlee on
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.

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

Ordinarily, 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: Charlie-Boo on
On Jun 29, 11:10 am, Chris Menzel <cmen...(a)remove-this.tamu.edu>
wrote:
> On Tue, 29 Jun 2010 03:16:07 -0700 (PDT), Charlie-Boo
> <shymath...(a)gmail.com> said:
>
>
>
>
>
> > On Jun 28, 10:17 pm, Chris Menzel <cmen...(a)remove-this.tamu.edu>
> > wrote:
> >> On Mon, 28 Jun 2010 04:56:30 -0700 (PDT), Charlie-Boo
> >> <shymath...(a)gmail.com> said:
>
> >> > On Jun 27, 6:31 pm, Chris Menzel <cmen...(a)remove-this.tamu.edu> wrote:
> >> >> On Sun, 27 Jun 2010 10:50:16 -0700 (PDT), Charlie-Boo
> >> >> <shymath...(a)gmail.com> said:
>
> >> >> > ...  ZFC declares that there is a set that satisfies Peano’s
> >> >> > Axioms and defines N to be that set.  
>
> >> >> You have it completely backwards.  The set is defined first,
> >> >> independent of any mention of PA.
>
> >> > So?  
>
> >> So what you said was false.  You said that ZFC defines N to be a set
> >> that satisfies the Peano Axioms.  False.
>
> > > So, to complete the answer to your question: N is never *defined* to
> > > be a set -- or, more exactly, the domain of a model -- in which the
> > > Peano axioms are true.  That *turns out* to be the case after the
> > > set and corresponding model are defined.
>
> > N is defined to be a set that meets the Peano Axioms whether they
> > mention PA or not.  
>
> You seem to use the word "define" in a way that no one else does.

You used the same word, referring to “after the set [N] (is) defined”,
but if you want to change it to something else, then fine. That
doesn’t change the point.

> > You say it "turns out" to be the case.  It turns out because of the
> > answer to my question that you steadfastly refuse to mention: It is
> > done with the ZFC Axiom of Infinity, which merely says that there is a
> > set that models Peano's Axioms.
>
> It simply says no such thing.

Ok, then it is done with the ZFC Axiom of Infinity. That doesn’t
change the point.

> > ZFC Axiom of Infinty = PA Induction
>
> > ZFC: Ex (0 e x ^ Ay e x (Y' e x) )
>
> I guess you mean
>
>   Ex ({} e x ^ Ay e x (yU{y} e x) )

It’s from Wolfram Mathworld http://mathworld.wolfram.com/AxiomofInfinity..html
Do you think that Wolfram is wrong?

> You use the constant '0' and a successor symbol but they are not part of
> the language of ZF.  Nor are the empty set and the operation yU{y} just
> magically identical to the number zero and the successor function,
> respectively.

Tell that to Stephen Wolfram.

> Among the things that are proved when one builds the
> usual model of PA, in fact, are that the empty set and the operation in
> question can serve in these roles.  It's part of what makes the matter
> interesting.
>
> Note more generally that there is no mention of Peano's axioms in the
> axiom of infinity nor is there any reference to the *true-in* relation
> between sentences and models.  There would have to be if the axiom
> actually said "that there is a set that models Peano's axioms".

Where did I say that? I just said that N is defined to be a set that
satisfies Peano’s Axioms. It has to satisfy Peano's Axioms, otherwise
the proof wouldn’t work. Talking about whether we should call it
“define” or whether “Peano’s Axioms” is mentioned has nothing to do
with this fact.

> Why you
> think otherwise is curious.
>
> > PA: 0 e N
> > PA: Ay e N (Y' e N)
>
> So that's what you think induction is, huh?

Where did I say that?

>  That explains a lot.
>
> > Change x in ZFC to N and you get PA.  That's just how the "proof"
> > works.
>
> Well, you've been pointed to many references that would be very helpful
> to you.

How about one in which there is a proof in ZFC of PA consistency?
That is the reference that I asked for.

C-B

- Hide quoted text -
>
> - Show quoted text -

From: MoeBlee on
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'.

> 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.

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.

Just look at Enderton's two books.

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 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.

MoeBlee

From: MoeBlee on
On Jun 29, 8:18 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> MoeBlee <jazzm...(a)hotmail.com> writes:
> > By the way, here's Aatu's proof:
>
> > Theorem (of Z-"ax regularity"-"ax infinity"+"~ ax infinity"):
>
> > Ax x is finite.
>
> You need an F up there, I believe.

Right. Indeed, and as deployed in the proof itself. I had been
pointing that out in an earlier context. My typo of omission.

Should be:

Theorem (of ZF-"ax regularity"-"ax infinity"+"~ ax infinity")

MoeBlee