home *** CD-ROM | disk | FTP | other *** search
- Newsgroups: sci.math
- Path: sparky!uunet!sun-barr!cs.utexas.edu!usc!wupost!darwin.sura.net!paladin.american.edu!news.univie.ac.at!email!mips.complang.tuwien.ac.at!rz
- From: rz@mips.complang.tuwien.ac.at (Richard Zach)
- Subject: Re: Foundational issues
- Message-ID: <1992Sep14.144632.21623@email.tuwien.ac.at>
- Sender: news@email.tuwien.ac.at
- Nntp-Posting-Host: mips.complang.tuwien.ac.at
- Reply-To: zach@csdec1.tuwien.ac.at
- Organization: Technische Universit"at Wien
- References: <92Sep12.101940edt.47512@neat.cs.toronto.edu> <12SEP199214515040@utkvx1.utk.edu>
- Distribution: na
- Date: Mon, 14 Sep 1992 14:46:32 GMT
- Lines: 78
-
- In article <12SEP199214515040@utkvx1.utk.edu>, dchatham@utkvx1.utk.edu (Chatham, Doug) writes:
- |> In article <92Sep12.101940edt.47512@neat.cs.toronto.edu>,
- |> arnold@cs.toronto.edu (Arnold Rosenbloom) writes...
-
- |> >First the number theory text assumes the Peano Axioms, now if we
- |> >view these axioms as the specification of a particular set, how
- |> >do we know that we have a well defined system. For example, the Peano
- |> >axioms assume the existence of a successor function that behaves in a certain
- |> >way. How do we know there is a subset of NxN which has the required properties.
- |> >
- |> >The other side (set theory) of the coin also presents some problems.
- |> >THat is, the natural
- |> >numbers are 'defined' as 0={}, 1={0}, 2={0,1}, ... , n+1={0,...,n}.
- |> >But this looks like an inductive definition. So how can you make an inductive
- |> >definition (and hope it makes sense) without the natural number system already
- |> >there to prove that you have actually defined something?
- |>
- |> I'm not sure what you mean by "well defined system." However, the
- |> reason we "know" the existence of a successor function is that we ASSUMED it.
-
- When you want to talk about numbers, or at least if you want to
- give an axiomatic foundation for number theory, you have to start
- *somewhere* and the obvious place to do this is by giving
- axioms for the natural numbers. The axiom system of Peano is
- one such system. You do not have to know anything about
- the symbols in the axioms to be able to work with the system,
- in particular you dont have to know that there is a function
- from N to N that behaves like the axioms want it to (ie
- 0 is no successor and two numbers are equal iff their successors
- are equal etc). You can develop a whole lot of number theory
- just using these axioms (though not all of it: *that* is
- G"odels 1st incompleteness theorem).
-
- If you want to know what these axioms talk about, in particular,
- if you want to know if your system is consistent (I assume that
- is what you mean by "well defined") you have to find a *model*.
- And to talk about models, you have to lay your foundations deeper,
- ie you have to go into set theory. Set theory tells you that
- there is a set satisfying the peano axioms, namely the set
- of natural numbers.
-
- If you even doubt that set theory is a "well defined system"
- (which you have every right to do) than you have to prove
- the consistency of set theory. Because of G"odel's theorems,
- you cannot do that *inside* set theory, and this leads to
- an infinite regress. But since most people *believe* that
- ZF is consistent, (almost) noone thinks about these things :-)
-
- |> Unfortunately, according to Godel we cannot prove the consistency of a
- |> number theory including the Peano axioms [without bringing in some larger
- |> formal system whose consistency would be unprovable without . . .ad nauseaum,
- |> ad infinitum]. So we can't prove the successor function won't cause a
- |> contradiction somehow.
-
- Successor is not the problem. You can prove that number theory
- only with successor (even with addition--Presburger arithmetic)
- is consistent, ie "well defined", inside number theory.
-
- And we can even prove the consistency of Peano arithmetic,
- but this proof has to use principles stronger than those
- of Peano arithmetic. G"odel's 2nd theorem does *not* say that we
- cannot prove the consistency of number theory, he says that a
- formal number theory cannot do this.
-
- |> Secondly, to make inductive definitions we need to ASSUME the
- |> existence of at least one inductive set. ZF (Zermelo-Frankel?) set theory
- |> makes this assumption an explicit axiom.
-
- Yes. Do YOU doubt that there is a set of natural numbers?
- Can't you count? ;-)
-
- Oh, BTW: if you post that kind of question in
- sci.logic next time, you'll get more answers.
-
- --
- Richard Zach [zach@csdec1.tuwien.ac.at]
- Technische Universitaet Wien, Institut fuer Computersprachen
- Resselgasse 3/185.2, A-1040 Vienna, Austria/Europe
-