Is the anti-foundation axiom considered constructive?

626 Views Asked by At

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?

1

There are 1 best solutions below

6
On

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.