[FOM] Eradicating Evil?

[Harvey Friedman]

My back channels tell me that there is a crusade to "eradicate evil"
spearheaded by the HoTT community. The word "evil" is commonly used
there. The worst specific widespread form of evil is apparently the
membership relation, which is to be eradicated at all costs.

There is a legitimate foundational problem here of general interest
which I believe is quite amenable to classical f.o.m. attack. It is a
genuine general purpose issue.

THESIS. The eradification of that  "evil", so glorified by that agent
of evil, classical f.o.m., is best achieved through variants of the
Standard Umbrella, also presented and developed through classical
f.o.m.

I will try to establish the above Thesis. We cannot expect to do this
in first attempts.

I see already a range of HoTT, thinkers from "oh, what we are doing is
totally compatible with classical f.o.m., or at least intuitionistic
set theory", all the way to "the classical f.o.m. is evil, and must be
expunged from mathematics". There is also "yes, it is fully compatible
with the Standard Umbrella, but you can't actually formalize proofs in
the practical sense", and so "in a practical sense, we need to
overthrow the Standard Umbrella".

So I will simply go under the working assumption that we can satisfy
everybody - practical proof formalization included - if we make some
traditional f.o.m. moves - with some finesse.

Of course, it is out of the question that even a very good first move
in this direction is going to come close to satisfying everybody. If I
can get a good start on this, the plan is to improve on it after the
complaints are understood.

So let me start by trying to state the major issue in clear, but
probably oversimplified terms.

One way of doing foundations of actual mathematics is to give specific
instantiations of fundamental mathematical structures. This is a very
common approach, and in some ways, is the simplest and most direct way
of doing actual mathematics in ZFC.

This approach - and the accusations of evil - start with the natural
numbers. These are taken to be the usual omega of set theory, with
emptyset, {emptyset}, {emptyset,{emptyset}}, etcetera.

Set theorists regard this as divine. It is very specific, and very set
theoretically convenient, where < is treated as epsilon. One readily
proves a lot of properties of this construction in ZFC. That we have a
well ordering with no greatest element, and no limit point. This
readily supports mathematical induction.

Many mathematicians regard this as evil. Use of the membership
relation is "bogus" because the natural number system has nothing to
do with sets - it is even pre set theoretic. Also, the very idea that
there is a preferred natural number system is either "bogus" or at
least highly suspect. And if there is even going to be any kind of
preferred natural number system, then it certainly isn't going to be
this set theoretic monstrosity.

So immediately at least one simple form of the challenge arises - how
do we do convenient f.o.m. without being committed to specific
representations of fundamental mathematical structures? This is not
going to be the strongest form of the challenge, but it is already an
interesting warmup.

In fact, let me take the challenge even further. Even if we avoid
having preferred representations of fundamental mathematical
structures, then we still have the evil epsilon relation working on
all of our objects. Perhaps we should avoid having an epsilon relation
at all?

Actually, for a different purpose entirely (however, one can argue
that the purpose is closely related), I have already written
extensively about what I (almost have previously) called "flat
foundations".

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

Let's talk about "flat ZFC". There are two kinds of sorts. The first
is the sort of all objects. The second kind of sort is relations. We
have a choice of the arity of relations. Minimalistically, we can use
just binary relations, period. Of course, we are quickly going to find
that we want relations of greater (and lesser!) arity, and it will
probably prove rather awkward to simulate this in binary relations.

So I choose to have these sorts:

1. The sort of all objects. We have variables over objects.
2. For all k >= 1, the sort of all k-ary relations. For each k >= 1,
we have variables over k-ary relations.

For greater unification, we can of course simply consider the sort of
all objects as the sort of all 0-ary relations. But this has its
drawbacks, and we consider objects very special here.

Now what are the atomic formulas going to be?

Most obviously, R(x_1,...,x_k), where R is a k-ary relation variable
and the x's are object variables.

But now we come to a critical issue. What about equality? Should there
be equality between objects, and there is equality between relations
of the same arity??

Well given all the fuss about equality among radicals, we should be
very careful here. I will at least provisionally take the approach
that equality is NOT PRIMITIVE. That it is to be defined in the
following way, and used carefully:

x = y if and only if for all 1-ary R, R(x) iff R(y).

Now that we are in the defining mood, we can also define, for k-ary R,S,

R = S if and only if for all x_1,...,x_k, R(x_1,...,x_k) iff S(x_1,...,x_k).

What we are moving towards is a formalization of MK = Morse Kelly
theory of classes. But really flat MK. No primitive relation between
objects.

Before I give the formalization of MK in this setup, I would like to
hear from radicals and moderates whether this is moving toward the
"eradication of evil" that is so ardently desired.

Harvey Friedman