[FOM] Isomorphic Structures

[David McAllester]

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

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.

David

On Sun, Mar 27, 2016 at 6:44 PM, Harvey Friedman <hmflogic at gmail.com> wrote:

> Follow up on http://www.cs.nyu.edu/pipermail/fom/2016-March/019610.html
>
> To try to steer the discussion into something productive, I suggest
> the following in B below.
>
> A. The idea of identifying isomorphic structures is a superficially
> appealing one, at least from a practical point of view, since it may
> allow you to not have to adapt proofs about one structure when moving
> to an isomorphic copy. Normally, you don't repeat, but instead say
> "obviously, the same proof shows that ...". In f.o.m., you just have
> that isomorphic structures are first or second or whatever order
> equivalent, and that gives you something at least semiformally
> rigorous to work with to avoid repeating proofs. I tried to compile a
> list of alternative approaches when trying to incorporate the
> practical demand of theorem provers, in
> http://www.cs.nyu.edu/pipermail/fom/2016-March/019610.html but I
> forgot one major one. And when that major one can be done, it is
> obviously even better than all the rest. I had listed
>
> "1. Require that the fact be reproved about the second structure. Of
> course, one may use cut and paste to the extent possible.
> 2. Formulate the right metatheorem (e.g., share the same first order
> or higher order properties if isormorphic), prove the metatheorem, and
> then apply it. The difficulty here is that to apply it, there is some
> sort of self referential or potentially self referential maze one has
> to negotiate. I.e., when you actually write down a moderately
> complicated first order property, you have to give a name for it and
> prove that it denotes a first order property, etcetera. Or, closely
> related, add a rule of inference to the prover. Definitely awkward.
> 3. Formulate the right metatheorem, but still adhere to the raw proof
> setup. This time, write a script that takes the first or second order
> property (or variant, and actually produces a formal proof that the
> property is preserved. You don't have to prove that the script is
> written properly, but instead plug in the output, and see if the
> prover accepts it."
>
> and preferred generally speaking 3. But there is
>
> 4. Go back to the proof that the first structure has the property, and
> upgrade that proof to show that all structures isomorphic to the first
> structure have the property. I'm thinking by hand. This is nothing
> more or less than sharpening up one's statements, which is done all
> the time. And this is of course very often actually done. So you just
> establish the properties you want once and for all for all structures
> isomorphic to some given structure. Or, for that matter, all
> structures obeying certain conditions. Frequently, all structures
> obeying the conditions you are interested in, are closed under
> isomorphism.
>
> So now I am having trouble thinking of a REASONABLY BASIC situation
> where there is anything much to be gained by having all isomorphic
> structures identical, and opposed to the usual isomorphism relation.
>
> Since the prima facie totally preposterous idea of identifying
> isomorphic structures is being presented by some people as a general
> purpose foundational idea, it is essential to come up with at least a
> small inventory of REASONABLY BASIC examples where one sees that there
> really is something substantial to be gained.
>
> B. Here is the list of Undergraduate Mathematics Courses at Princeton
> University. https://www.math.princeton.edu/undergraduate/courses For
> your convenience I list here the titles of these courses:
>
> Precalculus/Prestatistics
> 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
>
> It would be useful to spot preferably an early part of this Curriculum
> where there is something tangible to be gained by having isomorphic
> structures actually identical rather than just isomorphic. Then people
> can evaluate whether and to what extent one will want to go through
> various new logical complexities in order to support this prima facie
> preposterous idea.
>
> I had previously suggested on the FOM that as far as general purpose
> ideas that I have seen explained in any reasonably simple way, my
> impression is this: anything that can be done with alternative
> foundational ideas can be much more easily and straightforwardly by
> sugaring the usual foundational ideas. it remains to be seen if this
> is the case for the alternatives that we are trying to focus on here.
>
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160328/55c7afea/attachment-0001.html>