[FOM] Isomorphic Structures

[David McAllester]

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

​For me the issue is uncovering the existing "grammar" of mathematical
language. English speakers who (largely) speak grammatically must still be
trained to do grammatical analysis of English. Similarly, I believe,
mathematicians can be trained to recognize the naturally occurring
grammatical constraints on "well formed" mathematical expressions and
statements.  I believe that propositions-as-types, path-induction,
squashing and higher order isomorphism do not play a role in the grammar
governing the current common language used in mathematics departments. But
I do strongly believe that such a grammar exists --- mathematicians are
very sensitive to the well-formedness of phrases and sentences.  This
grammar plays a central role in understanding isomorphism and when
substitution of isomorphics is sound. My position is that MorTT is not
really a new foundation.  Rather it is just a theory of the grammar
actually in current use.


> > And what would the HoTT community say to that?
>

​I would like to know ...

>
> ​[Consider]
> the experience
> > with Bertrand Russell's type theories.
> ​ ... H​
> is original very
> > complicated typing
> ​ ​
> ... ​
> got
> > soundly rejected in favor of the untyped Zermelo and Zermelo-Frankel
> > set theory,
> ​ ...​
>
>
​I completely accept ZFC as a circumscription of the provable.  I believe
(or at least hope) that the theorems
of MorTT correspond in some precise sense the theorems of ZFC (extended
with some appropriate number of inaccessibles).

I have two motivation for types:

1) Natural mathematical language does have a grammar governing
well-formedness which we should try to understand.

2) There are important mathematical phenomenon that can only be
appropriately understood through an understanding of the grammar of
mathematical language.  In particular we need to understand isomorphism ---
what is it in general.  We need to understand when the substitution of
isomorphics is sound.
We need to understand cryptomorphism in the sense of Birkoff and Rota (see
my manuscript) and we need to understand Voldemort's theorem that, for
example, it is not possible to name a point on a geometric circle or a
particular basis for a vector space.  All of these phenomenon are easy to
exhibit and are present, at least implicitly, in every reasonable
undergraduate curriculum.

>
> ​[Regarding the real numbers one can say] ​
> "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
> ​ ...​
>
>
​I am playing the role of a cognitive scientist. For me "the preferred
handling" is the phenomenon of interest.
​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160329/c0866f58/attachment.html>