I am one of the authors of this preprint. Concerning the Grothendieck Universe, my first answer is this. Some terms of Flow are called ZF-sets. Through the use of our restriction axiom we are able to define a term u which acts on all ZF-sets. That means x belongs (membership relation is defined from the concept of action in Flow) to u iff x is a ZF-set. Next we prove u satisfies all conditions of a Grothendieck Universe. Concerning self-referential definitions, that is something we intend to fix for a next version of this work. Somehow we missed that important issue. Sorry about that. Concerning consistency of Flow, we should be very careful: if Flow is consistent, then we have a model of ZF where PP holds but AC is not valid. We are still considering questions regarding relative consistency. Anyway, it has been a great pleasure to collect all those first criticisms to our work.
In response to a question in comments:
The idea of Theorem 55 is something like this. AC is equivalent to the statement that every set can be well-ordered. So, if we want to prove AC does not hold, we need to exhibit a ZF-set which cannot be well-ordered. We chose a hyperfunction psi. But an analogous proof can be done to certain well-founded ZF-sets (unless, obviously, we made some mistake - that is why this is just a preprint). We suppose psi can be well-ordered. That means it is possible to fix (to define) an injection from psi into some ordinal o. And that is supposed to be recursively definable in a similar way how Zermelo's theorem is proven. Zermelo's theorem takes into account AC to prove every set can be well-ordered. Instead of AC we have our F-Choice axiom. By using recursively F-Choice, every time we define an injection from a proper restriction of psi into some ordinal, in the next step of such a transfinite recursion we "loose information" about some terms which belong to psi that were previously fixed in the previous step. Some terms previously fixed are no longer fixed, and we simply do not know who are those terms. That happens because F-Choice axiom demands the existence of an injection g whose domain is a restriction of a given surjection f but such that g itself is no restriction of f. That is why the concept of lurking functions is quite important within our proposal. In Zermelo's theorem that is not an issue, since AC is used. All terms which were previously assigned to an ordinal by means of AC, keep their assignment during all next steps of transfinite recursion. Our motivation is our focus on functions rather than sets. We hope our F-Choice axiom is strong enough to grant PP but too weak to grant AC.
