# 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?

• Maybe interesting: www1.maths.leeds.ac.uk/~rathjen/ANTI.pdf – Martín-Blas Pérez Pinilla Jan 5 '15 at 16:29
• The only thing I know is that the foundation axiom can be applied constructively. But does that exclude the reverse? – Han de Bruijn Jan 8 '15 at 20:24
• I suppose this is one of those questions that you could upgrade to mathoverflow.net... unless you get a convincing answer here (mine isn't) in the next 24hrs. – Fizz Jan 11 '15 at 17:43

• 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
• 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