4 ms·
I think that the "infinite, streaming structures" that you are referring to can be modelled in ZFC or HOL using Tarski's fixed-point theorem. See for example th
by nano_o 13y ago
I think that the "infinite, streaming structures" that you are referring to can be modelled in ZFC or HOL using Tarski's fixed-point theorem. See for example the paper by L. C. Paulson, "A fixedpoint approach to implementing (co)inductive definitions".
So the point of this anti-foundation axiom probably lies somewhere else.
- tel 13y agoWhile I haven't yet read that paper, I wanted to point out a thing I just read in a coinduction tutorial (http://www.cs.ru.nl/~bart/PAPERS/JR.pdf http://www.cs.ru.nl/~bart/PAPERS/JR.pdf). Coalgebras are defined as an isomorphism between "sets" X==P(A*X) which allow us to unfold our seed state over non-determistic updates. Such a "set" obviously cannot exist in ZFC directly as it violates set cardinality. It can be a set that satisfies the AFA, though—in fact, that equation I just wrote is sufficient to define it I think and then AFA guarantees uniqueness.
- tel 13y agoI don't think that either ZFC or ZFC/AFA dominates the other, just that the AFA bakes a framework for infinite streaming structures into the heart of your mathematics. You immediately lose extensional equality in favor of bisimulation, for instance. The point is more to see what centipede mathematics feels like than to claim greater power or expressiveness.