Background essays (the material I've tried to understand in leading up to this question):
- Daghighi, et. al. [2014], "The foundation axiom and elementary self-embeddings of the universe."
- Dimonte [2017], "I0 and rank-into-rank axioms."
- To some extent, I've also tried to invoke Dougherty[92] in my application of my (attempt at) understanding, here, but I'm not sure I'll need to address this material specifically in this MathOF question. C.f. Dimonte[18] even so, however.
The idea of an infinite antitone sequence of e.e.'s in this case is meant as follows: there is an infinite sequence of self-embedded models such that the critical point of any is smaller than that for , but the output of on each such point is ordered in reverse size, so that e.g. , etc. I asked both Paul Corazza and J. D. Hamkins about how this would cohere with a strict axiom of foundation, and they confirmed the answer that my intuition taught me to expect, i.e. that strict foundation would rule such a sequence out.
However, assume a different axiom involving well-founded sets, viz. an axiom of parafoundation, which allows for sets to exist with any of the foundation-theoretic properties, e.g. there are (possible) sets such that , where the difference in the subscripts for the -notation marks out how the same set ( here) sustains multiple foundation-theoretic relations. The third base case is then for infinite descending sequences.
Assume, then, that at some finite stage of the 's, some establishes some set that has some elements in a well-founded way, and other elements in a hyperfounded way. We might write something like:
Now, is it possible to identify the 's as sharpened embeddings (embeddings where at least one of a model's factor is a sharp)? I ask this on the basis of Dimonte talking about how careful we have to be about well-foundedness and iterated embeddings, and his discussion of sequences of sharpened embeddings. Technically, I would be satisfied even if it turned out just that some sequence of Icarus embeddings might be permissibly antitone per the above parameters, in case there are blunt Icarus embeddings and not only sharp ones (I don't understand what I'm reading yet to know if blunt Icaroi are possible, though). I will freely admit that my reasons for trying to build a set theory with an infinite antitone sequence of e.e.'s is bizarre bordering on preposterous, but I will not explain why this is so for now. I just would like to know how possible the "situation" would be, how much work there is yet to be done to smooth out the appearance of consistency between the axiom of the antitone sequence and the axiom of parafoundation (in the hope that the appearance can indeed be smoothed out!).