# Is the anti-foundation axiom considered constructive?

In the area of theoretical computer science that I am interested in, constructive mathematics is of practical interest because it gives algorithms that can be implemented on a computer. However, non-well-founded set theory is also of practical interest, since many of the phenomenon that we wish to model are circular or non-well-founded in nature.

The anti-foundation axiom can be stated in a number of ways, including the following.

Every system of equations $\varepsilon$ has a unique solution.

Every graph $G$ has a unique decoration.

This axiom, in all the formulations of it that I have found, seems to me to be decidedly non-constructive, since the axiom simply asserts that there exists a solution or a decoration, but does not give any way to actually construct these. However, in practice, such a solution often can be found (for instance using Tarski's fixed point theorem), so my question is simply: does the wider mathematical and philosophical community consider the anti-foundation axiom to be constructive or not, or is it perhaps still a fairly open question?

I think the answer should be no. I'm not a researcher in this field (or even in math), so I can't say if my opinion is in any way aligned to some "mainstream math" community, but the more general Wikipedia article on non-well-founded set theory (warning: to which I have contributed myself some edits in the past) lists some alternatives to Aczel's axiom and has some interesting comparison papers.

What is interesting about these alternatives is that an order (inclusion) theorem can produced, which says basically that the von Neumann universe is included in Aczel's (and in turn that is included in Scott's etc.) So my argument is simply that you'd have to consider von Neumann's universe constructive too by inclusion if you consider Aczel's this way. And I think that's not commonly done, although Godel's constructible universe might count as such, but that's not the whole von Neumann's universe. On this latter point, I find it unsatisfying that Wikipedia's article on constructivism doesn't mention Godel's constructible universe in any way, neither as example nor as a "false friend", but I guess that's a different question.

• No one says that the universe is "constructive". Given a graph, can you constructively say what is the unique set corresponding to that graph? In $\sf ZF$ the answer is yes. Transitive graphs has a unique collapse to a transitive set, and you can pick the relevant subset uniquely by knowing the original graph. – Asaf Karagila Jan 11 '15 at 16:45
• Ok, then I guess I don't understand the question. I thought it was really asking if Aczel's set theory is considered a constructive set theory. – Fizz Jan 11 '15 at 17:00
• For my edification, is the Axiom of regularity/foundation considered constructive in the sense that you mean it here? – Fizz Jan 11 '15 at 17:03
• I'm probably the wrong person to ask that, since I don't know a whole lot about constructive mathematics. But I suspect that the answer is positive. Given a graph that "can" have a decoration in $\sf ZF$, we can uniquely single out the set just from the graph in with all the isomorphisms and embeddings being uniquely definable from the graph itself (transitive closure, the collapse to a set, then the restriction of the collapse function to the original graph). – Asaf Karagila Jan 11 '15 at 17:06
• Well, I suppose you're right, depending on the meaning of "constructive" in mathematics, of which there are several. Indeed a common meaning for "constructive" is just "provable in ZF (sans C)"; but there are narrower meanings, which actually lead to IZF, CZF and so forth. If anything came out this discussion insofar is that we need to define constructive first, before we can answer the question. – Fizz Jan 11 '15 at 17:19