[FOM] Wiki: type theoretic fnds

[Harvey Friedman]

On Fri, Apr 1, 2016 at 3:15 AM, Mario Carneiro <di.gama at gmail.com> wrote:
>
Friedman:

>> 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.

Mario:
>
> 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.

Friedman:

Standard free logic discipline says that the statement I gave in
English is clearly false. This is because the two terms being compared
are each undefined, and they are being compared by an (formally)
atomic relation. Therefore by free logic, the result is false.

My point is that we do not endeavor to call such statements
ungrammatical. If we go down that path for English, we will never keep
our heads above water with all of the issues and problems that would
arise.

Mario:

... How do you
>> > propose to categorize and marginalize these type-theoretically invalid
>> > statements?
>>

Friedman:

>> 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.

Mario

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

The situation with ZFC foundations is just perfect in so many ways.
The working mathematician wants their foundations to be powerful,
reliable, and INVISIBLE. They don't want to be required to create
formal artifacts or auxiliary constructions. They just want to get on
with the mathematics. They don't want any requirements and
restrictions beyond a bare minimum of what is required in order to
avoid inconsistency. They want philosophical coherence, so that their
foundation is based on clear fundamental principles without
artificiality or obscure choices.

ZFC is perfect for this. The working mathematician can layer whatever
they want to focus on OVER it without any problem whatsoever (ok,
there are some issues if you reject classical logic). If you want to
emphasize categorical "foundations", then you, as MacLane did, define
a category as a *set* together with additional structure. If you like
type theoretic organization of math, then that is supported in a
totally obvious way. If you want structuralist ideas only, form
structures in the usual set theoretic way, but just we sure to state
everything up to isomorphism. If you don't like either, but want
something else, that probably can also be easily accommodated.

Not only is it hugely flexible, it is also based on a rigid mental
picture of the mathematical universe, which has huge advantages in
clarity and definiteness, and does an unusually good job in avoiding
vague notions.

Nevertheless, I am still interested in seriously alternative
foundations, as I am discussing in
http://www.cs.nyu.edu/pipermail/fom/2016-April/019648.html Not for
replacing the usual foundations for mathematics - unthinkable! - but
rather for some possibly new and interesting consistency proofs for
ZFC and variants. But there is no chance of this unless and until
seriously alternative foundations is giving a philosophically coherent
presentation.
>
> 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.

There is no point in straightjacketing the formalization of math to
conform to a type theory. Use ZFC at the bottom and layer whatever you
want over it. In fact, that is what mathematicians do.

Mario:

> 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.)

There is no problem with ZFC foundations dealing with computation. In
one sense, this is a trivial remark. The theory of computation,
including algorithms, computational complexity theory, etcetera, are
just normal branches of mathematics that are obviously formalized
totally straightforwardly in ZFC.

I think you are talking about having formal systems where you can
extract algorithms from proofs, or for which if you have a proof of a
certain kind, you at least know there is an algorithm of a certain
kind.

This is quite different than the issue of ultimate foundations for mathematics.

Nevertheless, the set theories with intuitionistic logic can be used
in striking ways to connect up with computability.

Harvey Friedman