[FOM] 654: Theory Inspired by Automated Proving 1

[Mario Carneiro]

On Wed, Feb 17, 2016 at 11:27 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> I’m only aware of two convincing implementations of set theory in proof
> assistants. One of them is Isabelle/ZF, which is my own work, and which
> provides a very nice environment for working in axiomatic set theory, but
> not for working in any other domain of mathematics. But notational issues
> cause problems very quickly. A textbook can use the same symbol (+) for
> both ordinal and cardinal addition, distinguishing the two by variable name
> conventions: this isn’t possible in a typeless framework. The system that
> gets it right is Mizar, which has an underlying set theory and a very
> elaborate and impressive soft type theory built above it. No one has
> managed to duplicate this, and Mizar itself, as far as I know, hasn’t been
> updated to be technologically competitive with modern systems.
>

While I don't fault you for not being aware of Metamath, I think it is
quite relevant for this discussion, as it is based on pure set theory. It
is also specifically designed for system simplicity. There is technically
an underlying type system, but only at the most basic level (the only types
are the sets, classes, and wffs, and this is not extensible in practice) so
it is not relevant here.

Metamath also (deliberately) does not support operator overloading, and
there are two techniques for managing this. One is just to use subscripts
and so on, which is used for distinguishing ordinal and cardinal addition
and complex addition. (Here an advantage of the typeless approach is that
the exact same class + can be an addition operation on complex numbers and
its subsets such as the natural numbers.) The other, more general approach
constructs a group structure, and extracts the addition component of the
structure into a variable that resembles a plus sign.

As for types in automation, of course in practice there is a soft type
system that will arise in any system, since all statements of interest will
be restricted to certain sets in any case, and terms will have closure
theorems that mimic the type deductions of a type theory. These are just as
susceptible to automatic derivation as they are in type systems, and
although automation is not nearly as well-developed in Metamath as it is in
Isabelle or Mizar, there is no foundational argument against it in
principle. Thus I do not buy the argument that type theory is a necessary
component for high automation, and the opportunities for mimicking types in
set theory make it so that the only real argument is the philosophical one
"it doesn't feel right that numbers are made of sets", which isn't
well-defined enough to effectively counter.

It all shakes out the same in the end, and I hope that we see more
inter-system translations in the future to validate this viewpoint.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160217/65940175/attachment-0001.html>