From: Charlie-Boo on
On Jun 29, 12:22 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> 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.

Check the earlier papers, actually.

C-B

> 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- Hide quoted text -
>
> - Show quoted text -

From: Charlie-Boo on
On Jun 29, 12:30 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jun 29, 11:18 am, Charlie-Boo <shymath...(a)gmail.com> wrote:
>
>
>
>
>
> > 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.
>
> Enderton proves the soundness theorem. That was my point in that
> particular mention.
>
> > 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.
>
> I need to stop posting with you. You're not listening.
>
> It's not just convential wisdom. Rather, it is a simple exercise
> anyone who knows about the subject can carry out.

Are you talking about using the Axiom of Infinity to derive the
assertion that there is a model for PA? That doesn't do it - it
doen't prove that implies consistency.

Nobody can give me a reference to a ZFC proof of PA. What would
anyone conclude?

"You're just being lazy" - No, guess again.

Didn't you just ask for a reference yourself a minute ago?

C-B

> I have carried it
> out myself. I'm not going to type out my notes for you, because you
> could do the exercise yourself.
>
> > > > 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?
>
> Just take the needed information from Enderton's two books. Then
> perform the proof as a simple exercise.
>
> > > 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.
>
> Just take the needed information and do it as an exercise. I have.
>
> YOU as much as stated the overall outline when you noted how N is
> shown in ZFC and then the axioms of PA proven in ZFC (or whatever
> exactly you said).
>
> > > 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?
>
> All you need to complete the exercise is provided you in Enderton's
> two books.
>
> > > 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?
>
> I really need to stop with you.
>
> MoeBlee- Hide quoted text -
>
> - Show quoted text -

From: R. Srinivasan on
On Jun 29, 8:33 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jun 29, 2:09 am, "R. Srinivasan" <sradh...(a)in.ibm.com> wrote:
>
> We PROVE from ZF-Inf that there IS NO SUCH object that you are calling
> 'D'. (or at least we have not before us a proof that there IS such an
> object). Just adding a constant symbol 'D' and saying whategver you
> want about it does not override.
>
You do not have any such proof. You don't even begin to understand
what I am talking about here. But I have attempted to give an
explanation further down.
>
> And I SHOWED you how to accomplish your axiom without resorting to D.
>
Yes, you did. But there are no issues with defining such a D and it is
very much needed for my purposes in defining a theory of finite sets
in the logic NAFL, as I was trying to explain.
>
> > But this would be controversial and there would
> > still be some ambiguity on whether the existence of infinite sets is
> > ruled out despite our forcing D=0.
>
> > Instead, what I have done in my work is to define D as a class and
> > allow the proposition D=0 in a theory of finite sets F where F allows
> > classes in its language. So according to the classical way of
> > thinking, D would be a set (null set) if infinite sets do not exist
> > and a proper class otherwise.
>
> But "THERE ARE NO proper classes" is a theorem of Y. (Why don't you
> understand this?) Therefore, talk of proper classes in context of Y is
> merely figurative, a figure of speech, for some other actual statement
> in the meta-language.
>
Again you are showing utter inability to parse what I am saying. I was
talking about a theory F which does permit classes, not about the
theory Y. But now let us talk about the theory ZF-Inf. We *can* add D
to the language of this theory and I claim that would entail the
provability of D=0 in ZF-Inf. However despite this fact, there can
arguably can exist models of ZF-Inf in which infinite sets can exist.
D=0 would continue to be true in such models in the same way that in
some set theories in which classes are not permitted, {x: x=x} is
taken as the empty set.
>
> And in this case, you don't even NEED D. I showed you how.
>
Yes, and I agreed with you. But I do need D for my purposes, as I have
explained below.
>
> > But in my logic NAFL, the undecidability
> > of the proposition D=0 in the theory F is a contradiction, and so the
> > conclusion is that D=0 must be provable in F. This would genuinely
> > rule out the existence of infinite sets in the NAFL theory F.
>
> Whatever about "NAFL".
>
If you say so.
>
> > I do not want to allow any explicit references to infinite objects in
> > the language of the theory ZF-Inf.
>
> What does that MEAN? What is your technical definition of "explict
> reference to infinite sets in the language"?
>
It is a phrase in good old English. I am saying that no definitions of
any infinite objects are allowed in the language of ZF-Inf and no
symbol in the language of ZF-Inf represents any infinite set. For
example "the set of PA-sentences" cannot even be defined in the
language of ZF-Inf under this constraint. This is the best I can do
with explanations. That such a language would be legitimate is obvious
to me.
>
> > We can and should deny the
> > existence of infinite sets without explicitly defining any infinite
> > object.
>
> Yes you can! You ALREADY did it with theory Y:
>
> ZF-"Inf'+"~Inf"
>
> That theory entails that every object is finite. And there is no
> definition of any infinite object possible in that theory.
>
OK. Here I want ~Inf to be stated in the form that you mentioned, that
is, every set is hereditarily finite.
>
> > Of course if we admit classes we may allow V_n as a class
> > without committing that it is a set.
>
> You CAN'T do that with ZF-Inf or ZF-Inf+"~Inf" or with ZF-Inf+"every
> set is hereditarily finite" (i.e., your "D=0") and still have a
> CONSISTENT theory.
>
> You have to maks some OTHER MODIFICATIONS.
>
Of course. That is understood.
>
[Big snip]
>
> > Therefore I assert that Y proves
> > ~Con(PA).
>
> WRONG. WRONG. WRONG. I've explained already how you are mixed up about
> this. You are now arguing just by RECLAIMING what you have not proven.
>
> Y proves "no x is infinite".
>
> In the language of Y there is a sentence S such that when S is
> translated into the language of PA (under an interpretation of Y into
> PA) as sentence S*, we have that S* is true in the standard model of
> PA iff PA is inconsistent.
>
I am having trouble parsing your sentence. How can something be true
"in the standard model of PA iff PA is inconsistent" ?????

