Programme

Voveodsky used the classical Quillen model structure on simplicial sets to build a model of univalent type theory. It has been noticed that, conversely, it is actually possible to start from presheaf models of univalent type theory and build a Quillen model structure on the presheaf category instead. This is interesting for constructive mathematics since it is possible to give models of univalent type theory in a constructive metatheory (and formalise this description in Agda). While this method does not work for simplicial sets, it can be used to build constructively a (Quillen) equivalent model structure on cartesian cubical sets, corresponding to what Grothendieck called “in a sense, the simplest test category” (Pursuing Stacks, p. 47–48). I will then sketch how this can be used constructively to describe the injective model structure on cubical presheaves.

Part of this work is joint work with Steve Awodey, Evan Cavallo, Emily Riehl and Christian Sattler.

This talk consists of two parts. In the first part: “Towards a constructive theory of distributions”, we look into some problems on constructivising the theory of distributions. In the second part: “A new direction in constructive reverse mathematics”, we propose a subsystem of intuitionistic finite-type arithmetic, and look into the monotone completeness theorem within the subsystem. The second part is a joint work with Takako Nemoto.

Just as in the long term the only solution for a sustainable life and development should be the radical one, namely zero emissions and zero wastes, so the search for a neutral position in the foundations of constructive mathematics should be the equally radical one, that is, zero ontological and epistemological assumptions. It is here claimed that the Minimalist Foundation (MF), introduced and developed by the author in collaboration with M.E. Maietti since 2005, completely fulfils this purpose.

Roughly speaking, MF can be seen as obtained from Martin-Löf type theory by keeping propositions distinct from sets, by adding a notion of collection, and by avoiding closure principles (as universes and well-orders). Using the three primitive notions of set, collection and proposition also in their dependent form, one gets all other notions, such as element, subset, relation, operation, function.

MF does not postulate the existence of anything; in particular, it is not an axiomatic theory, and thus no universe of sets is required. Operatively, the word set is used to refer to a certain kind of situation in which one has rules to generate effectively all elements. Similarly for propositions and collections. One can thus observe (not assume!) that sets are closed under usual constructions, such as products and sums. Propositions obey intuitionistic logic, which is explained by a principle of reflection.

Absolutely no assumptions are made connecting different notions (the only exception could be the principle propositions-into-sets introduced by Maietti in her formal system for MF). In particular, the power of a set is not a set, but a collection; this makes MF fully predicative. Also, MF does not validate the so-called axiom of unique choice. This means that one can talk about Brouwer’s choice sequences (again, with no ontological assumptions) as ideal points of a suitable pointfree topology without confusing them with lawlike sequences, rather than expunge them from the domain of constructive mathematics, as Bishop did.

All common foundations of mathematics are obtained as extension of MF in a modular way. This means that adding a principle, for example LEM, does not affect (in)validity of other principles. This makes MF the ideal framework to determine which principles are necessary to prove certain results (reverse mathematics).

The Minimalist Foundation [1,2] can be used to study and compare the existing foundations for neutral constructivism.

Indeed we can interpret the appropriate level of MF in most relevant constructive foundations including Aczel’s Constructive Set Theory, Martin-Löf’s type theory, Homotopy Type Theory, the Calculus of Constructions and the internal type theory of toposes (and quasi-toposes) by preserving the meaning of logical operators and set theoretic constructors. Furthermore the mentioned type theories can be obtained from a level of MF in [2] by the addition of specific rules.

We can then use such interpretations and their categorical semantics to discriminate between the Minimalist Foundation and every other mentioned foundation by focusing on the nature of existential quantifiers, exponentiation and compatibility with classical foundations, including predicative classical ones.

Our goal is then to transfer such an analysis to the extension of MF, called MFic, with inductive definitions in [3] and coinductive ones suitable to represent Sambin’s generated positive topologies.

The main issue is then how to strengthen the target predicative foundations at a minimum with suitable principles to meet our purpose. In particular we show that MFic can be interpreted in Martin-Löf’s type theory by preserving the meaning of the various constructors if the latter is extended with Palmgren’s notion of superuniverse.

1. Maietti, M.E., Sambin, G., Toward a minimalist foundation for constructive mathematics, in L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48 in Oxford Logic Guides,pp. 91–114. Oxford University Press (2005)

2. Maietti, M.E., A minimalist two-level foundation for constructive mathematics, Annals of Pure and Applied Logic 160(3), 319–354 (2009)

3. Maietti, M.E., Maschio S. and Rathjen M., A realizability semantics for inductive formal topologies, Church’s Thesis and Axiom of Choice, arXiv:1905.11966 (2019)

