[FOM] 622: Adventures in Formalization 6

[Freek Wiedijk]

Hi Larry,

>The first complication is that we already have to decide
>whether N denotes an integer or a natural number, even if
>we have the explicit assumption N>0.
[...]
>Now let’s confine ourselves to the natural numbers. The
>next question is whether N-1 exists.

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.

>And that’s before we even get to the question we started
>with, namely proving that no injection exists. A formal
>argument isn’t difficult, but requires a certain amount
>of technical skill that seems way out of proportion when
>the conclusion is so obvious.

That this is really "obvious" is not obvious to me.
The Banach-Tarski "paradox" and Hilbert's "paradox" of the
grand hotel and so on show to me that it's more that we
are familiar with facts like this, than that we immediately
_understand_ why this is the case.

I also think that the formal definitions of the notions
involved often introduces this kind of complication, but that
once one has proved some basic facts about these notions,
one is back in a world where these things are "obvious".

For instance, with the definition of natural numbers as
the cardinalities of the finite sets, commutativity of
multiplication doesn't need the complicated inductive proof
that many people seem to take to be "the" proof of this fact.
Then this follows from the obvious bijection between A x B
and B x A.

Freek