From Newsgroup: sci.logic

Hi,

But you might then experience the problem
that the usual extensionality axiom of
set theory is not enough, there could
be two quine atoms y = {y} and x = {x}
with x=/=y.

On the other hand SWI-Prolog is convinced
that X = [X] and Y = [Y] are the same,
it can even apply member/2 to it since
it has built-in rational trees:

/* SWI-Prolog 9.3.25 */
?- X = [X], Y = [Y], X == Y.
X = Y, Y = [Y].

?- X = [X], member(X, X).
X = [X].

But Peter AczelrCOs Original AFA Statement was
only Uniqueness of solutions to graph equations,
whereas today we would talk about Equality =

existence of a bisimulation relation.

Bye

Hi,

you do need a theory of terms, and a specific one

You could pull an Anti Ackerman. Negate the
infinity axiom like Ackerman did here, where
he also kept the regularity axiom:

Die Widerspruchsfreiheit der allgemeinen Mengenlehre
Ackermann, Wilhelm - 1937 https://www.digizeitschriften.de/id/235181684_0114%7Clog23

But instead of Ackermann, you get an Anti (-Foundation)
Ackermann if you drop the regularity axiom. Result, you
get a lot of exotic sets, among which are also the

famous Quine atoms:

x = {x}

Funny that in the setting I just described , where
there is the negation of the infinity axiom, i.e.
all sets are finite, contrary to the usually vulgar
view, x = {x} is a finite object. Just like in Prolog

X = f(X) is in principle a finite object, it has
only one subtree, or what Alain Colmerauer
already postulated:

Definition: a "rational" tre is a tree which
has a finite set of subtrees.

Bye

--- Synchronet 3.21a-Linux NewsLink 1.2