FOM: Reply to Trybulec on MIZAR project

[Joe Shipman]

>Still, I believe that it is more than suggestion. Actually I am
convinced (**)
>(not certain) that the formalization of the whole published mathematics

>is (virtually) possible.

>With two reservations:

>1. I doubt if it can be done with Mizar as it is now. (***)
>   The further development of the language is necessary. However,
>   most of the problems related seems to be rather linguistic ones
rather
>   than logical.

Can you be more specific?

>2. There are mathematical papers that hardly are formalizable.

>  - Some of them use strong geometrical insight
>    and some facts in them are not proved, but a picture is provided
instead.
>    For instance, we need two representation of a polyhedron, one
>    to prove that it is embeddable in E^3, just draw a picture, the
other
>    as a CW-complex to prove homotopy properties. And because the fact
>    that it is the same polyhedron (up to the homeomorphism) is easy
>    to see, so it is not proved.

This is exactly the kind of obstacle to formalization I was talking
about last month.  Have you seen my two examples?  (Theorem that
equal-area-polygons are cut-and-paste equivalent, non-cancellation
theorem for knots)

>     With the (computer generated) movies one can use the visualization

>    even for much more complicated arguments.

So you reduce the proofs to a "computer-checkable" piece plus a
"visualizable" piece?  This is very interesting.  Please say more, and
review the discussion about visual proofs starting around February 20th.

>The time needed for formalization is extremely difficult to estimate.
>   Proving Hahn-Banach theorem took 3 days, if I recall. On the other
>   hand the proof of the Jordan curve theorem we started in 1991 and
>   as yet it is proved only for polygonal curves (actually a special
case:
>   for polygons with edges parallel to axes).

Surely it is easy to prove the general polygonal case from this by
replacing each slanted edge with a suitably fine staircase?  (Actually
you should cut each edge in half first, because only one of the two
possible directions to start the staircase is guaranteed to be available
at each vertex, and may be incompatible with the available choice at the
other end, unless you bisect the edge so you can "cross over" at the
midpoint.)

> When we have defined a function, and from the definition is obvious
>   how to compute it, we do not prove that it is recursive (I owe this
>   example to Staszek Krajewski). And the proof may be very long and
>   tedious.

This is funny.  I said this on March 1:

an argument "by Church's thesis" that an
apparently effectively calculable function is recursive is like an
argument "by
Zermelo's thesis" that an apparently proved theorem is derivable from
the ZFC
axioms.  Logicians use this "argument" all the time.  Similarly,
Church's thesis
itself is justified because every time we have tried to eliminate the
appeal to it
by finding a real algorithm we have succeeded; I am pointing out that
"Zermelo's
thesis" doesn't have quite the same level of justification because it
seems much
more difficult to exhibit the desired ZFC-proof than the desired
algorithm in the
earlier example.

and later the same day:

I was only talking about the *possibility* of converting the proof
to sentential form -- the point is to convince yourself of the
possibility.
In my analogy with Church's thesis, this would correspond to writing
down
every quadruple of an actual Turing machine, a stage which also never
needs to
be reached when convincing oneself that a function is recursive.  My
distinction between the two situations is that going all the way down to
the
Turing machine specification, while cumbersome, is quite a bit more
feasible
than going all the way down to a ZFC-FOL proof (even allowing
abbreviations).
Furthermore, we even have tools (compilers and interpreters to reduce
high-level computer languages like LISP to register machine code, which
is
easily translatable to Turing machine code) that mechanize this process
very
nicely, while the technology of machine-aided proofs is much more
primitive.

Andrzej, the technology exists to completely formalize algorithms as
Turing machine programs from LISP code -- you should build this into
MIZAR!  Then you just need a good programmer and it won't be difficult
to prove the functions are recursive.  (Actually, it will be trivial to
prove the functions are partial recursive because all Turing machine
programs are partial recursive; but one could either use a restricted
programming language that only allowed primitive recursion or else add a
"clock" with a provably recursive running time to get total
recursiveness.)

-- Joe Shipman