[FOM] Formal Math Without Types?

[Lawrence Paulson]

> In the meantime, as I indicated earlier, I would like to explore just
> what problems arise when one wishes to work in a straightforwardly
> sugared form of ZFC (or ZC) without any serious typing.
> The first issue that I see is the overuse of the plus sign, +, across
> all these number systems, and even abstract ones.
> 
> Mathematicians use "where clauses". E.g., they would write
> 
> (a + b) + c = a + (b + c), where a,b,c are real numbers and + is
> addition on the real numbers.

This example illustrates perfectly why we tend to prefer typed systems: the phrase “are real numbers” is taken care of by typing and then so is the disambiguation of the + symbol. In Isabelle/ZF, which is essentially typeless, these constraints are instead expressed explicitly using set membership, so that the associative law above becomes a conditional statement and the + operator becomes a partial function, undefined when applied outside its domain. And that is why in Isabelle/ZF there is a construction of the closed and unbounded class of fixedpoints of the Aleph operator, but not of the rational number ½.

> I gather that in the MetaMath approach, there are variables over wffs.
> In the relatively purist approach I am talking about, I do not allow
> variables over wffs. 

Isabelle implements a logical framework in which there can be variables over any syntactic category, but they do not have the same status as variables in the embedded calculus (first-order logic in the case of ZF). This makes it possible to express the axiom scheme of separation, for example, as a single assertion, without extending the class of formulas that can be used for separation. Then entire developments can be schematic in such parameters. In particular, reasoning about classes can be done in a fairly natural way, but not allowing quantification over classes or even writing something like V = V.

Larry Paulson