[FOM] Formalization Thesis

[Freek Wiedijk]

Timothy:

>I'm presuming that Mizar does encode natural numbers using
>von Neumann ordinals, and has some set-theoretic definition
>of addition.

That's correct.  The definition of the set of natural
numbers NAT is "the first non-empty limit ordinal", and
addition on natural numbers is a special case of addition
on ordinal numbers.

By the way, in Mizar you can have multiple alternative
definitions, where Mizar then checks that these variant
definitions are equivalent.  This means that one can add
the following nice definition of addition on natural numbers
to Mizar:

  definition let n,m be natural number;
    redefine func n + m -> natural number means
      for X,Y being finite set st
        card X = n & card Y = m & X /\ Y = {}
      holds card (X \/ Y) = it;
  end;

It says that n + m is the unique number that is the
cardinality of the union of disjoint sets of cardinality n
and m.  (To be allowed this definition one needs to prove
that indeed that number does not depend on the specific
X and Y.  Mail me if you'd like to see the details of
that proof.)

To me this seems the "right" definition of addition
of natural numbers, which doesn't need anything as non-
intuitive as recursion.

>If we were to clarify it as I did, by running Mizar and
>asking them if they believe that Mizar verified that 2 +
>2 = 4, then I would guess that most of them would vote
>that Mizar did in fact verify that 2 + 2 = 4.

I'm not sure.  Mizar does treat this kind of basic arithmetic
specially, not reducing it to set theory, but instead just
verifying it using machine arithmetic.  So your "man in
the street" might object that Mizar didn't _really_ check
the correctness of this statement.

Now in HOL the proof of 2 + 2 = 4 _is_ checked all the way
down to the logic, so there that objection wouldn't apply.
But then again in HOL the definition of natural numbers is
a bit less natural than in Mizar.  (It uses the Hilbert
choice operator to define the natural numbers from the
infinity axiom.)

Freek