[FOM] Harrison Advocates ZFC (tweaked)

[Lawrence Paulson]

> I am proposing ZFC with urelements and free logic as the NEUTRAL
> UMBRELLA. Various factions can easily work smoothly within this
> Neutral Umbrella, and even probably almost compatibly.


I'd like to address these points with regard to Isabelle, simply because I know it best. It shows that there are solutions outside of modifying the calculus itself.

Isabelle provides two different ways of dealing with questions such as "what is an ordered pair". 

* One is to introduce the required abstract properties using an "axiomatisation" declaration: then you are required to justify your axioms through some concrete construction, which is henceforth completely inaccessible. Then you can be certain that no theorem is proved using some unexpected property of {{x},{x,y}}.

* The other is to specify the signature and properties of your construction in a "locale". This is a more flexible solution in that you can now provide multiple implementations of the locale (for example, multiple notions of ordered pair) and you can also abstractly specify refinements of your concept, adding additional constraints. The drawback compared with axiomatisation is that you must specify which locale you are assuming from time to time.

I am sceptical of free logics because long ago I worked with LCF, which added an "undefined" element to every type. Reasoning about "undefined” therefore became the main part of any project though it was almost always irrelevant. Free logics are quite a bit like that. We have found that partial functions are easily dealt with either by using relations ("s converges to a", not "lim s = a") or by extension (x/0 = 0, you really can get used to this).

Overloading is indeed the main concern in my example (the minor concern being inserting the canonical embeddings). This is something that Isabelle/HOL does extremely well with type classes: not only for the meanings of + - * / on so many numeric types, but with limits and other topological properties on a variety of topological spaces, et cetera. We need to recover this if we use an untyped formalism.

Larry

>