We develop an axiomatic set theory — the Theory of Hyperfinite Sets THS— which is based on the idea of the existence of proper subclasses of large finite sets. We demonstrate how theorems of classical continuous mathematics can be transfered to THS, prove consistency of THS, and present some applications.

In this article ‡ we show how the universe of HST, Hrbaček set theory admits a system of subuniverses which keep the Replacement, model Power set and Choice, and also keep as much of Saturation as it is necessary. This gives sufficient tools to develop the most complicated topics in nonstandard analysis, such as Loeb measures.

This article establishes the existence of a definable , countably saturated nonstandard enlargement of the superstructure over the reals. This nonstandard universe is obtained as the union of an inductive chain of bounded ultrapowers . The underlying ultrafilter is the one constructed by Kanovei and Shelah [10].

We demonstrate that the special model axiom SMA of Ross admits a natural formalization in Kawai's nonstandard set theory KST but is independent of KST. As an application of our methods to classical model theory, we present a short proof of the consistency of the existence of a k+ like k-saturated model of PA for a given cardinal k.