\(\newcommand{\HA}{\mathrm{HA}}\)Brouwer [1] claimed that every function from the Baire space to the natural numbers is induced by a neighbourhood function whose domain admits bar induction. We show that Brouwer’s claim is provable in intuitionistic arithmetic in all finite types (\(\HA^\omega\)) for definable functions of the system. The proof does not rely on elaborate proof theoretic methods such as normalisation or ordi- nal analysis. Instead, we internalise in \(\HA^\omega\) the dialogue tree interpretation of Gödel’s system T due to Escardó [2]. The interpretation determines a syntactic translation of terms, which yields a neighbourhood function from a closed term of \(\HA^\omega\) with the required property. Applications of this result include uniform continuity of definable functions on the Cantor space, closure under the rule of bar induction, and closure of bar recursion for the lowest type with a definable stopping function.

1. L. E. J. Brouwer, Über Definitionsbereiche von Funktionen, Mathematische Annalen, 97:60–75, 1927.
2. M. Escardó, Continuity of Gödel’s system T definable functionals via effectful forcing, Electron. Notes Theor Comput. Sci., 298:119–141, 2013.
3. T. Kawai, Representing definable functions of \(\HA^\omega\) by neighbourhood functions, Annals of Pure and Applied Logic, 170 (8):891–909, 2019.

It is generally accepted that the origin of music and language is one and the same. Thus far, there have been proposed many syntactic theories in music, however, all these efforts mainly concern generative syntax. Since these simple tree constructions are weak in representing mutual references in the tree, we propose the annotation in modal logic, by which the accessibility from each pitch event to regions, that represent local keys, are clarified. In addition, while the generative syntax constructs the tree in the top-down way, the modal interpretation gives the progressive view that is more familiar to our human recognition of music.

Keywords: Generative Syntax · Modal Logic · Kripke semantics

\(\newcommand{\Sm}{ {\mathbf{Set} } }\newcommand{\E}{ {\mathcal{E} } }\)Most models of constructive mathematics arise from so-called “triposes” (Hyland, Johnstone and Pitts) over \(\Sm\), i.e. finite limit preserving functors \(F : \Sm\to\E\) where \(\E\) is a topos and every \(A\in\E\) arises as subquotient of some \(FI\). Typically, the topos validates many propositions contradicting classical logic, e.g. in case of number and function realizability it validates the assumptions of RUSS and INT, respectively.

If one wants to “neutralize” this “gain” one may consider the topos \(\E{\downarrow}F\) together with the forgetful (“codomain”) functor \(P_F : \E{\downarrow}F\to\Sm\) having both adjoints which are full and faithful. In categorical logic this construction is known as “(Artin) glueing”.

In many cases this construction can be used to obtain models of constructive mathematics all whose theorems hold also in \(\Sm\) but still refute classically valid principles which are refuted by \(\E\).

IFP is a logical system for program extraction developed by Ulrich Berger and many collaborators, and I am also engaged in the project. IFP is an extension of first-order logic by inductive and coinductive definitions, and one can extract programs from proofs about absract mathematical objects like real numbers. In this talk, we explain IFP with the focus on extraction of partial programs. Partial data appear naturally when one considers computations on abstract mathematical objects. For example, some practical functions on real numbers, like division, are partial functions and a program for division has to start non-terminating computation on some input, and one can form a non-redundant representation of real numbers, called infinite Gray code, if one admit partiality in the representation. One of the features of IFP is that the target language of IFP has general recursion and one can extract a program that may not terminate on some input. For example, one can extract a program to convert signed digit representation to infinite Gray code from a proof. Actually, this proof uses important feature of IFP like Archimedean induction, treatment of Harrop formula, and so on. In this talk, we also mention extension of IFP with parallel program extraction, which is needed for the converse conversion.

We present a new constructive model of univalent type theory based on cubical sets. The difference from earlier work on similar models is that it depends neither on “diagonal cofibrations” nor on connections or reversals. The key idea is to weaken the notion of fibration from the cartesian cubical model so that it is not necessary to assume that the diagonal on the interval is a cofibration. Our notion of fibration coincides with that of the existing cartesian and De Morgan cubical set models in the presence of the additional structures of the respective models. This notion of fibration also gives rise to a model structure, generalizing earlier work of Sattler to cubical sets without connections. (This is joint work with Evan Cavallo and Andrew Swan.)

In homotopical models of type theory, such as cubical sets, homotopy propositions (types where any two elements are propositionally equal) can have non-trivial structure. Any two points need to be connected by a path, but they don’t need to be strictly equal. Although it seems at first that this structure can be easily used to show countable choice holds in cubical sets, it turns out on closer inspection that the opposite is the case. When working in a metatheory where all functions are continuous even weak versions of countable choice fail in CCHM cubical sets, as well as several very weak consequences of choice. One of these statements is purely homotopical: “the product of countably many copies of the circle is connected” does not hold in this setting. Others come from set theory: weak instances of collection and subset collection also fail. This technique can be used to give independence proofs for both homotopy type theory and constructive set theory.

