[FOM] CFA: Foundations of Mathematical Structuralism, Munich, Oct. 12-14, 2016

[Harvey Friedman]

On Sat, Jun 4, 2016 at 5:39 AM, John Wigglesworth
<jmwigglesworth at gmail.com> wrote:
> CFA: Foundations of Mathematical Structuralism
>
> 12-14 October 2016, Munich Center for Mathematical Philosophy, LMU Munich
>
There was an active thread on some major aspects of what I think is
being meant here by "Mathematical Structuralism" here on the FOM a
little while ago. I asked for at least something of a seriously
foundational nature surrounding "homotopy type theory", and more
broadly, and Dimitris Tsementzis started to take up the challenge in a
very interesting way. I hope he will return and continue, as there
were obvious indications that he had a good idea of what is needed to
take "homotopy type theory" from a specialized technical subject to
perhaps something of relevance to f.o.m.

In the meantime, I have been thinking quite a bit about the
development of a new Geometric Foundational Scheme, where the
primitives are completely commonplace from the geometric standpoint,
and where you get a system that is mutually interpretable with the
usual second order arithmetic of f.o.m. = Z_2, or equivalently, ZFC\P
= ZFC with the power set axiom deleted. Of course, ZFC and large
cardinals would be far more impressive.

This Geometric Foundational Scheme is very much in the spirit of the
well known Geometric Foundational Scheme of Aristotle, where in modern
terms, he is using the idea of an interval is a "part", and left to
right, where, emphatically, there are no points, so that intervals do
not have endpoints. There are some minor choices as to how you
formalize this, but you get very important first order systems -
single sorted - which are well known to be complete and decidable.
Technically, it corresponds to the elimination of quantifiers for
dense linear orderings without endpoints. Obviously nothing close to
even being able to interpret weak fragments of PA or ZFC\infinity or
even EFA. Here I am referring to the standard first order deductive
approximations to the second order semantic systems - where we use a
completeness scheme.

I'm no historian of Ancient Philosophy, but I think also we should be
considering the idea of adding "two intervals are of equal length" to
this here, also with obvious axioms including again the completeness
scheme for the extended language, as Aristotelean as well. And once
again you get satisfying completeness and decidability, as this falls
within the theory of divisible abelian groups. Still nowhere near even
EFA. And also, we can bring in proportionality, which is a 4-ary
relation on intervals. Then again we have satisfying completeness and
decidability, as this falls within the theory of real closed fields.
Relevant here is an old result of mine - with roots in Tarski - that
RCF is provably consistent in EFA.

So with these kinds of things, we don't even interpret EFA, let alone
PA, or Z_2 or ZFC\P, let alone ZFC itself.

But there are is another primitive that DOES get us up that far.

VERSION FOR PA, ZFC\infinity

1. Intervals as parts, with left to right.
2. There is a universal interval.
3. One interval is a component in some equal subdivision of a second interval.
4. Obvious axioms for the primitives 1-3.
5. Axiom scheme: If a given first property holds of some component of
some equal subdivision of a given interval, then it holds of a
leftmost such component.

VERSION FOR Z_2, ZFC\P

1. Intervals as parts, with left to right.
2. There is a universal interval.
3. One interval is a component in some equal subdivision of a second interval.
4. Obvious axioms for the primitives 1-3.
5. Axiom scheme: If a given first order property holds of all parts of
a given interval, then there is a maximal such interval.

I'll discuss formal details of this when I move it to my numbered postings.

There remain some additional serious challenges for this kind of
Geometric Foundations.

One is of course to entirely remove predicate calculus from the
picture. The other of course is to get up to ZFC and beyond. This is
not far fetched because of my recent Continuation Theory, which I have
stated in very basic biological terms, but also can be viewed
geometrically.

I.e., perhaps Continuation Theory should be also looked at as a theory
of Dynamic Geometric Objects.

Then instead of Pi01 Incompleteness, we have some

Principles of Structural Growth.

Now let me get to commenting on
http://www.cs.nyu.edu/pipermail/fom/2016-June/019891.html

> In the course of the last century, different general frameworks for the
> foundations of mathematics have been investigated. The orthodox approach to
> foundations interprets mathematics in the universe of sets. More recently,
> however, there have been other developments that call into question the
> whole method of set theory as a foundational discipline.

The last sentence is at least grossly misleading, if not outright false.

Here is an appropriate rewording of the facts of the matter:

