Marco Forti, Furio Honsell, Marina Lenisa
Operations, Collections and Sets within a General Axiomatic
Framework.
Abstract
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}.