We provide a partial solution to the problem of defining a constructive version of Voevodsky’s simplicial model of univalent foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent classifying fibration for small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, \(\Sigma\)-types, \(\Pi\)-types and a univalent universe, leaving only a coherence question to be addressed. Joint work with Simon Henry (Masaryk University). A preprint is available as arXiv:1905.0628

Inspired by [4], we introduce a notion of nucleus for types to generalize the syntactic translation of Gödel’s System T that we study in [5].\( \newcommand{\eqdef}{:\equiv} \newcommand{\J}{\mathsf{J}} \) A nucleus is an endofunction \(\J\) on types equipped with terms

\[ \eta : \rho \to \J \rho \qquad \kappa : (\sigma \to \J \rho) \to \J \sigma \to \J \rho \]

satisfying the equations of a Kleisli extension operator. Given any nucleus \(\J\), we can translate System T extended with products and coproducts into itself. Types are translated as follows:

This corresponds to the propositional part of the Gödel-Gentzen negative translation [1] of classical logic into minimal logic. And the translation of terms corresponds to its soundness proof. Working with different nuclei, we reveal various structures of functions that are definable in System T. In the talk I will present some examples of nuclei and their applications, including those for majorizability [2], (uniform) continuity [5] and bar recursion [3].

1. Hajime Ishihara, A note on the Gödel-Gentzen Translation., Mathematical Logic Quarterly 46 (2000), no. 1, 135–137.

2. Ulrich Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer Monographs in Mathematics, 2008.

3. Paulo Oliva and Silvia Steila, A direct proof of Schwichtenberg’s bar recursion closure theorem, The Journal of Symbolic Logic 83 (2018), no. 1, 70–83.

4. Benno van den Berg, A Kuroda-style j-translation, Archive for Mathematical Logic 58 (2019), no. 5–6, 627–634.

5. Chuangjie Xu, A syntactic approach to continuity of T-definable functionals, 2019, arXiv:1904.09794 [math.LO]

This will be an expanded version of my Types 2019 talk. Extended abstract (pdf).

Many times, an existence proof in algebra, written in classical mathematics, fails to be constructive because there is a case by case reasoning without an effective test allowing us to decide, in each concrete situation, what is the case to be used. If the structure we are studying admits a geometric description, then we can interpret the classical discourse about a usual (static) algebraic structure as a constructive one about a dynamic algebraic structure. We will give some relevant examples of this technique.

We apply fundamental notions of Bishop set theory (BST), an informal theory that complements Bishop’s informal system of constructive mathematics BISH, to the theory of Bishop spaces, a function-theoretic approach to constructive topology. Within BST we develop the notions of a direct family of sets, of a direct spectrum of Bishop spaces, of the direct limit of a direct spectrum of Bishop spaces, and of the inverse limit of a contravariant direct spectrum of Bishop spaces. Within the extension of BISH with inductive definitions with rules of countably many premises, we prove the fundamental theorems on the direct and inverse limits of spectra of Bishop spaces and the duality principles between them.

• I. Petrakis, Direct spectra of Bishop spaces and their limits, 2019, arXiv:1907.03273
• I. Petrakis, Dependent sums and dependent products in Bishop’s set theory, TYPES 2018, to appear.

The presentation of the Bishop-Cheng measure theory in chapter 6 of [1] contains a number of impredicative definitions that are quite problematic from a constructive viewpoint. Three problems in particular block a direct formalization of this theory in constructive set theory or in Martin-Löf type theory:

• (i) The totality of partial functions \(X \rightharpoonup Y\) is treated as a set.
• (ii) The definition of a measure space tacitly uses the powerset of \(X\) as a set.
• (iii) The definition of \(L_1\) is impredicative, as it rests on the use of the powerset of \(X\) as a set.

In his first book [2], Bishop was much more cautious to avoid the impredicativities (i) and (ii), by invoking set-indexed families of sets and subsets, which recently have been studied by Petrakis in [3]. Building on Petrakis’ definition of families of sets and families of subsets of a set, we study the corresponding notions of families of complemented subsets and partial functions. Using these tools we describe how the basic concepts of an integration space and of a measure space, together with central parts of the Bishop–Cheng measure theory, can be reformulated avoiding the aforementioned impredicativities.

(Joint work with Iosif Petrakis)

