Re: Reals without infinity

From: Norman Megill (nm_at_nospam.see.signature.domain.invalid)
Date: 11/02/04 

Date: Mon, 01 Nov 2004 22:14:45 -0500

Chairman of the Ozzy Osbourne Appreciation Society wrote:

> joshp wrote:
>
>> In article <ba7dcfd7.0410301311.6376feb3@posting.google.com>,
>> Chas Brown <cbrown@cbrownsystems.com> wrote:
>>
>>> It seems somewhat like the idea of "proper classes"; I specify the
>>> "class" of integers by specifying a property, without asserting that
>>> the resulting collection of "all integers" actually exists as a set.
>>
>>
>>
>> Yes.
>> For a fully-worked out formal proof that the class of natural
>> numbers can be constructed in ZF without the axiom of infinity, see:
>> <http://us.metamath.org/mpegif/peano1.html> through
>> <http://us.metamath.org/mpegif/peano5.html>.
>
>
>
> That theorem doesn't prove the existence of the naturals, but says
> that if S is a set which includes 0 and is closed under the successor
> operation, then the set of naturals (omega), is a subset of S.
>
> How do you prove the existence of sets which satisfy that
> theorem (withut AoI) ? Also, how do you get omega without
> the axiom of infinity?

The theorem peano5 is shown using class notation, where class variable 'A'
is a shorthand for {x|phi(x)} that may or may not exist as a set. peano5
is basically mathematical induction, and a translation of it to a theorem
scheme version is shown here:

   http://us.metamath.org/mpegif/findes.html

findes is derived from peano5 and is also proved without the AoI. It
just says that if a property phi(x) holds for 0 and also holds for x+1
when it holds for x, then it holds for all x in omega. "x in omega" is
a class shorthand for "x has the property of being a natural number",
and we don't need omega to exist as a set to state and prove this.

The Metamath derivation is very similar to that in Takeuti/Zaring's
_Introduction to Axiomatic Set Theory_, which also derives Peano's
postulates (p. 42) without AoI (which is first introduced on p. 43).
Metamath's use of class variables to represent theorem schemes follows
T&Z very closely (including the use of upper case letters for class
variables and lower case for set variables). A difference in the
Metamath derivation of Peano's postulates is that it also avoids the
Axiom of Regularity (which T&Z's does not avoid).

Note that the definition of the class omega
http://us.metamath.org/mpegif/df-om.html that Josh pointed to may seem
kind of bizarre, but we need to do that to avoid the AoI. Later, when
AoI is introduced, we prove that this equals the standard definition as
the smallest inductive set in http://us.metamath.org/mpegif/dfom2.html
(which needs the AoI to make any sense). 

-- 
Norm Megill  nm at alum dot mit dot edu

Relevant Pages

  • Re: Largest Set in ZFC?
    ... I think the reason ... We can derive omega from any set that satisfies AoI. ... set satisfying AoI, I see no reason to assume any ...
    (sci.logic)
  • Re: Largest Set in ZFC?
    ... there is no theoretical reason why such a set X could not be ... AoI says a set exists. ... set satisfying AoI, I see no reason to assume any ... Your argument suggests omega is a model of ZF. ...
    (sci.logic)
Loading