Non-Well-Founded Set Theories

Non-well-founded set theories allow ‘self-referential’ or circular sets which can refer to themselves in that they are elements of itself. Alternatively, infinitely descending $\in$-sequences (i.e., $x_0\ni x_1\ni \cdots \ni x_{n-1}\ni x_n\ni \dots$)

i.e., $Q=${$1,2,3,Q$}

The Quine atom $x=$ {$x$}

Non-well-founded sets cannot have the regular axiom of extensionality due to infinitely descending sequences we do not have a ‘starting point’ to show sets have the same elements.

Quine’s New Foundations(NF)

• Allows for a universal set $U:=\{x|x=x\}$, the set of all sets $\to P(U)=U$ and $P(U)\in U,U\in P(U)$
• Does not allow for quine atoms
• Utilizes stratified levels of formulae (similar to type theory)

Urelements are objects which are not sets, introducing them into set theory means it is no longer a ‘pure’ set theory $\to$ i.e., if $U$ is a urelement, then $x\in U$ makes no sense, although set can contain urelements, i.e., $U\in x$

Stratification: A formula $\phi$ is stratified if it can be ‘turned’ into a WFF of STT (simple type theory) via assigning type subscripts to variables. $\to$For variables $x$ and $y$, $x_n\in y_{n+1}$ is well-formed while $x_n\in y_n$ is not well-formed as they are of the same level (only the equality symbol ’=’ can be used between variables of the same level).

Axiom of Stratified Comprehension: $\forall x\exists y\forall x(z\in y\leftrightarrow \Phi (x,z))$ for $\Phi$ is a formula of STT and $y$ is not free in $\Phi$ The formation of sets is restricted to stratified formulae.

• NF is inconsistent w/ the axiom of choice (that is NF $⊢2^{{\aleph }_0}\ne {\aleph }_1$)
• NF is finitely axiomatizable (finite number of axioms, no axiom schemas)

Aczel’s Graph Theory

• Any set that can be described by a graph is a valid set (allows for loops, and Quine atoms)
• Has a (proper) class of all sets rather than a universal set
• Bisimulations to replace axiom of extensionality

Anti-Foundation Axiom (AFA): AFA loosely asserts that any object than can be ‘described’ by a graph are sets. Naturally, this includes ill-founded sets which will contain loops.

Bisimulation: A bisimulation is a binary relation $R$ between two models of a theory (called systems w/in the context of computer science). The intuition behind it is that it acts as a notion of equality for non-well-founded sets.

$R$ is a bisimulation on a model or system $M$ if $R\subseteq R^{+}$ i.e., The class of ordered pairs $R$ is a subclass of the class of ordered pairs $R^{+}$ (recall that binary relations can be thought of as a class of ordered pairs).

A maximum bisimulation is the largest possible bisimulation between two structures, that is, it is not the subclass of another bisimulation relation. It is the union of all bisimulation relations between any two structures.

If $R$ is a bisimulation of $M$ then for all $a,b\in M$, then $aRb⟹a{\equiv }_{M}b$

Proposition: For each system $M$ the relation ${\equiv }_M$ is an equivalence relation on $M$ such that for all $a,b\in M$, then $a{\equiv }_M^{+}b⟺a{\equiv }_{M}b$

If $M$ is a system, then for all $a,b\in M$ i) $a_M=b_M⟹a{\equiv }_{M}b$ ii) $Ma\cong Mb⟹a{\equiv }_{M}b$

A system $M$ is extensional if for all $a,b\in M$ $a_M=b_M⟹a=b$

A system $M$ is strongly extensional if for all $a,b\in M$ $a{\equiv }_{M}b⟹a=b$

References

Philosophy of Sets & Proper-Classes Type Theory