[FOM] 622: Adventures in Formalization 6

[Larry Paulson]

The assumption that everything is a complex number is fine when it is true, but it has a number of drawbacks. You have a problem as soon as you want to work with something that isn’t a subset of the complex numbers, such as the extended reals or polynomials. It seems unnatural to state that the cardinality of a set is a complex number. And then what is the status of the “real” natural numbers, which are surely present somewhere unless they are actually constructed to be a subset of the complex numbers, which would be even stranger? 

To anybody familiar with set theory, the natural numbers are precisely the finite ordinals, and their obvious generalisation as regards cardinality would be to allow transfinite ordinals for infinite cardinalities. There is no role for the complex numbers here.

To a mathematician, if there is an injection from one set into another, treating the former set as if it were simply a subset of the latter comes naturally. And so when necessary, we can indeed regard the cardinality of a set “as” a complex number, but that is different from asserting that natural numbers simply are complex numbers.

Formalising such notions is not going to be easy.

Larry Paulson


> On 30 Sep 2015, at 13:51, Freek Wiedijk <freek at cs.ru.nl> wrote:
> 
> These issues are caused by too weak a type system.  With
> the soft type system of Mizar, and the way it is applied in
> the Mizar mathematical library, there are no problems of
> this kind.  There the natural numbers are a subtype of the
> integers are a subtype of ... are a subtype of the complex
> numbers.  Subtraction is defined on the complex numbers,
> but the type system knows that 1 is a natural number and
> that if N is a natural number, then N-1 will be an integer.
> If you have a proof that N > 0, then you can change the
> type of N-1 to natural number too.
> 
> Relatedly, Mizar shows that there is no conflict between
> "working in raw ZFC" and a "typed formalism".  In Mizar
> everything is a "raw ZFC" set, while everything is fully
> typed as well.