Marco Forti, Furio Honsell, Marina Lenisa

Operations, Collections and Sets within a General Axiomatic Framework.


This paper is part of a general research programme on the Foundations of Mathematics, Logic and Computer Science, carried out since the early eighties at the the Seminar directed by Ennio De Giorgi at the Scuola Normale Superiore in Pisa. In this context, Foundations are not intended to provide {\em safe and unquestionable grounds} to {scientific activity}, but rather to provide {\em conceptual environments} where this activity can be carried out naturally and without artificial constraints. Earlier proposals of such foundational theories appear in \cite{TQ85,TA88} (see also \cite{FH89}). Further investigations, along theses lines, have been carried out by various mathematicians, logicians and computer scientists since Spring 1994, starting from the ``Basic Theories'' introduced in \cite{TB94} (see e.g. \cite{AAVV,CP95,Var94,2000,FH94,FHL95}). The principles which inspire and inform the foundational programme of E. De Giorgi are: \begin{itemize} \item {\em non-reductionism}: the fact that there are many kinds of ``qualitatively different'' objects and concepts should be taken seriously. All codings are ultimately artificial and opaque, and they can undermine the conceptual clarity of the system. In particular, blurring the distinction between {\em natural mathematical concepts} and their usual set-theoretic implementations, e.g. reducing {\em natural numbers} to {\em Von Neumann ordinals}, {\em ordered pairs} to {\em Kuratowski doubletons}, {\em binary relations} and {\em simple operations} to {\em graphs} makes it difficult, even impossible at times, to formulate appropriate axioms and conjectures. The intuitive notion of {\em operation} brings about the {\em non-extensional} concept of computation process, and so operations cannot be accounted for only in terms of graphs. Similarly, conceiving {\em collections} as {\em truth-valued operations} forces unnecessary commitments on the definition of collection, and yet it does not make apparent the crucial property of collections which is {\em extensionality}. Taking {\em natural numbers} as primitives saves us from having to fix priorities among different implementations, e.g. Frege-Russell cardinals, Von Neumann Ordinals, Church Numerals, etc.. \item {\em selfdescription}: the most relevant operations and relations which a foundational theory utilizes should themselves be objects of the theory. The principal relations and operations on collections ({\em membership, inclusion, union, relative complement, cartesian product}, etc.) should be introduced, as ``first class'' objects; similarly {\em application}, {\em abstraction} and {\em composition} of operations should themselves be operations. Moreover, various {\em qualities} should be introduced in order to classify the different {\em species} of objects, including operations,collections and qualities themselves. \item {\em open-endedness}: a foundation al theory should be open to extensions. The introduction of qualitatively new notions, both of mathematical character and of other kind, should be always possible. A foundational theory should be a framework suitable for accommodating most of classical and modern theories arising in Mathematics, Logic, Computer Science, and possibly other sciences (Economics, Linguistics, etc.). Any sufficiently clear concept should be ``engraftable'' ({\em innestabile}) in a natural way in it. For example, in \cite{CP95,con-tratto}, metamathematical notions, such as {\em formula, proposition}, and {\em interpretation} are engrafted in the open foundational theories of \cite{TB94} and \cite{2000} respectively, by introducing suitable kinds of objects together with relations and operations involving them. In \cite{Var94}, the concept of {\em variable} of classical Mathematical Physics and of Economics is engrafted, in the same style, in the theory of \cite{TB94}. Following \cite{2000}, this {\em open} character of foundational theories can be epitomized, by the words of Hamlet: ``There are more things in heaven and earth, Horatio, than are dreamt of in your philosophy'' (Hamlet, Act I, Sc.V, vv.166-167). \item {\em semiformal axiomatization}: a foundational theory should be expounded in a rigorous yet informal style and investigated using the axiomatic method of traditional mathematics. Although many first-order formalizations can be given (e.g. \cite{GLT}) none can be satisfactorily taken as definitive. In fact, any formalization misses part of the intended meaning of the original theory. Moreover, in order to keep the metatheoretic requirements to a minimum, a foundational theory should be finitely axiomatizable. \end{itemize} The present paper focuses on the concepts of {\em collection}, {\em correlation} (or {\em correspondence}), {\em set}, {\em operation} and {\em function}. As it is to be expected, many interesting alternatives arise in the process of axiomatizing these concepts. Besides giving the basic list of axioms which capture the traditional concepts of classes, functions and sets, we propose also several attractive strengthenings. Correspondingly, interesting problems of relative consistency also arise. The paper is organized as follows. In Section \ref{uno}, we introduce the first fundamental concepts of the theory, namely {\em qualities} and {\em relations}, as in \cite{2000}. In Section \ref{due} we introduce the concept of {\em operation} and develop a simplified version of the theory {\sf Oper} of \cite{FHL95}. In Section \ref{tre} we develop the general theory of {\em collections} and {\em correlations}. In Section \ref{quattro} we deal with the concepts of {\em set} and {\em function}. The theory presented in Sections \ref{tre}-\ref{quattro} is a reformulation of the theory {\sf TBCN} of \cite{FH94}, within the axiomatic framework of Section \ref{uno}-\ref{due}. Final remarks appear in Section \ref{cinque}. In the Appendix, we outline the construction of models of the whole theory axiomatized in Sections \ref{uno}-\ref{quattro}, which is thus proved to be relatively consistent with respect to {\sf ZF}.