[FOM] Concerning Flat Foundations

[Harvey Friedman]

I haven't been able to get a really useful dialog going with HoTT
related people (Steve Awodey would be useful, assuming we would stay
generally understandable), but I did get a snippet from someone
knowledgeable about HoTT. He/she says that

*) all equality is local

Well, that got me thinking about how to make Flat Foundations
http://www.cs.nyu.edu/pipermail/fom/2014-October/018337.html more
radical.

ASIDE: Do we all agree how relatively simple and generally
understandable my Flat Foundations is?

We still have sorts for objects and for each n, a sort of n-ary relations.

However, this time we will have no equality. But we still have a
problem. The same object may be in the field of two different
relations, violating principle *) above.

So what we really probably want is that

**) If two relations have a common field element then they hold of
exactly the same tuples (i.e., are extensionally equal)

Now the problem is just what should take the place of the
comprehension axioms. It is hard to imagine how we are going to
construct new relations without getting involved in relationships with
other relations. And how are we going to state relationships between
different relations without considering relations between their
fields? But then we can't even consider two such, as they will have
common field elements.

So now there are several ways to go. One is to continue to have n-ary
relations violating *) as in
http://www.cs.nyu.edu/pipermail/fom/2014-October/018337.html AND THEN
have a star operator R* which disjointifies the n-ary relations R. R**
would be the isomorphism that maps R to R*.

This seems to be a possibly attractive setup, but I am not sure how
responsive it is to the complaints coming from HoTT. Steve or others
can help me out, as I continue to adjust the greatly flexible
classical f.o.m.

I won't move this to my numbered postings until I get (and absorb)
sufficient feedback.

Harvey