A Completeness Theorem for Formal Topologies

The main mathematical result of this work is a quite simple formulation and proof of a Rasiowa-Sikorski-like theorem for countable lattices. Then the paper suggests an interpretation of this mathematical result as a completeness theorem for the formal topologies introduced by G. Sambin in order to provide a constructive approach to topology which is expressible within Martin Löf’s intuitionistic theory of types. This completeness theorem shows that, as long as one is interested in dealing only with the coverage relation between two open sets of a topology, within a constructive framework, a very simple mathematical structure is needed. It is necessary to stress that the completeness theorem holds because of the “weak” intuitionistic set and subset theory that we use when dealing with formal topologies.