[FOM] 556: Flat Foundations 1

Wed Oct 29 16:07:14 EDT 2014

For a long time, there have been complaints about ZFC and fragments
thereof as foundations for mathematics, in that the universe comes
with too much structure - the epsilon relation - that is irrelevant to
standard mathematical purposes. These complaints, as well as more
subtle complaints, have been forcefully reiterated by a new community
of categorically oriented scholars working on what they call HoTT.

Flat Foundations is based on a modification of the standard f.o.m.
through ZFC and fragments. Instead of having a single sort for sets
with epsilon,=, we have a sort for objects and sorts for relations on
objects of each arity. There is no epsilon relation between objects.
We think of the 1-ary relations on objects as classes (of objects).

With regard to equality, we can take it as primitive, or we can define
equality in a natural way.

IA very natural axiom in this setup asserts a very strong equivalence
between relations:

*every bijection between limited classes extends to a permutation of
all objects*

and this axiom has immediate consequences. E.g.,

**any two isomorphic limited structures have the same global properties**

If one goal is to make "isomorphic structures identical in some
sense", then there is more to do. But just how I should go about doing
this would preferably be guided by interaction with the categorical
foundations people including the HoTT people. So far, I have not been
able to secure such a communication line. There could be major
incompatibilities in language here. However, I know of at least one
person working with the HoTT community who is f.o.m. savvy, and I am
hoping to interact with him/her in the near future.

FLAT Z WITH EQUALITY
FZ(=)
WARNING: This will turn out to be a little stronger than the usual
Zermelo set theory = Z.

We have lower case letters ranging over sets. For each n >= 0, we have
upper case letters ranging over n-ary relations on the objects. We
have = between objects only. The atomic formulas are v = w,
R(v_1,...,v_n), where v,w,v_1,...,v_n are object variables, and R is
an n-ary relation variable. We use quantifiers over objects, and
quantifiers over relations of any given arity. Formulas are built up
as usual using connectives and quantifiers.

NOTE: In anticipated interaction with categorical foundationalists, I
may want to take up FZF without equality.

1. Equality axioms. These are the standard quantifier free equality
axioms in many sorted logic. We can derive the standard ones that
allow arbitrary formulas.

2. Comprehension axioms. (there exists R)(for all
x_1,...,x_n)(R(x_1,...,x_n) iff phi), where phi is any formula in
which R is not free.

DEFINITION 1. The domain of a binary relation R is the class of all
possible first arguments. The multivallues of R are the sections of R
obtained by fixing by the first argument.

DEFINITION 2. The field of any n-ary relation R is the class of all x
that used in R. A sectionizer for R is a binary relation S such that
every subclass of the field of R is a multivalue of S. R is
sectionable if and only if R has a sectionizer.

3. Infinity. There is a sectionable irreflexive transitive relation
with no maximal element.

4. Power Set. Every sectionable relation has a sectionable sectionizer.

FLAT ZF WITH EQUALITY
FZF(=)
WARNING: This will turn out to have the strength of Morse-Kelly.

1-4.
5. Every binary relation with a sectionable domain, whose multivalues
are all sectionable, is sectionable.

We can optionally use the Axiom of Choice.

6. Axiom of Choice. Every binary relation contains a binary relation
with the same domain, whose multivalues each have exactly one element.

It is now natural to present an axioms that tell us that isomorphic
sectionable structures have the same global properties. This is in
line with complaints about ZFC from categorical foundationalists, but
as i said earlier, I would like to interact with them to see how I
should go further and make Flat Foundations more radical.

DEFINITION 3. A structure is a nonempty class (domain) together with
finitely many relations of various arities whose field is included in
the domain. We write (D,R_1,...,R_k). We can incorporate constants and
functions in the obvious way.

7. Sectionable Equivalence. Let M =  (D,R_1,...,R_k) and M' =
(D',R_1',...,R_k') be two isomorphic structures whose domains are
sectionable. Then phi(M) iff phi(M'). Here phi is a formula in the
language whose free variables are among D,R_1,...,R_k.

Sectionable Equivalence follows formally form this:

8. Every bijection between two sectionable classes can be extended to
a bijection from the class of all objects onto the class of all
objects.

There are stronger forms of 7,8.

9. Strong Sectionable Equivalence. Let M =  (D,R_1,...,R_k) and M' =
(D',R_1',...,R_k') be two isomorphic structures where the complements
of their domains are not sectionable. Then phi(M) iff phi(M'). Here
phi is a formula in the language whose free variables are among
D,R_1,...,R_k.

10. Every bijection between two sectionable classes can be extended to
a bijection from the class of all objects onto the class of all
objects.

Perhaps categorical people don't like even being able to talk about an
object in the domain of one structure being equal to an object in the
domain of a different structure? That probably can be accomodated by
some standard f.o.m. formal language moves. Maybe we want to abolish
equality between objects altogether? There is always going to be a
defined equality relation - we learned that from Leibniz. So this may
creep unless we take some more radical steps. One is to just work with
isomorphism classes of structures, and somehow never even get into an
element of an isomorphism class. There are too many possibilities for
dealing with these issues, and so I need to engage categorical
foundationalists at this point. Steve Awodey?? Good choice, as long as
we stay generally understandable.

************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 556th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-527 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2014-August/018092.html

528: More Perfect Pi01  8/16/14  5:19AM
529: Yet more Perfect Pi01 8/18/14  5:50AM
530: Friendlier Perfect Pi01
531: General Theory/Perfect Pi01  8/22/14  5:16PM
532: More General Theory/Perfect Pi01  8/23/14  7:32AM
533: Progress - General Theory/Perfect Pi01 8/25/14  1:17AM
534: Perfect Explicitly Pi01  8/27/14  10:40AM
535: Updated Perfect Explicitly Pi01  8/30/14  2:39PM
536: Pi01 Progress  9/1/14 11:31AM
537: Pi01/Flat Pics/Testing  9/6/14  12:49AM
538: Progress Pi01 9/6/14  11:31PM
539: Absolute Perfect Naturalness 9/7/14  9:00PM
540: SRM/Comparability  9/8/14  12:03AM
541: Master Templates  9/9/14  12:41AM
542: Templates/LC shadow  9/10/14  12:44AM
543: New Explicitly Pi01  9/10/14  11:17PM
544: Initial Maximality/HUGE  9/12/14  8:07PM
545: Set Theoretic Consistency/SRM/SRP  9/14/14  10:06PM
546: New Pi01/solving CH  9/26/14  12:05AM
547: Conservative Growth - Triples  9/29/14  11:34PM
548: New Explicitly Pi01  10/4/14  8:45PM
549: Conservative Growth - beyond triples  10/6/14  1:31AM
550: Foundational Methodology 1/Maximality  10/17/14  5:43AM
551: Foundational Methodology 2/Maximality  10/19/14 3:06AM
552: Foundational Methodology 3/Maximality  10/21/14 9:59AM
553: Foundational Methodology 4/Maximality  10/21/14 11:57AM
554: Foundational Methodology 5/Maximality  10/26/14 3:17AM
555: Foundational Methodology 6/Maximality

Harvey Friedman