From: Charlie-Boo on
On Jun 27, 12:50 pm, Charlie-Boo <shymath...(a)gmail.com> wrote:
> On Jun 27, 8:21 am, Frederick Williams <frederick.willia...(a)tesco.net>
> wrote:> Charlie-Boo wrote:
>
> > > On Jun 25, 4:58 pm, Frederick Williams <frederick.willia...(a)tesco.net>
> > > wrote:
> > > > Charlie-Boo wrote:
> > > > > point.  Who has proved PA consistent using ZFC?
>
>  > >  >  Also, see Gentzen> >  >  and Ackermann.  Gentzen's proof used far less than full ZFC.
>
> > > References please.  On-line??  Thanks!
>
>  > Gentzen:   Mathematische Annalen, vol. 112, pp 493-565
>
> >     and    Forschungen zur Logik  und zur Grundlegung der exakten
> >            Wissenschaften no. 4, pp 19-44.
>
> “Gentzen's consistency proof "reduces" the consistency of mathematics,
> not to something that could be proved.” – Wikipediahttp://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof
>
> Wiki doesn’t say anything about ZF in its write-up of Gentzen’s proof
> of the consistency of PA!  What happened??
>
> C-B
>
> > Ackermann: Mathematische Annalen, vol 117, pp 162-194.
>
>  > For Gentzen in English see his collected papers edited by Szabo.
>
> $449.94 - and worth every penny of it!
>
> http://www.amazon.com/collected-Gerhard-Gentzen-foundations-mathemati...

Hey Frederick, I bet you $449.94 that Gentzen's book doesn't contain a
proof that PA is consistent, carried out in ZFC. You on? I'll pay
via PayPal or Western Union, and will absorb any delivery charges.

Or do you say things that you don't believe?

C-B

>
>
> >  For an
> > account of Ackermann's proof see Wang, Logic, Computers and Sets, Ch
> > XIV.
>
> > >  >  You may wish to know that ZFC with the axiom of infinity replaced
> > > by
> > >  >  its negation is a model of PA and vice versa.
>
> > > Wow, that sounds cool.  I'll have to think anout that one.  Where can
> > > I read about it?
>
> > I wish I could remember.  Chris Menzel will tell us shortly.
>
> > --
> > I can't go on, I'll go on.- Hide quoted text -
>
> - Show quoted text -

From: William Hale on
In article
<dbebec73-757b-4de5-ae60-d5f6a6ab8830(a)t10g2000yqg.googlegroups.com>,
Charlie-Boo <shymathguy(a)gmail.com> wrote:

> On Jun 27, 5:18�am, William Hale <h...(a)tulane.edu> wrote:
> > In article
> > <ff54cc7d-b23f-4a45-9040-0459145ff...(a)j8g2000yqd.googlegroups.com>,�Charlie-
> > Boo <shymath...(a)gmail.com> wrote:
> >
> > [cut]
> >
> > > If ZFC can't calculate what PA can, how can anyone say that ZFC is a
> > > good basis for doing mathematics - PA is used by lots of
> > > mathematicians.
> >
> > PA is not used by any mathematicians to do algebra, number theory,
> real
> > analysis, complex analysis, topology, or differential geometry. These
> > mathematicians represent most mathematicians. They use ZFC as their
> > axiomatic system.
>
> PA is not used but ZFC is? But ZFC invokes the Peano Axioms carte
> blanche to represent N - so PA is used by ZFC and thus by all of these
> Mathematicians.

ZFC does not invoke the Peano Axioms to represent N. Textbooks may
mention the Peano Axioms when they show how ZFC incorporates what it
deems to be the natural numbers, but this mention of PA is only for
putting things in a historical perspective or to give some motivation
for what is going on in ZFC, but it is not necessary for ZFC to have any
mention of PA in order to develop natural numbers.

A textbook could mention how Euclid developed natural numbers (for
historical purposes or to show similarities etc), but this does not mean
that ZFC invokes the five Euclidean postulates of geometry.

> Good point!
>
> C-B
From: Frederick Williams on
Charlie-Boo wrote:

> �Gentzen's consistency proof "reduces" the consistency of mathematics,
> not to something that could be proved.� � Wikipedia
> http://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof
>
> Wiki doesn�t say anything about ZF in its write-up of Gentzen�s proof
> of the consistency of PA! What happened??

I cannot speak for the Wikipedists, but can you not see that the proof
could be formalized in ZFC?

I don't know what to make of

It "reduces" the consistency of a simplified part of mathematics,
not to something that could be proved (which would contradict the
basic results of Kurt G�del), but to clarified logical principles.

But then that's Wikipedia for you.

--
I can't go on, I'll go on.
From: Frederick Williams on
Charlie-Boo wrote:

> Hey Frederick, I bet you $449.94 that Gentzen's book doesn't contain a
> proof that PA is consistent, carried out in ZFC. You on?

No, but I do claim that it could be formalized in ZFC.

> Or do you say things that you don't believe?

Yes, but I don't think that's relevant here.

