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