We examine the conditions under which a model of Tangled Type Theory satisfies the same sentences as a model of (assuming we ignore type indices).

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)

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].