such proof to be carried out, rekindling some interest in non-well-founded axiomatic systems. The next axiom proposal came in a 1960 congress talk of Dana Scott (never published as a paper), proposing an alternative axiom now called SAFA. Another axiom proposed in the late 1960s was Maurice Boffa's axiom of superuniversality, described by Aczel as the highpoint of research of its decade. Boffa's idea was to make foundation fail as badly as it can (or rather, as extensionality permits): Boffa's axiom implies that every extensional set-like relation is isomorphic to the elementhood predicate on a transitive class. A more recent approach to non-well-founded set theory, pioneered by M. Forti and F. Honsell in the 1980s, borrows from computer science the concept of a bisimulation. Bisimilar sets are considered indistinguishable and thus equal, which leads to a strengthening of the axiom of extensionality. In this context, axioms contradicting the axiom of regularity are known as anti-foundation axioms, and a set that is not necessarily well-founded is called a hyperset. Four mutually independent anti-foundation axioms are well-known, sometimes abbreviated by the first letter in the following list: AFA ("Anti-Foundation Axiom") – due to M. Forti and F. Honsell (this is also known as Aczel's anti-foundation axiom); SAFA ("Scott’s AFA") – due to Dana Scott, FAFA ("Finsler’s AFA") – due to Paul Finsler, BAFA ("Boffa’s AFA") – due to Maurice Boffa. They essentially correspond to four different notions of equality for non-well-founded sets. The first of these, AFA, is based on accessible pointed graphs (apg) and states that two hypersets are equal if and only if they can be pictured by the same apg. Within this framework, it can be shown that the so-called Quine atom, formally defined by Q={Q}, exists and is unique. Each of the axioms given above extends the universe of the previous, so that: V ⊆ A ⊆ S ⊆ F ⊆ B. In the Boffa universe, the distinct Quine atoms form a proper class. It is worth emphasizing that hyperset theory is an extension of classical set theory rather than a replacement: the well-founded sets within a hyperset domain conform to classical set theory. Applications Aczel’s hypersets were extensively used by Jon Barwise and John Etchemendy in their 1987 book The Liar, on the liar's paradox; The book is also a good introduction to the topic of non-well-founded sets. Boffa’s superuniversality axiom has found application as a basis