PolySets

Pragmatic considerations arising in the formalisation of 
mathematics (using tools such as Isabelle, HOL4, ProofPower ...) 
can be seen to motivate the adoption of non-well-founded 
foundational ontologies.
These considerations also yield intuitions about the kinds of 
non-well-founded sets which are desirable.
Inductively defined classes of well-founded sets may be used to 
represent a domain which includes both the well-founded sets and 
the desired non-well-founded sets.

By such means we arrive at PolySets.
Some of the motives and intuitions will be described, together 
with details of the construction of the PolySets.

The PolySets appear to meet those desiderata most closely related 
to the intuitions on which they were based, but not all the 
desiderata.
The methods used can be strengthened and generalised providing a 
framework in which one might speak of "the open ended nature of 
non-well-founded sets" and in which the incoherent ideal of full 
infinitary comprehension can be approached.
This more general "framework" will be sketched.