Formal logic has different "fragments" that allow different kinds of reasoning. This paper focuses on a fragment called sigma-coherent logic, which is a version of geometric logic restricted to countable collections of symbols and rules, but allowed to express infinitely long statements involving countably infinite lists of alternatives (disjunctions). The central question is whether the proof system for this logic is "complete," meaning that everything that is true can actually be proved. The paper provides clean, self-contained proofs that this completeness holds, covering both a simpler propositional version (where statements have no variables ranging over objects) and a richer predicate version (where statements can quantify over individuals in a mathematical structure).
A key insight is that the collection of models satisfying a given theory has natural topological structure. In the propositional case, this collection forms a kind of generalized topological space called a quasi-Polish space, a well-studied class of spaces that generalizes both complete metric spaces and certain spaces arising in theoretical computer science. Logical formulas, when considered up to provable equivalence, correspond exactly to continuous functions on this space of models. This means logic and topology are secretly describing the same thing, and completeness falls out of this correspondence.
The predicate case is richer and more technically involved. Here the models form not just a space but a category, meaning there are also structure-preserving maps between models to keep track of. The paper shows that the relevant category of models is a quasi-Polish category, and logical formulas correspond to continuous functors, which are maps that respect both the categorical and topological structure. The authors also explore an analogy with a classical topological concept called sobriety, which captures when a space can be perfectly reconstructed from its collection of open sets, and they develop a version of this idea suited to these topological categories of models.