# [FOM] Computational set thery

Arnon Avron aa at tau.ac.il
Sun Feb 23 04:07:40 EST 2014

On Fri, Feb 21, 2014 at 10:31:40AM +0100, henk wrote:

> Set theory is a very awkward theory to represent  computations.
> It can be done in principle, by describing Turing Machines as sets
> but then the computational fun gets lost as proofs involving serious
> computing
> become unreadable. In short: set theory doesn't contain a convenient
> computational  model.

Henk - this is simply not true. It is true that computational issues
have not been a factor at the development of set theory and its
use as the foundations of math - but this is does not
mean that this is impossible in principle, using appropriate
notations and with computational-driven development of the theory.
To see work that has already been done in this direction,
I suggest that you have a look at the following two books:

\bibitem{CFO89} Cantone D., Ferro A., and Omodeo E.,
{\bf Computable Set Theory}, Clarendon Press, Oxford, 1989.

\bibitem{COP01} Cantone D., Omodeo E., and Policriti A.,
{\bf Set Theory for Computing: From Decisions Procedures to
Declarative Programming with Sets}, Springer, 2001.

or at the following work of Sazonov:

\bibitem{Sa97} Sazonov V. Y., {\em On Bounded Set Theory}, Proceedings
of the 10th International Congress on Logic, Methodology and Philosophy
of Sciences, Florence, August 1995, in Volume I: Logic and
Scientific Method, Kluwer Academic Publishers, 85-103, 1997.

or (if I may) at my own attempt, which I plan to continue as soon
as I finish another project I am in involved in:

\bibitem{Av08}  Avron A.,
{\em Constructibility and Decidability versus
Domain Independence and  Absoluteness},
Theoretical Computer Science 394 (2008), 144--158.

\bibitem{Av10} Avron A.,
{\em A New Approach to Predicative Set Theory}, In {\bf
Ways of Proof Theory} (R. Schindler, ed.), 31-63,
onto series in mathematical logic, onto verlag, 2010.

Note that my  approach is based on ideas from relational database
theory- a theory which  is all about computations with sets!

By the way, Henk, do you now disagree with the views you have expressed
about the importance and naturalness of *type-free* calculi
at the beginning of your great book on the (type-free) lambda
calculus (or in your chapter at the handbook of mathematical logic)?

Arnon