On Extensionality, Uniformity and Comprehension in Explicit Mathematics


Andrea Cantini
Dipartimento di Filosofia
Universit`a degli Studi di Firenze, Italy
cantini@mailserver.idg.fi.cnr.it

Abstract

The informal intuitions behind Feferman's explicit mathematics naturally hint at a radically non-extensional ontology. In particular, there is a tension between uniform class comprehension and class extensionality.

This is exemplified by a few negative results, which lift recursion theoretic techniques to applicative theories of operations and classes, and imply formal refutations of class extensionality and power class existence.

On the positive side, we show that class extensionality is consistent with non-trivial principles of uniform comprehension, (and yet it forces simple class constructors, e.g. singleton, not to be uniformly given by an internal operation). The basic idea is to apply Feferman's method for generating partial combinatory algebras to models of provably consistent fragments of Quine's NF.