MORE RECENTLY, SOME ADDITIONAL GOALS FOR A FOUNDATION FOR MATHEMATICS
HAVE BEEN OFFERED UP FOR INVESTIGATION.

It is completely obvious that on the classical and entirely
appropriate conception of a foundation for mathematics, set theory
isn't even remotely being called into question, and is far the
cleanest, clearest, and most transparent of all proposals.

Furthermore, all proposals of any note for f.o.m. are either known to
or believed to be interpretable in the usual set theoretic
foundations.

What remains to be carefully explicated is

EXACTLY WHAT ADDITIONAL GOALS FOR A FOUNDATION FOR MATHEMATICS ARE WE
REALLY TALKING ABOUT?

Now I have many times issued a challenge. To come up with such
additional goals, so that we can see if the usual set theoretic f.o.m.
can be adapted to meet those goals. And I have conjectured many times
that

CONJECTURE: Any clearly stated additional goals for f.o.m. that are to
be realized by the kind of schemes being proposed can be done much
better through adaptation of the existing standard f.o.m.

Of course, the Geometric Foundations development being investigated
above would be probably a special case of this "anything you can do I
can do better" conjecture.

> Category-theoretic
> methods that focus on structural relationships and structure-preserving
> mappings between mathematical objects, rather than on the objects
> themselves, have been in play since the early 1960s.

Yes, and it has proved to be comparatively awkward, and imitates a lot
from set theory, and is clearly mutually interpretable with set
theory. So there remains the question as to just what has been gained.
I have no doubt that it is a technically useful setup that has proved
to be useful and at least very convenient for a lot of abstract
mathematics. Especially, if not overdone.

The part of current mathematical logic that is in rather close contact
with many core mathematicians is Applied Model Theory. By definition,
Model Theory is "structural". Yet when I talk to Applied Model
Theorists about seriously categorical approaches, they say that they
very much wish to avoid this way of doing things. They speak with a
lot of credibility on this matter, as much of their entire motivation
comes from Grothendieck's viewpoints - his tame topology.

> But in the last few
> years they have found clarification and expression through the development
> of homotopy type theory.

I haven't yet seen any coherent clarification of anything of any
general purpose or general interest, and Dimitris Tsementzis was at
least starting to take up this challenge seriously and COHERENTLY,
here on the FOM. I hope he can come back to this.

> This represents a fascinating development in the
> philosophy of mathematics,  where category-theoretic structural methods are
> combined with type theory to produce a foundation that accounts for the
> structural aspects of mathematical practice. We are now at a point where the
> notion of mathematical structure can be elucidated more clearly and its role
> in the foundations of mathematics can be explored more fruitfully.

I would like to see any clear elucidation. Can you provide anything
like that from first principles as we all know how to do with set
theory? I would prefer that the burden not be solely put on Dimitris
Tsementzis.

There are all manners and sorts of "elucidations" and "clarifications"
that have been or can be readily treated within the standard f.o.m.
that are already "clear".
>
> The main objective of the conference is to reevaluate the different
> perspectives on mathematical structuralism in the foundations of mathematics
> and in mathematical practice. To do this, the conference will explore the
> following research questions:

> Does mathematical structuralism offer a
> philosophically viable foundation for modern mathematics?

What exactly is meant by "mathematical structuralism" is from what I
gather not at all fixed. Does the development above following
Aristotle count as within "mathematical structuralism"?

> What role do key
> notions such as structural abstraction, invariance, dependence, or
> structural identity play in the different theories of structuralism? To what
> degree does mathematical structuralism as a philosophical position describe
> actual mathematical practice? Does category theory or homotopy type theory
> provide a fully structural account for mathematics?

Good questions. I would very much like to see a discussion here on the
FOM from any of the list of Confirmed Speakers and the Organizers:

> Confirmed Speakers:
>
> Prof. Steve Awodey (Carnegie Mellon University)
> Dr. Jessica Carter (University of Southern Denmark)
> Prof. Gerhard Heinzmann (Université de Lorraine)
> Prof. Geoffrey Hellman (University of Minnesota)
> Prof. James Ladyman (University of Bristol)
> Prof. Elaine Landry (UC Davis)
> Prof. Hannes Leitgeb (LMU Munich)
> Dr. Mary Leng (University of York)
> Prof. Øystein Linnebo (University of Oslo)
> Prof. Erich Reck (UC Riverside)

> Organizers:
>
> Georg Schiemer (MCMP & University of Vienna), John Wigglesworth (MCMP)

Harvey Friedman