Introduction to nonwell-founded set theory

Question

I'm interested in playing with nonwell-founded variants of set theory and weaker/different axioms of induction/extensionality.

I have a hunch coalgebraic methods could better handle weirdness like modelling homotopy type theory.

I also have just been interested in the idea of coinduction as primitive as opposed to induction.

Weak limits like weak function spaces are also useful in Computer Science for higher order abstract syntax. So set-theory minus induction/extensionality could lead to cleaner encodings of stuff like the lambda calculus.

But I really don't know where to start with nonwell-founded set theory in the first place. Unfortunately nonwell-founded set theory seems a bit esoteric.

Answer 1

Here is one entrypoint to a particular family of non-well-founded set theories, New Foundations and its descendants.

All variants of New Foundations have a universal set $U$ and have $U \in U$ as a theorem, so none of them are well-founded.

Versions of New Foundations without urelements have the same extensionality axiom as ZFC. Adding urelements forces us to restrict extensionality to sets with at least one element, but this is not a large modification of the axiom extensionality. It is the same modification one would make to add atoms to ZFC.

Here's the Wikipedia page on New Foundations. It starts with Russellian type theory, which does not take the key step of erasing types outside of comprehension contexts and so isn't in the New Foundations family per se.

Randall Holmes has a web page describing New Foundations.

Metamath has a proof database for New Foundations.

Answer 2

One version of non-well founded set theory arises when we replace the Axiom of Foundation with the Anti-Foundation Axiom (AFA), explored in an influential book written by Peter Aczel in 1988.

The obvious place to start finding out more about this is the Stanford Encyclopaedia article https://plato.stanford.edu/entries/nonwellfounded-set-theory/