Standard sets in nonstandard set theory

We prove that Standardization fails in every nontrivial universe definable in the nonstandard set theory BST, and that a natural characterization of the standard universe is both consistent with and independent of BST. As a consequence we obtain a formulation of nonstandard class theory in the ∈-language.

An axiomatic presentation of the nonstandard methods in mathematics

A nonstandard set theory *ZFC is proposed that axiomatizes the nonstandard embedding *. Besides the usual principles of nonstandard analysis, all axioms of ZFC except regularity are assumed. A strong form of saturation is also postulated. *ZFC is a conservative extension of ZFC.

An axiomatics for nonstandard set theory, based on von Neumann–Bernays–Gödel Theory

We present an axiomatic framework for nonstandard analysis—the Nonstandard Class Theory (NCT) which extends von Neumann–Gödel–Bernays Set Theory (NBG) by adding a unary predicate symbol St to the language of NBG (St(X) means that the class X is standard) and axioms—related to it—analogs of Nelson's idealization, standardization and transfer principles. Those principles are formulated as axioms, rather than axiom schemes, so that NCT is finitely axiomatizable. NCT can be considered as a theory of definable classes of Bounded Set Theory by V. Kanovei and M. Reeken. In many aspects NCT resembles the Alternative Set Theory by P. Vopenka. For example there exist semisets (proper subclasses of sets) in NCT and it can be proved that a set has a standard finite cardinality iff it does not contain any proper subsemiset. Semisets can be considered as external classes in NCT. Thus the saturation principle can be formalized in NCT.

Processes as terms: non-well-founded models for bisimulation

A compositional semantics characterizing bisimulation equivalence is derived from transition system specifications in the SOS style, satisfying certain syntactic syntactic conditions. We use Aczel's nonstandard set theory for solving a recursive equation for a domain fo processes. It contains non-well-founded elements modelling possibly infinite behaviour. Semantic interpretations of syntactic operators are obtained by defining the operational semantics for terms consisting of both syntactic and semantic (processes)entities. Finally, we return to standard set theory by observing that a similar, though less general, result can be obtained with the use of complete metric spaces.