[FOM] Mizar's type system

[Anthony Coulter]

Good Freek,

 > I don't see how this would be different from
 > Mizar-types-that-don't-need-be-non-empty, but maybe I'm
 > missing something?

Actually, that was my question to you---it seemed as though predicates
could do everything that types could do (albeit less conveniently), so
I made a list of conveniences to see if *I* was missing something.
Apparently I hit all the important points, except for this next bit:

 > And I think you underestimate the amount of "inference" about
 > the predicates-as-types that is going on in Mizar.  If you
 > would add all that, how would it then that be different
 > from having a "separate type mechanism"?  That _is_ the
 > separate type mechanism!

Maybe `separate type mechanism' is the wrong phrase; my only real
target is the `separate type concept.' I would prefer to avoid having
to distinguish between "Nat the type" and "Nat the predicate;" I would
prefer that only the predicate exist. I accept the necessity of a
separate mechanism for type inference. My impression of things is that
the predicate logic is semidecidable but certain fragments of it are
not only decidable but *efficiently* decidable. The type mechanism
would automate proofs of some natural-seeming fragment, e.g. horn
clauses plus conclusions about the type of a function based on the
types of its arguments. It would apply to *all* predicates, so when
a theorem depends on whether b is zero, it wouldn't matter whether
"b != 0" is expressed as an ordinary predicate or as a type that is
quantified over---the proof checker would recognize a predicate as
a predicate.

As for "underestimating" the amount of inference... Let's just say
that I agree that there's an awful lot of work to be done to replicate
what Mizar is already capable of, but that if we speak directly about
just *how* much work is involved, I would never get around to doing it.
I would be thrilled if a committee managed to "bless" a proof checker
specification that covers all the awkward issues like what to do about
partial functions, how to flip a switch to support intuitionistic and
constructive reasoning, what to use for the "standard set theory" that
is available to people who don't want the full power of ZFC, how to
discuss category theory in a flexible way that doesn't prematurely lock
you into a particular set-theoretic universe, how to support flexible
variable-binding expressions, and so on. A consensus on how things
*ought* to work would go a long way towards encouraging folks (e.g. me)
to implement it.

 > So having sorts and predicates seems duplicate, why not work
 > in an untyped world then?  It sounds a bit HOLZF-ish to me.

Here I show my true colors. Yes, I started this discussion by quoting
your post about how strongly-typed systems are compatible with making
everything a ZFC set. But that was only to motivate the discussion; I
don't actually want to use ZFC as a foundation. I would prefer to let
a bunch of theories coexist peacefully (with mostly-distinct sorts and
axioms) in the framework of HOL (to force everyone to use a standard
set theory with known Prawitz-esque normalization properties). I think
this approach will eventually prove to be the most natural---it's how
most mathematicians seem to think about the standard mathematical
universe. The Foundations of Mathematics community has a slightly
distorted view of things. (I mean no offense!) Here, we're comfortable
claiming that the natural numbers are a subset of the ordinals, and
that the integers are equivalence classes of ordered pairs of naturals.
If you ask a regular mathematician about it, he'd probably rephrase it
and say that the naturals are *isomorphic* to a subset of the ordinals,
and the integers are *isomorphic* to equivalence classes of pairs of
naturals. To a normal mathematician, the "true" naturals are a subset
of the integers, which are in turn a subset of the rationals, the
reals, and the complex numbers.

My vision for the Standard Mathematical Ontology gets a little tricky
here: I see a primitive sort of "numbers" which is intended to include
the complex numbers and any extensions folks might want to add to it
or its subsets (e.g. the infinities of the extended real line, complex
projective infinity, the hyperreal numbers, or the p-adic numbers).
Then there would be two ways to introduce Peano arithmetic: you could
either set it up inside this "number" sort and add a new primitive
"IsNatural" predicate, or you could stubbornly work with your own
separate "natural number" sort. If you take the latter approach then
your naturals will be distinct from the "true" naturals and you will
have to construct an injection from your numbers to the "true" numbers.
In some situations this would be worthwhile---if you're formalizing
Simpson's "Subsystems of Second-Order Arithmetic," you have to be
especially careful about what sorts of predicates you do induction
over, so in most cases you have to re-prove all the theorems you want
anyway. But the rest of the time this would be a pain. In the standard
library, the standard natural numbers would follow the first approach
with the usual "number" sort and a special "IsNatural" predicate. If
someone wants to construct the natural numbers as a subset of the
real numbers, they can do so. They'd start with a different set of
axioms and definitions (so IsNatural would no longer be primitive; it
would be defined as the closure of the set {0, 1} under addition) but
they could use the same symbols, so no extra translation would be
needed to import theorems from Peano arithmetic into real analysis.

