Relating Quine's NF to Feferman's EM (Q1288960)

A strong applicative system \(\text{PCL}^*_2+\text{UMID}\) is translated into Quine's NF almost literally: stratification for arising comprehension axioms mostly assigns \(0\) to individuum variables and 1 to second-order variables. Translation of partial recursive operations and application uses ideas from untyped \(\lambda\)-calculus. To get a translation into a subsystem NFU(pair), known to be consistent, extensionality in \(\text{PCL}^*_2\) is restricted to non-empty sets, and the principle UMID of uniform monotone inductive definitions is replaced by its non-uniform version MID. A theory \(\text{nu}\)-\(\text{BAT}^*_2\) of explicit mathematics is then interpreted in \(\text{PCL}^*_2+ \text{MID}\) and hence proved consistent, answering positively a question posed by G. Jäger: Is \(\text{POW}^+\) (strong power type axiom) consistent with non-uniform comprehension?