From: rz@mips.complang.tuwien.ac.at (Richard Zach)
Subject: Re: Foundational issues
Reply-To: zach@csdec1.tuwien.ac.at
Organization: Technische Universit"at Wien
Distribution: na
Date: Mon, 14 Sep 1992 14:46:32 GMT

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