[FOM] Computational set thery

[Arnon Avron]

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
> of quadruples,
> 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