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

This paper, a contribution to “micro set theory”, is the study promised by the first author in [M4], as improved and extended by work of the second. We use the rudimentarily recursive functions and the slightly larger collection of gentle functions to initiate the study of provident sets, which are transitive models of $\mathsf{PROVI}$, a subsystem of $\mathsf{KP}$ whose minimal model is Jensen’s $J_{\omega}$. $\mathsf{PROVI}$ supports familiar definitions, such as rank, transitive closure and ordinal addition—though not ordinal multiplication—and Shoenfield’s unramified (...) forcing. Providence is preserved under directed unions. An arbitrary set has a provident closure, and the extension of a provident $M$ by a set-generic $\mathcal{G}$ is the provident closure of $M\cup\{\mathcal{G}\}$. The improvidence of many models of $\mathsf{Z}$ is shown. The final section uses similar but simpler recursions to show, in the weak system $\mathsf{MW}$, that the truth predicate for $\dot{\varDelta}_{0}$ formulæ is $\Delta_{1}$. (shrink)