[FOM] Is mathematical realism compatible with classical reasoning?
hendrik at topoi.pooq.com
Mon Aug 7 21:46:39 EDT 2017
On Mon, Aug 07, 2017 at 07:20:57AM +0300, Patrik Eklund wrote:
> This discussion is turning into a very strange discussion.
> If we start to use things like "majority position" as de facto
> justifications of mathematical rightfulness, what are we really doing?
> Philosophy is ok, and even new branches of philosophy (whatever they are)
> are ok, but philosophy is not mathematics. Metamathematics is mathematics,
> but as soon as we realize there may be meta of meta, and meta of meta of
> meta, and so on, we wonder about fons et origo, and how to start from there.
> Set theory needs logic, and logic needs set theory to kick off. After a
> while they develop hand in hand and become intertwined. This is pretty much
> where we were one hundred years ago. That intertwining didn't per se justify
> self-referentiality, since on the set theoretic side it remained strictly
> forbidden. On the logical side it was allowed.
Self-referentiality does seem to be the elephant 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.
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. I can't say
that the number 3 is real in anything like the sense in which the
table I'm writing this on is real. So the questin of mathematical
realism is really a question of natural language syntax and semantics
-- whether it is appropriate to extend the meaning of "real" to
encompass mathematical objects.
But the problem of self-reference is a real one. We want to use it to
build magnificent edifices, but have to make sure they are properly
founded. Ultimately that seems to hinge on whether self-referential
definitions, when ultimately expanded, turn out to be well-founded.
The Russell set of sets that are not members of themselves unwinds in
a completely circular fashion, and is therefore not legitimate.
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.
> The problem is about types. For sets we really don't have them, and in logic
> we mix terms and sentences, and we mix truth and provability.
> Type theory tries to fix this but they make the same mistake as is done is
> this debate. They reject the idea that metamathematics must be mathematics.
> They want a meta that is the first and fundamental meta of everything. What
> happens in such approaches is that something eventually goes wrong, and then
> something cute is brought in from the outside as a rescue, but it is not
> called another meta, but it lives its own life as a nice trick.
Type theories are an atttempt to force sufficient well-foundedness
to ensure meaning.
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.
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.
More information about the FOM