PRL Seminars

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.