Towards an untyped proof of Con(NF)

TL;DR

This paper explores a novel untyped approach to proving the consistency of Quine's New Foundations set theory by leveraging ZF with automorphisms and external bijections, avoiding type considerations.

Contribution

It introduces a new untyped proof framework for NF's consistency, utilizing ZF with automorphisms and a modified Boffa construction model.

Findings

NF can be interpreted within ZF with automorphisms and external bijections

The approach avoids type-based reasoning in proving NF's consistency

A modified Boffa construction model supports the interpretation

Abstract

The idea of this approach towards proving the consistency of Quine's New Foundations set theory is to go in a completely untyped manner. So no contemplation about types is utilized here. All conceptualization pivots around proving a handful many axioms that are completely untyped and framed in the usual language of set theory, and proven to be equivalent to NF. Here, it'll be shown that if we assume the consistency of ZF plus an automorphism and an external bijection with suitable internalization of subsets of its domain and codomain, then NF would be interpreted in this system using a modification of Boffa construction models.