$\sigma$-locales in Formal Topology

A $\sigma$-frame is a poset with countable joins and finite meets in which binary meets distribute over countable joins. The aim of this paper is to show that $\sigma$-frames, actually $\sigma$-locales, can be seen as a branch of Formal Topology, that is, intuitionistic and predicative point-free topology. Every $\sigma$-frame $L$ is the lattice of Lindel\"of elements (those for which each of their covers admits a countable subcover) of a formal topology of a specific kind which, in its turn, is a presentation of the free frame over $L$. We then give a constructive characterization of the smallest (strongly) dense $\sigma$-sublocale of a given $\sigma$-locale, thus providing a "$\sigma$-version" of a Boolean locale. Our development depends on the axiom of countable choice.

General Recursion and Formal Topology

It is well known that general recursion cannot be expressed within Martin-Löf's type theory and that various approaches have been proposed to overcome this problem still maintaining the termination of the computation of the typable terms. In this work we propose a new approach to this problem based on the use of inductively generated formal topologies.

ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION

Completeness and other forms of Zorn’s Lemma are sometimes invoked for semantic proofs of conservation in relatively elementary mathematical contexts in which the corresponding syntactical conservation would suffice. We now show how a fairly general syntactical conservation theorem that covers plenty of the semantic approaches follows from an utmost versatile criterion for conservation given by Scott in 1974.To this end we work with multi-conclusion entailment relations as extending single-conclusion entailment relations. In a nutshell, the additional axioms with disjunctions in positive position can be eliminated by reducing them to the corresponding disjunction elimination rules, which in turn prove admissible in all known mathematical instances. In deduction terms this means to fold up branchings of proof trees by way of properties of the relevant mathematical structures.Applications include the syntactical counterparts of the theorems or lemmas known under the names of Artin–Schreier, Krull–Lindenbaum, and Szpilrajn. Related work has been done before on individual instances, e.g., in locale theory, dynamical algebra, formal topology and proof analysis.

Generalized geometric theories and set-generated classes

We introduce infinitary propositional theories over a set and their models which are subsets of the set, and define a generalized geometric theory as an infinitary propositional theory of a special form. The main result is thatthe class of models of a generalized geometric theory is set-generated. Here, a class$\mathcal{X}$of subsets of a set is set-generated if there exists a subsetGof$\mathcal{X}$such that for each α ∈$\mathcal{X}$, and finitely enumerable subset τ of α there exists a subset β ∈Gsuch that τ ⊆ β ⊆ α. We show the main result in the constructive Zermelo–Fraenkel set theory (CZF) with an additional axiom, called the set generation axiom which is derivable inCZF, both from the relativized dependent choice scheme and from a regular extension axiom. We give some applications of the main result to algebra, topology and formal topology.

The axiom of multiple choice and models for constructive set theory

We propose an extension of Aczel's constructive set theory CZF by an axiom for inductive types and a choice principle, and show that this extension has the following properties: it is interpretable in Martin-Löf's type theory (hence acceptable from a constructive and generalized-predicative standpoint). In addition, it is strong enough to prove the Set Compactness theorem and the results in formal topology which make use of this theorem. Moreover, it is stable under the standard constructions from algebraic set theory, namely exact completion, realizability models, forcing as well as more general sheaf extensions. As a result, methods from our earlier work can be applied to show that this extension satisfies various derived rules, such as a derived compactness rule for Cantor space and a derived continuity rule for Baire space. Finally, we show that this extension is robust in the sense that it is also reflected by the model constructions from algebraic set theory just mentioned.