[FOM] Is mathematical realism compatible with classical reasoning?

[Hendrik Boom]

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.

-- hendrik