Computability is Ineffable in ZF Set Theory
Evan explained Peter Aczel's translation of the
language of set theory into type theory. I will show
that classical set theory is unable to express the
idea of computation and data used in constructive
type theory. The talk will be somewhat philosophical
but we will examine a few key points in the
development of constructive set theory, CZF, to see in what
sense it can express computational ideas.
The fact that Hopcroft and Ullman could not base their
automata theory books on classical set theory is a
practical consequence of these philosophical observations.
I will discuss some of the problems they faced in trying
to define an adequate foundational basis for their work.
What is missing from their books is a thesis, like
Church's Thesis, but for data - call it the Digital Data
Thesis. This could not be formulated with out constructive
type theory which did not come into being until after their book.