This vision has plenty of gaps. For example, I tell myself that
carting around an extra "IsNatural" predicate when I do number theory
won't be overly burdensome because the aforementioned type-inferrer
should be smart enough to keep track of predicates most of the time.
But I don't have a complete specification for the type-inferrer yet.
I also don't know how I would approach the importation of theorem
schemes. Simpson's book makes use of Delta_1^0, Sigma_1^0, and Pi_1^1
schemes, and Aczel's constructive set theory does something similar.
I would like to support a generalized arithmetic hierarchy, but while
it's easy to implement something like that for an individual theory
it's more complicated to figure out how to import predicate schemes
with those sorts of restrictions from one theory to another. But I
think the basic idea is fairly natural, and in general I believe that
most design decisions can be made by asking ``How would a mathematician
who has *not* studied foundations of math expect the proof checker to
behave?'' (It's the *implementation* that requires an understanding
of F.O.M.)

When I have a coherent proposal I intend to post it to this list for
comments. If you have a tolerance for incoherent proposals, feel free
to email me directly. (By a curious twist of fate involving aggressive
air conditioner salesmen, emails mentioning "free ultrafilters" in the
subject line automatically go to my spam bin. :-))

 > Another thing might be to somehow "identify" types and classes,
 > so to not have a distinction between the set of natural numbers
 > (as a class) and the type of natural numbers.

I've thought about this and I'm currently inclined against it. One
problem is that the (n+1)-ary predicates you need for dependent types
are awkward to convert into sets. (I'm leaning towards providing tuples
for free as part of higher-order logic, but that doesn't make it any
less awkward.) Another is that it wastes short symbols; I'm looking at
a grammar that lets atomic symbols (like the set "R") and symbols which
take arguments (like the predicate "R[...]") to live in separate
namespaces, so you could have "R" and "R[]" refer to entirely different
concepts if it turns out to be convenient for your purposes. If I link
predicates and sets automatically, the existence of an "R[]" predicate
prevents you from letting "R" be a variable standing for an arbitrary
ring. But one-letter symbols are in short supply; there are only 52!

My third problem is that people's expectations for type inference are
lower when predicates are involved. I can promise to infer types for
Horn clauses (e.g. "All x: Positive[x] -> Integer[x] -> Natural[x]")
without raising any eyebrows. But if I promise to infer types involving
sets, then folks will want automatic inferences about formulas like
   All x: x \in (SetOfPositiveReals \cap Integers) -> x \in Naturals
where x's membership in a simple set (Naturals) now depends on its
membership in a more complex set (the intersection of two other sets).
Ideally, automatic type inference would be limited to proving something
complex from simpler assumptions, not the other way around. But of
course this depends on what exactly the automatic type inference system
promises.

I understand your fourth argument (that we don't want to force people
into a particular set theory) but at the moment I intend to provide a
standard higher-order logic since, as Prawitz showed, it's conservative
over first-order theories without axiom schemas and I'm already looking
at ways to keep track of what sorts of symbols get instantiated in
formula schemes. Constructivists who only want to admit Delta_1^0 sets
would be facilitated with free logic: You can still talk about
impredicative sets, but you can't do anything with them until you (or
an automatic mechanism) prove that the set in question exists. Free
logic is required for certain forms of constructivism anyway; see
  <http://cs.nyu.edu/pipermail/fom/2015-September/019169.html>

So at the moment, automatically identifying types/predicates with
classes appears to be more trouble than it would be worth. But that
could change as other design decisions firm up.


 > There also is <http://www.cs.ru.nl/~freek/mizar/miztype.pdf>
 > although I doubt it will add much for you.

Ah, I have not seen this before. It does add something---a list of
type inference rules. This will help refine my estimate of how much
inference "is going on." Thanks!

Anthony