[FOM] Wiki: type theoretic fnds

[Mario Carneiro]

On Fri, Apr 1, 2016 at 2:02 AM, Harvey Friedman <hmflogic at gmail.com> wrote:

> On Thu, Mar 31, 2016 at 12:08 AM, Mario Carneiro <di.gama at gmail.com>
> wrote:
> > One obvious property of type theory in general, that has been mentioned
> > several times on related threads, is that type theory has a much stronger
> > ability to reject statements as ill-formed, which is a *good thing*. In
> set
> > theory, you are not allowed to write "x in in y". Why?
>
> The cost is of course that lots of very natural things that you want
> to say are now barred. I believe that the cure is much worse than the
> disease.
>
> Consider English. I can say all kinds of silly things. Statistically,
> most things are silly.
>
> The sum of your left hand and your average hair is greater than the
> product of your right hand and your average nail.
>
> Do we really want to add types to English to avoid allowing us to make
> such outrageously ridiculous statements? I.e., to make them
> ungrammatical? Ungrammatical like: This it blue green.
>
> No. We acknowledge this problem with English, and we move on,
> realizing that fixing this problem with English is probably going to
> cost us far too much intellectual energy than anything that we gain.
> And the likelihood is that in trying to "fix" this we are going to
> inevitably tie the hands of some speakers for some legitimate
> purposes.
>

I will not say much on this example except to note that you do not attempt
to assign a truth value to that "outrageously ridiculous statement",
because there is no suitable truth value.


> > In type theory, this sort of thing is thrown out. If "0" and "1" are
> > definitions of real numbers, we allow expressions like "0 + 1" and "0 =
> 1",
> > but "0 in 1" is rejected. You say "there needs to be a major effort made
> to
> > see if the existing much simpler system already can be used to address
> the
> > issues, whatever they are, adequately, or maybe even better." How do you
> > propose to categorize and marginalize these type-theoretically invalid
> > statements?
>
> By disposing of the issue as not worth the effort. Of course, if there
> was a simple enough way to do this, it could well be very interesting.
> Maybe there is a theorem that there is no simple way to do what you
> ask.
>

I would argue that there is a simple way to do this, and this way is called
simple type theory.

My main point is that when you "do ZFC", you aren't actually working in ZFC
most of the time. You are working in simple type theory embedded in ZFC. I
have had the opportunity to work on many formalizations in ZFC of
statements from "advanced basic mathematics", such as the fundamental
theorem of Algebra or Bertrand's postulate. If you check out the statements
of these:

http://us.metamath.org/mpegif/fta.html
http://us.metamath.org/mpegif/bpos.html

you will notice that

* All free variables are restricted to a set
* All quantifiers are restricted
* All relations and functions are applied only in their domains of
definition

And this is not just true of the statements - it is true of all the lines
of proof, all the way down, until you get to predicate calculus (aka FOL),
where you see the embedding being constructed.

Given this, it is entirely reasonable to extract this "well-typed" part of
ZFC for reuse; what you get is essentially simple type theory, with
occasional forays to more exotic sets, particularly in the sections which
cover set theory proper (ordinals and cardinals, rank functions and the
cumulative hierarchy). This is not just idle thought: I am attempting to
build bridges between the Metamath database and other formalization, and
this kind of "type identification" is essential for good quality theorem
embeddings.

I have not yet seen any seriously alternative foundational setup that
> tries to be better than ZFC in this and other respects that isn't far
> far worse than ZFC in other even more important respects.


> Now where do ZFC and the seriously alternative frameworks meet on
> common ground, and on that common ground, what can we say about how
> they compare?
>

When we try to boil down a common denominator to "standard math"
interpreted in all these competing foundations, if you take the
intersection of all the consistency strengths, what you end up with seems
to be some kind of type theory. (For example, if you want to have a
collection of theorems that work under both constructive and classical
reasoning, this means they must be constructive, because one theory is a
subset of the other. Similarly, if you want to operate in both type theory
and set theory, you must be doing type theory, because type theory easily
embeds into set theory but not vice versa.)

I believe this is the sense in which type theorists measure their
foundation as the best. Note that the simplicity of the axiomatic
presentation is irrelevant here: the ZFC embedding might be quite complex
(in fact it isn't), but what matters is that it captures all of the math
that we can express in all the systems. It is a foundational "interchange
language".

Another factor in favor of type theory is computation. This is a rather
vague word to throw out, but it seems to be the case that all the powerful
automation tools out there in Coq, Isabelle, HOL light, are all working in
a type theory. Now I don't doubt that one could also write such a system
for ZFC; but I am just as certain that any such tool would be working
within the aforementioned implicit type theory embedding into ZFC. The
ability to put blinders on the computer in its travails to avoid those
"gramatical but patently ridiculous sentences" is an extremely useful
tactic for improving the performance of search algorithms. (By way of
exception, one might note that most automated theorem provers like Z3 or
Otter are actually FOL; but these are usually used within subsystems like
Peano arithmetic, formed by projecting just one type and its operations
from a HOL system.)

Mario

>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160401/158cb6e8/attachment.html>