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