Are you saying that there is such a thing called the "standard model
of PA" even if PA is inconsistent? Or are you saying that PA is
"really" consistent and its standard model exists even if "PA is
inconsistent" is true?

Anyway, here is what I was claiming. The proof of "No x is infinite"
in Y will translate to a proof of some sentence of PA when we
interpret Y in PA. *That* proof ought to be a proof of the
inconsistency of PA in PA. I do not have the foggiest idea whether
*that* PA-sentence will turn out to be Godels ~Con(PA) or not.

However, in light of what Aatu Koskensilta said, it seems that despite
Y's proof of the non-existence of a model for PA, we cannot conclude
that Y proves that PA is inconsistent, for the implied equivalence
will be provable only in a theory with infinite sets permitted (like
ZF). I have to think about this a little more.
>
> But you have NOT shown that S is a THEOREM of Y.
>
> Just because there is a sentence in the language of Y doesn't entail
> that sentence is a THEOREM of Y.
>
I am referring to the THEOREM of Y that "every set is hereditarily
finite". A proof of the translation of THAT sentence in PA ought to
have been a proof of the inconsistency of PA in PA, unless Aatu's
objection holds.

RS


From: Chris Menzel on
On Tue, 29 Jun 2010 08:56:48 -0700 (PDT), Charlie-Boo
<shymathguy(a)gmail.com> said:
> ...
>> > 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?

"Careless" might be a better or, at least, more charitiable, description.

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

Oh, I'm sure he's an avid sci.logic reader. Unlike you, the MathWorld
folks at least realize that a definition of the operator is needed,
although they only state informally how the operator functions with
respect to the ordinals, viz., 0=∅, 1=0'={0}, 2=1'={0,1}, etc. But note
that doesn't say in general what the operator means when applied to
arbitrary terms, in particular, variables, as in the axiom. The general
definition is:

x' =df xU{x}

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

But *that* N can serve as the domain of a model of PA is not part of its
*definition*, contrary to what you seem to be asserting. That is
something that is proved after the set is defined.

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

You boldly proclaimed "ZFC axiom of infinity = PA induction" at the top
of your little demonstration. So since the two PA "axioms" were the
only things remotely resembling induction, it seems pretty clear that
they constitute your understanding of induction.

From: Chris Menzel on
On Tue, 29 Jun 2010 09:18:59 -0700 (PDT), Charlie-Boo
<shymathguy(a)gmail.com> said:
> 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.

It has been demonstrated in this very thread numerous times, just simply
not to your satisfaction. It is a simple exercise to verify that the
axioms of PA are true in the standard representation of the number
structure in terms of finite von Neumann ordinals. It is a simple
exercise to prove the existence of this representation in ZF. It is a
simple exercise to code languages as sets and formalize basic
first-order model theory in ZF. It is a simple exercise to prove the
soundness theorem for first-order logic. Anyone with with a basic
understanding elementary set theory and mathematical logic can now see
that it follows immediately that ZF proves the consistency of PA. To
work it out in complete, formal detail would be as tedious and frivolous
an exercise as working out the proof that there is a prime number
between 95 and 100 in Principia Mathematica.