--
I can't go on, I'll go on.
From: Charlie-Boo on
On Jun 27, 1:21 pm, ah...(a)FreeNet.Carleton.CA (David Libert) wrote:
> Transfer Principle (lwal...(a)lausd.net) writes:
> > On Jun 26, 7:51=A0pm, Tim Little <t...(a)little-possums.net> wrote:
> >> On 2010-06-26, R. Srinivasan <sradh...(a)in.ibm.com> wrote:
> >> > The theory ZF-Inf+~Inf clearly proves ~Inf ("Infinite sets do not
> >> > exist").
> >> Actually ~Inf does not assert "Infinite sets do not exist". =A0It only
> >> asserts "there does not exist a successor-closed set containing the
> >> empty set".
>
> > This has come up time and time again. I myself have claimed that
> > the theory ZF-Infinity+~Infinity proves that every set is finite,
> > and someone (usually MoeBlee or Rupert) points out that this
> > theory only proves that there's no _successor-inductive_ set
> > containing 0, not that there is no infinite set.
>
> > And every time this comes up, I want to say _fine_ -- so if
> > ZF-Inf+~Inf _doesn't_ prove that every set is finite, then there
> > should exist a model M of ZF-Inf+~Inf in which "there is an
> > infinite set" is true, even though "there exists a set containing
> > 0 that is successor-inductive" is clearly false (assuming, of
> > course, that ZF is itself consistent), just as the fact that ZFC
> > doesn't prove CH implies that there is a model of ZFC in which
> > CH is false (once again, assuming that ZF is itself consistent).
>
> > Yet no one seems to accept the existence of this model M.
>
> > Either this model M exists, or ZF-Inf+~Inf really does prove that
> > every set is finite. There are no other possibilities.
>
> > So let's settle this once and for all. Assuming that ZF is
> > consistent, I ask:
>
> > 1. Is there a proof in ZF-Inf+~Inf that every set is finite?
> > 2. Does there exist a model M of ZF-Inf+~Inf in which "there
> > is an infinite set" is true?
>
> > Notice that exactly one of these questions has a "yes" answer
> > and exactly one has a "no" answer. (Actually, come to think
> > of it, since the base theory is ZF and not ZFC, it's possible
> > that the answer to 1. is "yes" if by "finite" we mean one
> > type of finite, say Dedekind finite, and "no" if we mean some
> > other type of finite. In this case, I'd like to know which
> > types of finite produce a "yes" answer.)
>
> > If 1. is "yes," then I hope that I will never again see a post
> > claiming that ZF-Inf+~Inf doesn't prove that every set is in
> > fact finite. In fact, I'll go as far as to suggest that if 1.
> > is "yes," then those who claim that ZF-Inf+~Inf doesn't prove
> > that every set is finite deserve to be called five-letter
> > insults -- if posters are going to call those who deny the
> > proof of Cantor's Theorem by five-letter insults, then those
> > who deny the proof of "every set is finite" in ZF-Inf+~Inf
> > also ought to be called the same.
>
> > If 2. is "yes," then what I'd like to know is how can I take
> > _advantage_ of this fact? Suppose I want to consider a theory,
> > based on ZF-Inf, which actually proves that an infinite set
> > exists, yet also proves that no successor-inductive set
> > containing 0 exists.
>
> > In the current Tony Orlow thread, there is a discussion about
> > whether TO is defining N+ to be a successor-inductive set. It
> > is possible that the theory that I mentioned above might be
> > useful to discussing TO's ideas.
>
> > But of course, we can't proceed until we know, once and for
> > all, whether ZF-Inf+~Inf proves every set to be finite or not.
>
>   I posted a couple of articles in an old thread related to the
> questions above, I will give references below.
>
>   One issue in all this is how to define  infinite  in the posing of
> the question.
>
>   In usual  ZF  or ZFC,  in the presence of the usual axiom of
> infinity,  we can prove there exists a smallest set having as
> member    emptyset  and closed under  the successor operation
> on von Neumann ordinals.
>
>   (The axiom of infinity does not directly assert the existence
> of such a set.  It asserts directly that there is a set having
> emptyset as memeber and closed under trhe von Neumann successor
> operation.  It does not directly assert there is a smallest such
> set.  But that axiom of infinity together with the separation
> axiom proves as a theorem there is a smallest such set.)
>
>   We then define this smallest such set to be the set omega.
>
>   The usual definition of finiteness in ordinary ZF or ZFC
> is having von Neumann cardinaity a member of omega.  Infinite
> is defined as not finite in that sense.
>
>   These definitions rest on the axiom of infinity itself, so
> it at least bears some discussion whether to try working with
> this definition or some alternatives.
>
>   One alternative pair of definitions would be  Dedekind finite
> and Dedekind infinite.  See my references below for more details.
>
>   In my references below I also give another definition of finite,
> not presupposing the usual axiom of infinity.
>
>   With these definitions, we can get various rephrasings of the
> question, that could be more suitable for this theory.
>
>   My articles especially concentrate on Dedekind finite.  But
> from the discussion there you can also extract information
> about the other cases.
>
>   The articles:
>
> [1]     David Libert     "Axiom of Infinity (AxF) in ZF"
>         sci.logic        Aug 26, 2003
>        http://groups.google.com/group/sci.logic/msg/8b55a452fdf641d9
>
> [2]     David Libert     "Axiom of Infinity (AxF) in ZF"
>         sci.logic        Aug 29, 2003
>        http://groups.google.com/group/sci.logic/msg/9417324657c5b242

Where is ZFC used to prove that if a system has a model then it is
consistent?

C-B

> --
> David Libert          ah...(a)FreeNet.Carleton.CA- Hide quoted text -
>
> - Show quoted text -