We present a theory of stratified truth with a μ‐operator, where terms representing fixed points of stratified monotone operations are available. We prove that is relatively intepretable into Quine's (or subsystems thereof). The motivation is to investigate a strong theory of truth, which is consistent by means of stratification, i.e., by adopting an implicit type theoretic discipline, and yet is compatible with self‐reference (to a certain extent). The present version of is an enhancement of the theory presented in [2].

Tangled Type Theory was introduced by Randall Holmes in [3] as a new way of approaching the consistency problem for$\mathrm {NF}$. Although the task of finding models for this theory is far from trivial (considering it is equiconsistent with$\mathrm {NF}$), ways of constructing models for certain fragments of it have been discovered. In this article, we present a simpler way of constructing models of predicative Tangled Type Theory and consequently of predicative$\mathrm {NF}$. In these new models of predicative$\mathrm {NF}$, the (...) universe is well-orderable and equinumerous to the set of singletons. (shrink)

This paper presents an exposition of subsystems and of Quine's , originally defined and shown to be consistent by Crabbé, along with related systems and of type theory. A proof that (and so ) interpret the ramified theory of types is presented (this is a simplified exposition of a result of Crabbé). The new result that the consistency strength of is the same as that of is demonstrated. It will also be shown that cannot be finitely axiomatized (as can and (...) ). (shrink)

The usual construction of models of NFU (New Foundations with urelements, introduced by Jensen) is due to Maurice Boffa. A Boffa model is obtained from a model of (a fragment of) Zermelo–Fraenkel with Choice (ZFC) with an automorphism which moves a rank: the domain of the Boffa model is a rank that is moved. “Most” elements of the domain of the Boffa model are urelements in terms of the interpreted NFU. The main result of this paper is that the restriction (...) of the membership relation of the original model of set theory with automorphism to the domain of the Boffa model is first-order definable in the language of NFU. In particular, all information about the extensions in the original model of the urelements of the model of NFU is definable in terms of NFU. A corollary (answering a question of Thomas Forster) is that the urelements in a Boffa model are not homogeneous. (shrink)

This paper extends the results of an earlier paper by the author . New subsystems of the combinatory logic TRC shown in that paper to be equivalent to NF are introduced; these systems are analogous to subsystems of NF with predicativity restrictions on set comprehension introduced and shown to be consistent by Crabbé. For one of these systems, an exact equivalence in consistency strength and expressive power with the analogous subsystem of NF is established.

A common objection to Quine's set theory "New Foundations" is that it is inadequately motivated because the restriction on comprehension which appears to avert paradox is a syntactical trick. We present a semantic criterion for determining whether a class is a set which motivates NF.

A common objection to Quine’s set theory “New Foundations” is that it is inadequately motivated because the restriction on comprehension which appears to avert paradox is a syntactical trick. We present a semantic criterion for determining whether a class is a set (a kind of symmetry) which motivates NF.