Pretopologies and completeness proofs

Pretopologies were introduced in [S] and there shown to give a complete semantics for a propositional sequent calculus BL here called basic linear logic1, as well as for its extensions by structural rules, ex falso quodlibet or double negation. Immediately after the Logic Colloquium '88, conversation with Per Martin-Lof helped me to see how the pretopology semantics should be extended to predicate logic; the result now is a simple and fully constructive completeness proof for rst order BL and virtually all its extensions, including usual, or structured, intuitionistic and classical logic. Such a proof clearly illustrates the fact that stronger set-theoretic principles and classical metalogic are necessary only when completeness is sought with respect to a special class of models, such as usual two-valued models. To make the paper self-contained, I brie y review in section 1 the denition of pre-topologies; section 2 deals with syntax and section 3 with semantics. The completeness proof in section 4, though similar in structure, is sensibly simpler than that in [S], and this is why it is given in detail. In section 5 it is shown how little is needed to obtain completeness for extensions of BL in the same language. Finally, in section 6 connec