The Univalent Foundations project constitutes what is arguably the most serious challenge to set-theoretic foundations of mathematics since intuitionism. Like intuitionism, it differs both in its philosophical motivations and its mathematical-logical apparatus. In this paper we will focus on one such difference: Univalent Foundations’ reliance on an intensional rather than extensional logic, through its use of intensional Martin-Löf type theory. To this, UF adds what may be regarded as certain extensionality principles, although it is not immediately clear how these principles (...) are to be interpreted philosophically. In fact, this framework gives an interesting example of a kind of border case between intensional and extensional mathematics. Our main purpose will be the philosophical investigation of this system, and the relation of the concepts of intensionality it satisfies to more traditional philosophical or logical concepts such as those of Carnap and Quine. (shrink)

This article provides a survey of key papers that characterise computable functions, but also provides some novel insights as follows. It is argued that the power of algorithms is at least as strong as functions that can be proved to be totally computable in type-theoretic translations of subsystems of second-order Zermelo Fraenkel set theory. Moreover, it is claimed that typed systems of the lambda calculus give rise naturally to a functional interpretation of rich systems of types and to a hierarchy (...) of ordinal recursive functionals of arbitrary type that can be reduced by substitution to natural number functions. (shrink)

Mancosu, P., Generalizing classical and effective model theory in theories of operations and classes, Annas of Pure and Applied Logic 52 249-308 . In this paper I propose a family of theories of operations and classes with the aim of developing abstract versions of model-theoretic results. The systems are closely related to those introduced and already used by Feferman for developing his program of ‘explicit mathematics’. The theories in question are two-sorted, with one kind of variable for individuals and the (...) other for classes. The individual variables range over a domain closed under pairing and containing, among other things, natural numbers and operations.All the theories used assume a common group of axioms that insure that the individuals in the domain satisfy the conditions for a partial combinatory algebra with pairing. We also assume a class of natural numbers and a class induction axiom on . Finally there are various class existence axioms. I work mainly with three theories, FMT0, FMT and FMTΩ, which differ from each other both in their class existence axioms as well as in some further applicative axioms.These theories have various interpretations in which every object is explicitly presented by some means of definition as well as classical, or ‘standard’, set-theoretical interpretation. The systems are formulated in a flexible general language which can be used to prove abstract theorems of mathematics , thereby generalizing recursive, hyperarithmetic and admissible versions of classical mathematics.The aim of my work is to give an abstract development of portions of model theory in the afore-mentioned theories, in a way to look as much as possible like classical mathematics. Thus, FMT0 generalizes portions of countable and recursive model theory; FMT further generalizes portions of countable and hyperarithmetical model theory and finally FMTΩ provides a generalization of the classical L-completeness theorem and of an admissible version of L-completeness due to Bruce and Keisler. This continues the development of the program mentioned above, originating with Feferman. (shrink)

This paper explores strengths and limitations of both predicativism and nominalism, especially in connection with the problem of characterizing the continuum. Although the natural number structure can be recovered predicatively (despite appearances), no predicative system can characterize even the full predicative continuum which the classicist can recognize. It is shown, however, that the classical second-order theory of continua (third-order number theory) can be recovered nominalistically, by synthesizing mereology, plural quantification, and a modal-structured approach with essentially just the assumption that an (...) -sequence of concrete atoms be possible. Predicative flexible type theory may then be used to carry out virtually all of scientifically applicable mathematics in a natural way, still without ultimate need of the platonist ontology of classes and relations. (shrink)