$\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.

Quotienting the delay monad by weak bisimilarity

The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos).Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.

A generalization of Nash's theorem with higher-order functionals

The recent theory of sequential games and selection functions by Escardó & Oliva is extended to games in which players move simultaneously. The Nash existence theorem for mixed-strategy equilibria of finite games is generalized to games defined by selection functions. A normal form construction is given, which generalizes the game-theoretic normal form, and its soundness is proved. Minimax strategies also generalize to the new class of games, and are computed by the Berardi–Bezem–Coquand functional, studied in proof theory as an interpretation of the axiom of countable choice.

THE FINE STRUCTURE OF THE INTUITIONISTIC BOREL HIERARCHY

In intuitionistic analysis, a subset of a Polish space like ℝ or ${\cal N}$ is called positively Borel if and only if it is an open subset of the space or a closed subset of the space or the result of forming either the countable union or the countable intersection of an infinite sequence of (earlier constructed) positively Borel subsets of the space. The operation of taking the complement is absent from this inductive definition, and, in fact, the complement of a positively Borel set is not always positively Borel itself (see Veldman, 2008a). The main result of Veldman (2008a) is that, assuming Brouwer's Continuity Principle and an Axiom of Countable Choice, one may prove that the hierarchy formed by the positively Borel sets is genuinely growing: every level of the hierarchy contains sets that do not occur at any lower level. The purpose of the present paper is a different one: we want to explore the truly remarkable fine structure of the hierarchy. Brouwer's Continuity Principle again is our main tool. A second axiom proposed by Brouwer, his Thesis on Bars is also used, but only incidentally.

The Borel Hierarchy Theorem from Brouwer's intuitionistic perspective

In intuitionistic analysis, Brouwer's Continuity Principle implies, together with an Axiom of Countable Choice, that the positively Borel sets form a genuinely growing hierarchy: every level of the hierarchy contains sets that do not occur at any lower level.

Modified Bar Recursion

We introduce a variant of Spector's bar recursion (called "modified bar recursion'') in finite types to give a realizability interpretation of the classical axiom of countable choice allowing for the extraction of witnesses from proofs of Sigma_1 formulas in classical analysis. As a second application of modified bar recursion we present a bar recursive definition of the fan functional. Moreover, we show that modified bar recursion exists in M (the model of strongly majorizable functionals) and is not S1-S9 computable in C (the model of total functionals). Finally, we show that modified bar recursion defines Spector's bar recursion primitive recursively.

On the computational content of the axiom of choice

We present a possible computational content of the negative translation of classical analysis with the Axiom of (countable) Choice. Interestingly, this interpretation uses a refinement of the realizability semantics of the absurdity proposition, which is not interpreted as the empty type here. We also show how to compute witnesses from proofs in classical analysis of ∃-statements and how to extract algorithms from proofs of ∀∃-statements. Our interpretation seems computationally more direct than the one based on Gödel's Dialectica interpretation.

The Lindelöf Tychonoff Theorem and choice principles

It is an important result in frame theory that the coproduct of a family of regular Lindelöf frames is Lindelöf [3]. We show that this ‘Lindelöf Tychonoff Theorem’ or ‘LTT’ is independent of ZF and indeed lies close in logical strength to the Axiom of Countable Choice, quite unlike the case with the usual (frame) Tychonoff Theorem. Along the way we construct the regular Lindelöf coreflection and obtain a simple proof of the LTT as a corollary.