[FOM] Wiki: type theoretic fnds

[Harvey Friedman]

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.

> Because it does not
> fit the formation rules for wffs, it is a meaningless expression. However,
> "0 in 1" is perfectly valid, even though many mathematicians will tell you
> this is meaningless. (If you spend too much time with ZFC, you will become
> convinced that this is a normal question, since it is well-formed according
> to ZFC, and the answer is "yes" if those are defined as von Neumann
> ordinals.)

The most intellectually efficient mindset is that this is harmless enough.
>
> 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.

You accept that a great virtue of ZFC is the underlying picture of the
immutable rock solid objects. Given that, you are free to create your
own focus - say structures under isomorphism. Everything rests on
bedrock, and that is the best way to do things. You still have
incredibly great freedom in what you layer on top.

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?

The heart of mathematics is concrete statements. As far as I know, the
seriously alternative frameworks fall into these categories.

1. Those which have been shown to be mutually interpretable with roughly ZFC.
2. Those which have been shown to be mutually interpretable with
roughly ZC or weaker.
3. Those which have not been shown to be interpretable in ZFC or
standard extensions thereof.

In every case of 3 that I know, there is no credible argument ever put
forward that the system is consistent. ZFC is still recognized as
being utterly dominate here.

In every case of 1,2 that I know, the interpretations show that as far
as concrete mathematical statements are concerned, provability in the
seriously alternative foundational framework is equivalent to
provability in ZFC. So for the most critical of all classical
foundational issues,

do our foundations support the legitimate proofs of concrete
mathematical theorems?

the choice of foundational framework is utterly irrelevant.

But there are still many reasons to greatly prefer ZFC. Here are some.

a. Even with respect to concrete statements. Here all of the methods
known for obtaining Concrete Incompleteness and even Incompleteness
generally, come out of the methods developed from the usual f.o.m.
This could be a mere historical coincidence, but I have my doubts.

b. ZFC is based on FOL= which is first order logic with equality. ZFC
is clearly extremely simple if you don't include FOL=. Even if you do,
it is conceptually far simpler than alternatives, although I doubt if
anybody would take my word for it. But if you don't charge anything
for FOL= then there is no contest.

c. FOL= should be for free on the following grounds. It is utterly
fundamental to the whole of deductive thought, whether in mathematics
or not in mathematics.

d. This raises the crucial question of whether there is some analog of
FOL= living in seriously alternative foundations, that is also utterly
fundamental to the whole of deductive thought, whether in mathematics
or not, and whether if we also charge nothing for it, then the
alternative foundations will be as simple as ZFC.

Harvey Friedman