[FOM] Is mathematical realism compatible with classical reasoning?

[Patrik Eklund]

On 2017-08-08 04:46, Hendrik Boom wrote:

> Self-referentiality does seem to be the elephant in the room.

Using category theory for construction e.g. of terms and sentences, and 
the way terms appear in sentences (e.g. controlling the way substitution 
is allowed), and so on, brings in "lativity" (= 
anti-self-referentiality) into these constructions.

So it's not elephant. It's "in the room".

> Pretty
> well any logic or set theory seems to work consistently as long as
> there's no self-reference involved.  Introduce self-reference and
> there's a problem.

Allowing rooms in rooms.

> The question isn't about whether mathematics is "real" or not.  That
> hardly matters, and in any case the word "real" has a different
> meaningin this context than it does in everyday life.

The reason for us to do what we do is not being foundational about 
foundations, but foundational about applications. Terminology, like in 
health care, needs type constructors more than just type construction, 
and those constructors must reside within (not outside) the 
terminological machinery. Another important aspect in application is 
order. In health, the order by which interventions are applied, the 
order by which disorders affect each order, and so on. Mathematical fact 
is two-valued, but logic in applications need often be many-valued. 
There is an algebraic foundation of logic that explains how 
many-valuedness and order can be handled. This foundation is based on 
category theory. Lots of structure can be arranged in underlying 
categories. Functors and monads are constructors.

> The various formalizations that preserve mathematics successfully all
> place different constraints on circular reference.  Unfortunately,
> "well-founded" does not seem to be something that can be completely
> formalized, only approximated.

A construction can be made well-founded in a language if we close the 
door for self-referentiality between language and metalanguage. When we 
come close to fons-et-origo foundations, metalanguage narrows down to 
natural language, and that "room" no longer comes with any blueprints.

Such foundations are tricky, but the least we could do is to disallow 
self-referentiality, not reward it, however smart it has been applied. 
In my view, Hilbert and Bernays has a mild formulation to say so in 
their GdM II. They could have chosen much stronger wordings, but for 
some reason they didn't. My conviction is that we are about to voice out 
those stronger wordings, and it will happen over the next century from 
now.

I even believe that the interplay with applications will drive these 
things in the right directions.

> The constructive type theories I've seen contain their own metatheory
> to a significant extent.  The journey you can take through meta,
> metameta, metametameta, and so forth are mirrored in the hierarchy of
> universes.  Ultimately, though, this formulation has its own limits,
> in that it doesn't have a fully transfinite hierarchy of unuverses.

Precisely. So we must be careful about universes, not see them as an 
opportunity. HoTT and constructive type theory are foundationally 
fragile. Over the decades, weakness have been "fixed" and the theory 
today is like leaky patchwork.

> The problems we seem to be having here about whether truth is
> mathematical seems to be translatable to the question whether
> well-foundedness is mathematical.  Foe limited systems, yes.  In
> complete generality, it's hard to know what the queston means.

Hilbert did the right thing to formulate the problem, for others to 
investigate, and Gödel's "solution" involving the Liar must not be seen 
as end of the story. The story of recursion is also still wide open, if 
you ask me.

It's up to all of us to decide how to approach the furnishing of this 
room. The elephant is just the clumsy elephant.

Thanks, Hendrik.

Best,

Patrik