[FOM] Isomorphic Structures

[Harvey Friedman]

On Mon, Mar 28, 2016 at 8:24 AM, David McAllester <mcallester at ttic.edu> wrote:
> I am jumping in the middle here so correct me if I am repeating earlier
> discussion.  The main point of Morphoid type theory (MorTT), and also of
> HoTT, is to define isomorphism across all types and prove the soundness of
> the substitution of isomorphics.  The substitution rule essentially states
> that isomorphic objects can be identified and eliminates any need to repeat
> proofs.    MorTT's classical departure point avoids HoTT's
> propositions-as-types,  path induction, squashing and higher order
> isomorphisms and seems more faithful to the informal language actually used
> in mathematics departments.  Informal mathematics does seem to have a strong
> notion of well-formedness of statements (types).

It is interesting to note that you are proposing another "alternative
foundational" setup which you call MorTT = Morphoid type theory, as an
alternative(?) to HoTT. You say it "avoids HoTT's
propositions-as-types, path induction, squashing and higher order
isomorphisms and seems more faithful to the informal language actually
used in mathematics departments".

So it is clear that you think that "propositions-as-types, path
induction, squashing, and higher order isomorphisms" are indeed worth
avoiding. It could be useful for the discussion to indicate why you
think that these items are in fact worth avoiding.

And what would the HoTT community say to that? That they are worth
avoiding, but you can't avoid them? Or they are not worth avoiding
because they are fundamentally important, or vital? Or what?

Now my own point of view, until I see some reasonably simply
communicated foundational point, is that not only are these items
worth avoiding, but also any type theory is worth avoiding.

Let me make a distinction here. There is the question of what should
be avoided for a foundation for mathematics, and what should be
avoided for practical formalization of definition/theorems, and what
should be avoided for formal proving of mathematical theorems.

My own preliminary view is that type theory should be avoided
emphatically for a foundation of mathematics, less emphatically for a
practical formalization of definition/theorems, and probably for the
proving of mathematical theorems.

History does at least seem to be on my side, because of the experience
with Bertrand Russell's type theories. There is his original very
complicated typing, out of his reacting to Russell's paradox. This got
soundly rejected in favor of the untyped Zermelo and Zermelo-Frankel
set theory, the gold standard foundation for mathematics for nearly
100 years. Many years ago, e.g.,  under Quine, a simple theory of
types emerged out of Russell. This is still soundly rejected in favor
of the untyped ZC and ZFC.

Of course, I reserve the right to totally change my mind if I see
compelling reasons to do so. I gather that you see a reason for me to
change my mind with MorTT, and some others see a reason for me to
change my mind with HoTT?

> The real point, for me, is that the structure of mathematics is almost
> completely driven by the identification of isomorphics.  For example, the
> classification of finite simple groups is "up to isomorphism".  Consider
> Poincare's conjecture that S^3 is the only simply connected compact three
> manifold.  The word "only" is up to isomorphism.  The issue is not just
> making proofs shorter, but rather that the very structure of mathematics as
> a whole is driven by the identification of isomorphics.  Even the natural
> number and the reals are only identified up to isomorphism of the structures
> involved.

"the structure of math almost completely driven by identification of
isomorphics" is very defensible if you just mean the very usual "up to
isomorphism". This is of course easily accommodated with no *apparent*
difficulties with the standard f.o.m.

To illustrate just how much of a non issue this is in the usual
f.o.m., let us say that we are looking at a book on the rather deep
subject of semi algebraic geometry. I'm more familiar with this than
algebraic geometry.

In semi algebraic geometry, one develops a vast and deep theory of the
semi algebraic subsets of the R^n. It has its origins in Grothendieck
with his tame topology.

But say you complain that R doesn't have a good foundation, since R
may be given, under the hood, as the set of Dedekind cuts, or maybe
equivalence classes of Cauchy sequences of rationals. People don't
agree as to what is under the hood here, and people may think that
having anything like that under the hood is a bad idea. Hence there is
a "foundational problem".

The vast preponderance of working mathematicians don't care about this
issue, and don't believe that there is even any point in talking about
it.

But it is resolved rather nicely in standard f.o.m. in a few ways.
Here is perhaps the nicest.

In the Introduction to the book on semi algebraic geometry, you say that

"This work is based on the ordered field of real numbers. However, all
of the work goes through if we use any complete ordered field
whatsoever. All such are uniquely isomorphic."

This is the preferred way of handling this in the form of a math book.
However, for theorem proving, the best course for formally treating
real algebraic geometry is probably to formally make all statements
really live over any complete ordered field. This makes the results,
in a trivial sense, more general. This is of course rather easy to do.

So what is to be gained by rather complicated alternative foundational
schemes such as MoTT and HoTT? Again, I repeat my request to hear a
simple account as to what is to be gained - as early as possible in
the Princeton Undergard curriculum - which I repeat here from
https://www.math.princeton.edu/undergraduate/courses :

>> Precalculus/Pre statistics
>> Calculus 1
>> Calculus II
>> Number, Shape and Symmetry
>> The Magic of Numbers
>> An Integrated Introduction to Engineering, Mathematics, Physics
>> An Integrated Introduction to Engineering, Mathematics, Physics (more)
>> Useful Fictions: How and why mathematics is developed and then changes the
>> world
>> Math Alive
>> Calculus III (Multivariable Calculus)
>> Introduction to Linear Algebra
>> Advanced Multivariable Calculus
>> Advanced Linear Algebra with Applications
>> Numbers, Equations, and Proofs
>> Honors Analysis in a Single Variable
>> Accelerated Honors Analysis I
>> Honors Linear Algebra
>> Accelerated Honors Analysis II
>> Mathematics in Engineering 1
>> Mathematics in Engineering II
>> Introduction to Real Analysis
>> Numerical Methods
>> Introduction to Differential Equations
>> Topics in Mathematical Modeling - Mathematical Neuroscience
>> Analysis I: Fourier Series and Partial Differential Equations
>> Complex Analysis with Applications
>> Analysis II: Complex Analysis
>> Applied Algebra
>> Algebra I
>> Algebra II
>> Fundamentals of multivariable analysis and calculus on manifolds
>> Introduction to Differential Geometry
>> Topology
>> Introduction to Graph Theory
>> Combinatorial Mathematics
>> Theory of Games
>> Probability Theory
>> Analytic Number Theory
>> Topics in Number Theory: Algebraic Number Theory
>> Analysis III: Integration Theory and Hilbert Spaces
>> Ordinary Differential Equations
>> Advanced Topics in Analysis
>> Cryptography
>> Commutative Algebra
>> Topics in Algebra: Representation Theory
>> Advanced Topics in Geometry - Lie Theory
>> Algebraic Geometry
>> Advanced Topology
>> Random Processes
>> Functional Analysis
>> Introduction to Partial Differential Equations
>> Advanced Analysis
>> Riemann Surfaces

Harvey Friedman