[FOM] Isomorphic Structures in f.o.m./2

[Harvey Friedman]

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