[FOM] Is mathematical realism compatible with classical reasoning?
peklund at cs.umu.se
Wed Aug 9 00:24:09 EDT 2017
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".
> 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
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.
More information about the FOM