Formal Topology

The completeness theorem for first-order logic is not valid constructively, as shown by Gödel and Kreisel, and so cannot be expressed in Type Theory. There exists however a natural constructive topological reformulation which has been analysed by Thierry Coquand and Jan Smith. In particular, they showed how to derive from this a simple proof of a conservativity result. Further study, jointly with G. Sambin and P. Aczel, has revealed the fundamental status of inductively defined formal topologies. P. Aczel has found an equivalent suggestive definition (set-based condition), while we have found connections between this notion and the notion of tree sets, introduced by K. Petersson and D. Synek. In a joint work with G. Sambin and S. Sadocco we have analysed these conditions for topologies connected arising in first-order logic. We are now working an a counter-example showing that there are natural complete Heyting algebra in Type Theory that are not inductively defined.

We intend to further investigate connections between the foundations of Formal Topology and inductive definitions.

Last modified: Wed May 27 14:10:09 MET DST 1998