[FOM] Formal Math Without Types?

[Harvey Friedman]

On Mon, Feb 22, 2016 at 11:54 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> It might be useful to try to be clear about different type systems that are in use and set up some basic terminology.
...

> On the other hand, it is sometimes necessary to use R^1 instead of R, and to convert between these obviously equivalent types. And to bring the complex numbers into this scheme, it is necessary to identify C with R^2, so that we actually have 1 = (1,0) and i = (0,1) by definition.
>
> The more elaborate type system that I described in previous messages extends that of HOL Light by incorporating axiomatic type classes. This allows the development of multivariate analysis in a much more abstract and natural way, as I alluded to previously. On the other hand, it is considerably more complicated theoretically than the HOL Light system.
>
> Then there are the various dependent type theories, used in proof assistants such as Coq, PVS, Nuprl. There’s quite a lot of variation here, many of these theories are constructive in one way or another and not all of them are decidable. It’s richly ironic that the people most likely to be dogmatically attached to type theory will prefer one of these systems, where types take on more and more attributes of sets. But it’s not always obvious how to interpret such a type theory in set theory.
>
> What really puzzles me are the remarks about John Harrison attached below. He is the architect of HOL Light, which uses the very strong type system that I’ve just described. There’s no other way to work. Either there is some misunderstanding here or he has done some very new work not using types.

Concerning the last paragraph above, I have reached out to John
Harrison to see if he is willing to write about the types issue here
on the FOM.

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.

I already see many more issues involved when proofs are included. But
there are already some issues involved without proofs. I.e., just
axioms, definitions, and theorems. I.e., just Semantic Representation.

So for Semantic Representation, where do we first encounter problems
with the type free set theory approach?

I am talking about ZFC with straightforward sugar like in
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-lecture-notes-2/
#65 An Approach to the Formal Representation of Mathematical
Propositions.

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. I can see the reason for this. But for Semantic
Representation, the case is not compelling. Also I will argue (later)
that one can reasonably avoid this also when proofs are involved.

For Semantic Representation (i.e., no proofs), you still have to be
extremely careful about such things as Z^1. Z^1 is not Z, but there is
an isomorphism. I don't see any issue here.

Now perhaps issues first arise when one develops (without proofs) the
number systems: naturals, integers, rationals, reals, complexes. Sure
there are always going to be people who prefer various ways of doing
this to other ways, no matter whether one is using types or one is
using no types. There needs to be an official version, and there needs
to be theorems stated that accommodate other conceptions. This seems
to be fine in the type free approach.

I would recommend that the natural number system be based on the set
theoretic object omega. That integers are ordered pairs (0,n), (1,n),
n nonzero. That rationals are equivalence classes of pairs of
integers. That reals are sets of rationals. That complexes are ordered
pairs of reals.

Then one does the abstract theory. I.e., that the various systems
above, and parts of them, are unique up to isomorphism satisfying
their basic laws.

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.

I would like to follow exactly the way mathematicians handle this,
only make it syntactically and semantically perfect. It should read
exactly as above.

More issues of this kind arise when dealing with, say,

(a + b)^2 = a^2 + 2ab + b^2, in the real numbers.

Again, make this literally syntactically and semantically perfect, and
looking exactly like the above.

It would seem that any substantial variance from this kind of writing
would cost too much in lost readability for the general mathematical
community.

Harvey Friedman