1. Bishop, E., Bridges, D. S., Constructive Analysis, Grundlehren der math. Wissenschaften. Bd. 279., Springer-Verlag, 1985, Heidelberg–Berlin–New York
2. Bishop, E., Foundations of constructive analysis, McGraw–Hill, 1967 (McGraw–Hill series in higher mathematics)
3. Petrakis, Iosif, Dependent sums and dependent products in Bishop’s set theory, submitted to TYPES 2018

Elementary part of recursion theory over intuitionistic logic is done by Kleene. Based on the interest on itself and aiming for application, I tried to develop more. In this talk, I talk about unprovability of Post’s problem and some basic properties of 1-1 reducibility.

In 1930’s, A. Heyting introduced so-called Heyting arithmetic (HA) with an informal semantics, called the Brouwer-Heyting-Kolmogorov (BHK) interpretation, which works as a criterion for the constructive reasoning thereafter. Note that HA is based on intuitionstic logic and one can obtain classical arithmetic (PA) just by adding the law of excluded middle (A or not A) into the axioms of HA. Though the sentences provable in HA are valid in the (informal) sense of the BHK interpretation, it seems not that all the sentences valid in the BHK interpretation are provable in HA. Thus some weak fragment of the law of excluded middle seems to be contained in the arithmetic which exactly obeys the BHK interpretation. Motivated from this observation, the structure (derivability relation) of weak logical principles has been studied over Heyting arithmetic and its extension in all finite types. In fact, the weak logical principles are closely related to various kinds of realizability, which can be seen as formal treatments of the BHK interpretation. To show that one logical principle A does not imply another principle B, one typically uses appropriate forms of realizability to show that A has a certain semi-constructive interpretation which B does not. In this talk, we overview the known structure of the weak logical principles and discuss about the relation with the variations of realizability.

(Joint work with Stefano Berardi, University of Torino, Italy.)

A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega implies the provability of first order classical logic LKID with inductive definitions in Martin-Löf’s style and conjectured the equivalence. The 2017 paper by the authors of this talk showed the conjecture is false. The paper considers a statement called 2-Hydra in these two systems with the first-order language formed by 0, the successor, the natural number predicate, and a binary predicate symbol used to express 2-Hydra. The paper shows that the 2-Hydra statement is provable in CLKID-omega, but the statement is not provable in LKID. This talk improves the proof of the 2017 paper to present a simpler proof.

In this talk, we will overview recent approaches to calibrate the first-order strength of Ramsey’s theorem for pairs and two colors \(({\rm RT}^2_2)\). Cholak/Jouckusch/Slaman showed that the \(\Pi^1_1\)-part of \({\rm WKL}_0+{\rm RT}^2_2\) is weaker than \({\rm I}\Sigma^0_2\) and asked whether it is \(\Pi^1_1\)-conservative over \({\rm B}\Sigma^0_2\) or not. Since then, there are large number of studies to answer this question with various approaches. Here, we will see a characterization of the \(\Pi^0_n\)-part of \({\rm WKL}_0+{\rm RT}^2_2\), and a new candidate for a counterexample of \(\Pi^1_1\)-conservation provided by recent studies of models of arithmetic.

One at-first-puzzling feature of constructive mathematics is the pervasive use of apartness relations and similar notions: dual counterparts to classically familiar predicates. Mike Shulman shows in arXiv:1805.07518 [1] that many such notions can be seen as arising from a translation of linear logic into intuitionistic logic.

In this mostly expository talk, I will give a quick introduction to linear logic, and present Shulman’s analysis of its appearance in constructive mathematics via a Chu construction translation.

I will also begin with a short polemical aside on non-decidable syntax, as discussed in arXiv:1604.03851 [2].

1. Mike Shulman, Linear logic for constructive mathematics, 2018, arXiv:1805.07518

2. Henrik Forssell, Peter LeFanu Lumsdaine, Constructive reflection principles for regular theories, 2016, arXiv:1604.03851

Homotopy type theory is an extension of Martin-Löf type theory with a new axiom (the univalence axiom) and new type formers (higher inductive types). As it relies on an axiom, it does not satisfy the canonicity property of Martin-Löf type theory, which states that every closed natural number is definitionally equal to a numeral. Nevertheless, it is now known to have a constructive interpretation, and several implementations of it have been given.

I will give several examples of computations in homotopy type theory, related to the homotopy groups of spheres in algebraic topology, including computations that we haven’t been able to perform yet. I will not assume any prior knowledge of homotopy type theory.

The Arrow–Hahn existence theorem for representing a continuous, locally nonsatiated preference relation on a closed convex subset of \(N\)-dimensional Euclidean space is generalised, without requiring local nonsatiation, to the context of certain locally compact metric spaces. In order to accomplish this, convexity is replaced by a new geometrical condition, the uniform ball-centre distance property on compact sets. The talk is set in the framework of Bishop’s constructive analysis.