Relating Quine's NF to Feferman's EM
type: Item
instance of: scholarly article
title: Relating Quine's NF to Feferman's EM
zbMATH Open document ID: 0923.03068
DOI: 10.1023/A:1026495301622
published in: Studia Logica
publication date: 1999-10-18T00:00:00Z
review text: 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?
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03E70
zbMATH DE Number: 1289851
zbMATH Keywords: Quine's New Foundations
zbMATH Keywords: consistency
zbMATH Keywords: strong power type axiom
zbMATH Keywords: applicative system
zbMATH Keywords: comprehension
zbMATH Keywords: translation
zbMATH Keywords: uniform monotone inductive definitions
zbMATH Keywords: explicit mathematics
author: Andrea Cantini
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: a:1026495301622
OpenAlex ID: W1517950697
description: scientific article; zbMATH DE number 1289851