[FOM] What Foundational Issues? #1

[Harvey Friedman]

I think it would be greatly useful for the discussion of seriously
alternative foundations for mathematics to also have a discussion of
the major foundational issues about mathematics.

The level of knowledge and tractability about the major issues do vary.

There is a division of such issues that needs very much to be kept in mind.

A. Those foundational issues which are (highly) insensitive to the
choice of a foundational framework.

B. Those foundational issues for which the choice of a foundational
framework is critical.

Of course, the emphasis on the current FOM discussion for some weeks
has been on category B.

For some needed background here, at the present time and for the
foreseeable future, we have the following state of affairs. I will
take it for granted, but there is definitely the possibility that this
might change. In fact, I am going to include the possibility of such a
change in category B.

AS OF NOW. The current gold standard for whether any proposed
foundational framework for mathematics is at least prima facie VIABLE
is

i. For rule based frameworks, that we know that it is free of
contradiction. Generally speaking, "free of contradiction" makes sense
for these axiom/rule based frameworks, although issues can arise even
here. E.g., paraconsistent foundations, something which I, for many
reasons, reject (until some hurdles are overcome, and this is not the
place to discuss this). AND that we know that it is free of
contradiction by a proof within roughly ZFC.

ii. For semantic based frameworks, that we know that we have a system
of objects obeying the axioms. Generally speaking, "having a model"
makes sense for these semantic based frameworks, although issues can
arise even here. AND that we have a proof of the existence of such a
model within roughly ZFC.

AS OF NOW, ZFC rules for determining whether a seriously alternative
foundation for mathematics is even viable.

An interesting question of course is just why ZFC should be accorded
this special status as the gold standard for (prima facie) viability.
I have no doubt that this is warranted, but as always, am interested
in hearing any arguments about this.

HOW THIS COULD CHANGE. The special status of ZFC for "determining
viability" could change if the following transpires. There arises a
foundational framework which has such philosophical coherence that its
prima facie viability is at least as intellectually compelling as the
viability of roughly ZFC. In particular, it could be based on the
formalization of fundamental reliable coherent intuitions that we have
that are quite different from what is embodied in set theory. For
instance, there might be a way of directly formalizing our basic
intuitions about space, time, and motion, that speaks to us as well as
the idea of collections of things, where collections themselves are
also things. However, it is still a very tall order to stay within
such basic non set theoretic intuitions in a philosophically coherent
way and still be able to have a general purpose foundation for
mathematics.

MAJOR ISSUE HERE. Regardless of whether we arrive at a seriously
alternative foundation for mathematics, can be come up with some
fundamental principles about non set theoretic concepts, which are so
powerful as to provide a reasonably compelling consistency proof for
ZFC or some strong fragments thereof?

I have done work on this over the years, which I do not regard as
conclusive in this direction. Some of it goes under the name Concept
Calculus. Most recently, look at

84. Flat Mental Pictures, September 5, 2014, 5 pages. Extended abstract.
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

Staying on the special status of ZFC and major fragments and variants,
there is also FOL=, first order logic with equality.

AS OF NOW. FOL= is regarded as the gold standard for formalizing
deductive reasoning across the entire intellectual landscape. Much of
the reason why ZFC based systems are so well accepted as the gold
standard is its sitting on top of FOL=. And on top of FOL=, it is
particularly simple All of the technical stuff is buried in FOL=. But
because of the independent gold standard status of FOL=, the FOL= is
generally accepted as free of charge. I adhere completely to FOL= in
my Concept Calculus and my more recent #84 on Flat Mental Pictures,
cited above.

HOW THIS COULD CHANGE 1. One way is to use only a fundamental fragment
of FOL=. Specifically, maybe the quantifier free part only (so called
free variable part), or even more ambitiously, maybe only the
equational or almost equational part (equational or almost equational
logic). in the first case, we would no longer be taking quantification
(there exists, for all) as primitive, but retain the connectives (not,
and, or, if then, iff) as primitive. In the second case, even removing
the connectives from the primitives. Relevant here is of course
Hilbert's epsilon calculus. But what I have in mind here needs to be
much simpler when combined with set theoretic axioms. I think there is
work of Tarski and followers on this which needs to be revisited.
I.e., quantifier free or free variable set theory. We would get a
somewhat new kind of more elemental form of ZFC and variants this way,
which could be greatly polished over a period of time.

HOW THIS COULD CHANGE 2.  More radically, some entirely different
conception of deductive reasoning. Or even perhaps something that is
not even deductive. Of course, it does seem hard to avoid at least
equational logic. Maybe something like "emotion logic", where our
emotions (feelings) are what drives the reasoning. Or logic of the
visual field, based on the way we interpret what we actually see with
our eyes.

HOW THIS COULD CHANGE 3. We can talk about using more than FOL= for
the underlying logic. What is the point of that? Well, if we adopt an
extension of FOL= that we argue is really deductively fundamental,
then perhaps this makes ZFC even simpler, and also will initiate some
new kinds of tractable studies in simplicity. What I specifically have
in mind is that we add predication over the objects to FOL= together
with the usual impredicative comprehension principle, and treat this
as an axiom/rule based system like FOL=. However, in contrast to FOL=,
there is no completeness theorem, at least none in the usual sense.
That we would be giving up, but at potentially great gain. For
experts, I am talking about first order second order logic. No, those
four words connected together are not a new kind of typo. And maybe it
is better to even have a free variable version of this, without any
quantifiers! Or even equational or almost equational!! Here I would
use function variables rather than predicate variables. Then there are
only finitely many axioms of set theory, and in terms of
interpretation power, they can probably be made incredibly simple.
Then we can really start doing some simplicity studies.

I will continue this in #2.

Harvey Friedman