• Types, Sets and Constructions
• Workshop: Constructive Mathematics

• Schedule
• Participants

I first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every T0-space is separable and every discrete space is countable. It follows that intuitionistic logic does not show the existence of a non-separable metric space, or an uncountable set with decidable equality, even if we assume principles that are validated by function realizability, such as Dependent and Function choice, Markov's principle, and Brouwer's continuity and fan principles.

Recorded talk

(joint work with Gregor Svindland)

We give an overview over our recent study in the field of constructive convex analysis.

Recorded talk

Publications:
[1] Josef Berger and Gregor Svindland. Convexity and constructive infima. Arch. Math. Logic, 55, 2016.
https://doi.org/10.1007/s00153-016-0502-y.
[2] Josef Berger and Gregor Svindland. A separating hyperplane theorem, the fundamental theorem of asset pricing, and Markov's principle. Ann. Pure Appl. Logic, 167, 2016.
https://doi.org/10.1016/j.apal.2016.05.003.
[3] Josef Berger and Gregor Svindland. Constructive convex programming. In Proof and Computation. World Scientic, 2018.
https://doi.org/10.1142/11005.
[4] Josef Berger and Gregor Svindland. Convexity and unique minimum points. Arch. Math. Logic, 2018.
https://doi.org/10.1007/s00153-018-0619-2.

The usual formulation of Brouwer's Theorem ('every bar is inductive')involves quantification over infinite sequences of natural numbers. We propose an alternative formulation that avoids infinite sequences and instead uses a coin ductive definition to express the bar property. In the talk I will present some arguments why the coinductive formulation behaves better in the context of program extraction from proofs than Brouwer's original formulation. 

Recorded talk

Aczel propsed CZF as a foundation for constructive mathematics and gave an interpretation of it in Martin-Löf type theory. He then extended the theory with the Regular Extension Axiom and gave an interpretation of that using Martin-Löf type theory wit W-types. Later, he studied non-wellfounded set theroy with an anti-foundation axiom. Ingrid Lindstrrom gave an interpretation of that theroy in Martin-Löf type theory. The motivation for CZF as a foundation for constructive mathematics may still be relevant for some, but we prefer to work directly in type theory - in particular, Nuprl. However, the interpretations of CZF and it non-wellfounded versions are interesting and illustrate the use of some interesting types in Nuprl. [more]

Recorded talk

I present some of Ishihara's fundamental contributions to Bishop-style constructive analysis, and their consequences. Among the areas discussed in the talk are: Ishihara's tricks; pseudoboundedness and Ishihara's principle BD-N; Hahn-Banach and separation theorems;   smoothness, duality, and locatedness. The talk was originally presented in Kanazawa at the conference in honour of Hajime’s 60th birthday.

Recorded talk

Boolean algebras play a key role in the foundations of classical mathematics. And a similar role is played by Heyting algebras for constructive mathematics. But this is not the end of the story, as a look at pointfree topology reveals. A Boolean locale is a complete Boolean algebra regarded as a pointfree space. A spatial Boolean locale is just a discrete space, at least classically. As usual, things go quite differently intuitionistically. First of all, "discrete" and "Boolean" become orthogonal concepts: unless LEM holds, the only discrete and Boolean locale is the trivial one (i.e. the powerset of the empty set). Even worse, there exists essentially no non-trivial locale which is both Boolean and overt. So Boolean locales cannot be presented as formal topologies with a positivity predicate. On the other hand, Boolean locales have some features which make them interesting also from an intuitionistic viewpoint. For instance, every locale has a smallest dense sublocale (Isbell's density theorem) which is Boolean. Now, is there any way to retain these interesting features of Boolean locales and, at the same time, to recover some of what is lost of their classical properties, such as overtness? Sambin's notion of an overlap algebra (o-algebra for short) could be the answer. My aim is to provide evidence for this statement. Classically, the definition of an o-algebra can be understood as a "negation-free" axiomatization of a complete Boolean algebra. After recalling Sambin's original definition as well as a characterization of o-algebras in terms of formal topologies, I shall illustrate some of the results we have been able to obtain so far: (i) o-algebras are always overt; (ii) atomic o-algebras are the same thing as discrete spaces; (iii) the smallest fiberwise dense (in the sense of Johnstone) sublocale of an overt locale is an o-algebra, and every o-algebra arises in this way (which is manifestly a version of Isbell's density theorem); (iv) every open sublocale of an o-algebra is itself an o-algebra. Besides these facts, many problems are still open, such as an explicit characterization of spatial o-algebras.

References:
C., Overlap Algebras as Almost Discrete Locales, arXiv:1601.04830 (2016)
C. and Maietti and Toto, Constructive version of Boolean algebra, Logic Journal of the IGPL 21 (2013)
C. and Sambin, The overlap algebra of regular opens, JPAA 214 (2010)

Recorded Talk

Standard philosophical approaches to intuitionistic logic move from philosophical considerations to propose the exclusive adoption of intuitionistic logic in mathematics. This is the case, for example, of Brouwerian intuitionism and Dummett’s well-known semantic argument for intuitionistic logic. Prominent constructive mathematicians today propose an entirely different route to intuitionistic logic, as they offer intra-mathematical reasons for developing mathematics on the basis of intuitionistic logic, that is, reasons which arise directly from the mathematical practice. One motive for developing constructive mathematics is its greater generality over classical mathematics and its ability to express meaningful distinctions, as already advanced by Bishop (1973) and particularly emphasized by Richman (1990). The most renowned reason for constructive mathematics is its distinctive computational character, as clearly realised already by Bishop (1967) (see also Bridges and Revees 1999). In this talk, I discuss this approach to constructive mathematics and investigate which philosophical conclusions can we draw from it. I frame my analysis in relation to a current position in the philosophy of mathematics which goes under the name of naturalism and claims that the only authoritative standards in the philosophy of mathematics are those of science.

Bibliography:
E. Bishop, Foundations of Constructive Analysis. New York: McGraw-Hill, 1967.
E. Bishop, Schizophrenia in Contemporary Mathematics (American Mathematical Society Colloquium Lectures), Missoula: University of Montana; reprinted in Errett Bishop: Reflections on Him and His Research, American Mathematical Society Memoirs 39.
D. Bridges and S. Revees, Constructive mathematics, in theory and programming practice, Philosophia Math. (3) 7, 1999.
F. Richman, Intuitionism as generalization, Philosophia Math. (2) 5, 1990

(joint work with Tatsuji Kawai)

Bar induction is originally discussed by L. E. J. Brouwer under the name of “bar theorem” in his intuitionistic mathematics but first formalized in a workable form by S. C. Kleene probably in late 1950’s.On the other hand, in his posthumously published paper [1], C. Spector gave a consistency proof of classical analysis by using the Dialectica interpretation with a fundamental principle so-called “bar recursion”. As already mentioned in [1], bar recursion is some analogue of bar induction in the sense that bar recursion is a principle of definition and bar induction is a corresponding principle of proof. In particular, the formalized bar theorem is informally compared with bar recursion for continuous functions with computable modulus in [1, 6.4 with footnote 6 written by G. Kreisel]. In this talk, we formally investigate the relation between bar theorem and bar recursion for continuous functions, which is classically valid while bar recursion in general is not so. Among other things, we show that bar recursion for continuous functions with continuous modulus of type N^N → N is derivable from the decidable bar induction of type N (namely, the formalized bar theorem) in intuitionistic arithmetic in all finite types augmented with the axiom scheme of countable choice and also that the converse is the case in intuitionistic arithmetic in all finite types augmented with the characteristic principles of the Dialectica interpretation.

References:
[1] C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In F. D. E. Dekker, editor, Recursive Function Theory: Proceedings of Symposia in Pure Mathematics, volume 5, pp. 1--27. American Mathematical Society, Providence, Rhode Island, 1962.

Recorded talk

Bridges and Havea have given a constructive analysis of the convexity of the numerical range and what we can hope for in a constructive setting. In this talk we concentrate on constructive challenges regarding the boundary and border of the numerical range.

Recorded talk

Martin-Löf's type theory has strong existential elimination (dependent sum type) what allows to prove the full axiom of choice. However the theory is intuitionistic. We give a condition on strong existential elimination that makes it computationally compatible with classical logic. With this restriction, we lose the full axiom of choice but, thanks to a lazily-evaluated coinductive representation of quantification, we are still able to constructively prove the axiom of countable choice, the axiom of dependent choice, and a form of bar induction in ways that make each of them computationally compatible with classical logic. Because the proof is constructive, it directly yields the conservativity of classical arithmetic over intuitionistic arithmetic for Σ⁰₁-formulae in the presence of the above axioms.

Recorded Talk

The Hahn-Banach theorem, named after the mathematicians Hans Hahn and Stefan Banach who proved it independently in the late 1920s, is a central tool in functional analysis. The theorem has several forms:

1. The continuous extension theorem, which enables the extension of a bounded linear functional defined on a subspace of a normed space to the whole space;

2. The separation theorem, which enables a separation of two convex subsets of a normed space by a hyperplane, and has numerous uses in convex analysis (geometry);

3. The dominated extension theorem, which is the most general form of the theorem, and enables the extension of a linear functional, defined on a subspace of a normed space and dominated by a sublinear function, to the whole space.

We review the constructive (approximate) separation theorem, given by Bishop, and the construc-tive (approximate) continuous extension theorem as its corollary. Then, with the help of geometric properties of a Banach space such as uniform convexity and Gateaux differentiability of the norm, and without invoking Zorn's lemma, we discuss an exact version of the separation theorem and the continuous extension theorem for normable linear functionals on nonseparable spaces.

We introduce the notions of a subderivative and a Gateaux derivative of a convex function, and see a relationship between subdifferentiablity, and the separation theorem and the dominated extension theorem. Finally, we describe a constructive version of the Mazur theorem by using the constructive Baire theorem, and two of its corollaries: the constructive (approximate) separation theorem and the constructive (approximate) dominated extension theorem.

Recorded talk

Starting from Hilbert's Programme, we discuss how computation became a central notion in mathematical foundations. Special emphasis is put on the distinction of syntax and semantics. 

I show that the domain of Godel's system-T definable functional from the Baire space to the natural numbers satisfies bar induction.

Recorded talk

We discuss two representations of real numbers, namely Cauchy-sequences of rationals and signed-digit(sd)-code. We prove how to translate between the two and then use the translations to prove some statements in connection with exact real arithmetic, e.g. division for sd-code. In contrast to the (usually) complicated proofs these will be almost trivial.

We work in a pure constructive context, minimalist, à la Bishop. Constructive real algebra is not well understood. In fact constructive real algebra is fairly distinct from the usual theory of discrete real closed fields, where a sign test is assumed to be given for the order structure. Most theorems of discrete real algebra fail from a constructive point of view because there is no sign test for constructive real numbers. Searching to describe the purely algebraic properties of a constructive real number system (e.g. the one of Bishop), we consider that a good way is to construct a geometric theory, as complete as possible, whose a model should be any of the proposed constructive real number systems in the literature. For the external language, e.g. when we speak about models, we want also to use some weak form of constructive set theory, with intuitionist logic. We also need a very uniform theory, avoiding properties that can be proven only with the use of dependant choice (as somme results in Bishop's book). A first attempt, when searching for a coherent theory, leads us to the theory of local real closed rings. The theory of real closed rings can be given in a purely equational form. And the fact that a real number field is a local ring is a way to formulate the dichotomy for overlapping intervals: if x+y >0, then x>0 or y>0 (with an explicit “or''). But the theory seems still unsatisfactory and incomplete. We think it is necessary to add new sorts in order to describe in a more uniform way the properties of semialgebraic continuous functions on a compact cube. We see in this new context that some infinitary axioms appear to be important and necessary. So we pass from a coherent theory to a more general geometric theory. Finally we hope to obtain a good geometric theory for o-minimal structures. This is a confirmation of our moto: the constructive field of real numbers is nothing else than the first example of constructive o-minimal structures.

Recorded Talk

Since antiquity, mathematical proofs were realized by logical conclusions and constructive procedures rooted in everyday routines of practitioners (e.g., compass and ruler in geometry or counting and computing rules in arithmetic). Later on, constructions were extended by machines, and, nowadays, we use computers for applications of algorithms. The logic of constructive practice is intuitionistic, while classical logic was abstracted from the mathematics of finite sets, “forgetful of this limited origin, … without justification to the mathematics of infinite sets” (H. Weyl). Thus, in the age of computers and algorithms, mathematics with intuitionistic logic seems to be justified by technical practice and need of control and no longer by the ideological polarization of a “Grundlagenstreit”. But, the question arises how far modern mathematics can be reconstructed and justified by constructive procedures? What are the possibilities and limitations of constructive methods in, e.g., Brouwer’s intuitionism, predicative mathematics, constructive recursive mathematics, constructive reverse mathematics, Bishop’s constructive mathematics, or Martin-Löf’s constructive type theory? Besides these foundational questions, there are practical challenges of constructive mathematics in physics, financial mathematics, and computer science. Thus, nowadays, constructive mathematics has also a deep societal impact.

References:
E. Bishop, Foundations of Constructive Analysis, Ishi Press Internal 2012
E. Bishop, D. Bridges, Constructive Analysis, Springer 1985
K. Mainzer, Wie berechenbar ist unsere Welt. Herausforderungen für Mathematik, Informatik und Philosophie im Zeitalter der Digitalisierung (Reihe Essentials), Springer 2018
K. Mainzer, The Digital and the Real World. Computational Foundations of Mathematics, Science, Technology, and Philosophy, World Scientific: Singapore 2018
K. Mainzer, P. Schuster, H. Schwichtenberg (Eds.), Proof and Computation. Digitization in Mathematics, Computer Science, and Philosophy, World Scientific: Singapore 2018.

Recorded talk

In classical mathematics, Kolmogorov’s axiomatic theory is the standard paradigm for probability. However, for a long time, many different non-overlapping approaches were competing: classical probability, frequentist probability, subjective probability etc. Constructively, there is no standard paradigm, yet. In this talk I will present a constructive account of frequentist probability and a constructive pointfree metric approach to probability (joint work in progress with H. Ishihara) and I will compare these two approaches to each other and with other ones in the literature.

Recorded talk

In this introductory talk, I will formulate a notion of higher-order parity automaton which extends to infinitary simply-typed λ-terms the traditional notion of parity tree automaton on infinitary ranked trees. The main result of the talk will be that the acceptance of an infinitary λ-term by a higher-order parity automaton A is decidable, whenever the infinitary λ-term is generated by a finite and simply-typed λ Y-term. The decidability theorem is established by combining ideas coming from linear logic, from denotational semantics and from infinitary rewriting theory. If you are curious and want to know more about this work, please have a look at: https://www.irif.fr/~mellies/papers/higher-order-parity-automata.pdf

In Bishop's constructive mathematics, it is known that Baire category theorem is provable. This proof requires the axiom of countable choice (cf. [1]). On the other hand, in classical reverse mathematics, their same form of Baire category theorem restricted for complete separable metric space is provable in RCA₀, which has only restricted version of countable choice (cf. [2, Theorem II.5.8]). In this talk, we will see that the proof in classical reverse mathematics also works in constructive counterpart EL₀ of RCA₀, which has only quantifier free number-number choice and ∑₁⁰ induction. We will also see that this version of Baire category theorem is enough to show the existence of nowhere differentiable continuous function on [0; 1].

References:
[1] E. Bishop, Foundations of Constructive Analysis, Mcgraw-Hill, 1967.
[2] S. G. Simpson, Subsystems of Second Order Arithmetic, Cambridge University Press, 2009.

Recorded talk

The principle of ex falso quodlibet (EFQ) states that contradiction entails everything: (A ∧ ¬A) → B. EFQ is valid in intuitionistic logic, but this is seen as problematic by Johansson, who created an alternative subsystem called minimal logic [3]. In minimal logic, EFQ is rejected albeit not entirely, as a weaker version (A ∧ ¬A) → ¬B still holds. Some subsystems of minimal logic are investigated in Colacito [1] and Colacito et al. [2] in the framework of subminimal logics. The start point for them is the observation that minimal logic has a negation axiom if ¬ rather than ⊥ is taken as primitive. Compared with minimal logic, subminimal logics have weaker negation axioms, while maintaining the positive axioms and rules. One logic they investigated was contraposition logic characterised by the axiom (p → q) → (¬q → ¬p), Some subminimal logics were shown to be subsystems of contraposition logic, but it is not well-studied what subminimal logics have contraposition logic as a subsystem. In the talk, I shall present some logics between contraposition logic and minimal logic, with a discussion of their proof-theoretic and semantic properties. In particular, I shall talk about logics which has a semantics that is a straightforward generalisation of the Kripke semantics for minimal logic. [1] Almudena Colacito, Minimal and Subminimal Logic of Negation, Master’s Thesis, University of Amsterdam, 2016. [2] Almudena Colacito, Dick de Jongh, Ana Lucia Vargas, Subminimal negation, Soft Computing, vol. 21 (2017), pp. 165–174. [3] Ingebrigt Johansson, Der Minimalkalkl, ein reduzierter intuitionistischer Formalismus, Compositio Mathematica, vol. 4 (1937), pp. 119–136.

Errett Bishop proposed several type-theoretic languages to be used for formalization of constructive mathematics. The notion of set of (Bishop-Bridges 1985) always requires a specification of an equality on each set used. This concept of set is widely employed in computer formalizations under the name setoid. These type systems used in such formalizations are often based on dependent type theory, such as Martin-Löf constructive type theory. The dependent types solves some of the problems of formalizing functions defined on subsets in the Bishop's proposals which where based on Gödel's system T. Formalising models of Martin-Löf type theory in itself provides a challenge for the development of theory of setoids, and its implementation in proof assistants. In this talk we report on progress with the setoid model of this type theory. We also give an introduction to setoids and its use formalizing Bishop style mathematics. The first two thirds of the talk do not require any detailed knowledge of dependent type theories.  

Recorded talk

We present a constructive theory of domains, geared towards computation with real numbers. In the standard representation of reals as Cauchy sequence together with modulus of convergence, the estimate of closeness given by the modulus is generally way too conservative. Our motivating example is the representation of reals as nested sequences of intervals, the width of which is (only) classically known to converge to zero. We construct (continuous) domains as completion of predomain basis, where ever element arises as a monotone sequence of basis elements. Our main results are closure under function space and a characterisation of countinuous, real-valued functions that can be constructively represented in our domain theoretic approach.

According to Bishop (see [1], p.28), the constructivization of general topology is impeded by two obstacles. First, the classical notion of a topological space is not constructively viable. Second, since uniform continuity for functions on a compact metric space is much more useful than pointwise continuity, “and since uniform continuity cannot be formulated in the context of a general topological space, the latter concept is left with no useful function to perform”. In this talk we explain how the theory of Bishop spaces can overcome these obstacles. A Bishop space is a function-theoretic notion of space that does not copy the pattern of the set-based notion of a topological space. Moreover, a Bishop morphism, the notion of morphism between Bishop spaces, generalizes the notion of uniform continuity, as in many important cases it is reduced to it. We present several such reducibility results, found in [3] and [4]. In order to show the fruitfulness of Bishop spaces, we present the fundamental results on pseudocompact Bishop spaces, found in [6], which show that pseudo-compact Bishop spaces form a constructive alternative to the classical theory of C*(X). In order to show the smooth interaction between Bishop spaces and other constructive notions of space, we give an overview of the basic results from [5], that connect Bishop spaces with uniform spaces the uniformity of which is given by pseudometrics, and from [7], that connect Bishop spaces with C-spaces, studied by Escardó and Xu in [2].

Recorded talk

References:
[1] E. Bishop: Schizophrenia in Contemporary Mathematics, American Mathematical Society Colloquium Lectures, Missoula University of Montana 1973.
[2] M. H. Escardó, C. Xu. A constructive manifestation of the Kleene-Kreisel continuous functionals. Ann. Pure Appl. Logic, 167(9), 2016, 770-793.
[3] I. Petrakis: Constructive Topology of Bishop Spaces, PhD Thesis, LMU München, 2015.
[4] I. Petrakis: A constructive function-theoretic approach to topological compactness, LICS 2016, IEEE Computer Society Publications, 2016, 605-614, DOI: 10.1145/2933575.2933582.
[5] I. Petrakis: Constructive uniformities of pseudometrics and Bishop topologies, accepted in Journal of Logic and Analysis, 42 pages.
[6] I. Petrakis: A constructive theory of C(X), part I and II, preprint, 2018.
[7] J. Geins: Bridges between the theory of Bishop spaces and the theory of C-spaces, Master’s Thesis, LMU München, 2018.

There seems to be a very close connection between category theory and constructive mathematics which still is hard to make manifest, but which may be extremely useful to improve the intuition that a practical mathematician has of explicit constructions. Categories and functors provide a very precise notion of model for logical theories, hence they may become a very practical tool to develop and strengthen constructive theories. We shall produce some instances of how to apply categorical completions to build suitable models of constructive theories. This talk draws from joint work with several people during the semester at HIM, including Steve Awodey, Jacopo Emmeneger, Jonas Frey, Maria Emilia Maietti, Paulo Oliva, Fabio Pasquali, and Davide Trotta.

Recorded talk

Both competing visions of mathematics in the past century, the thesis of formal- ism and the antithesis intuitionism, assume a notion of truth in which the quality of information is fixed (logical consistency for the former, computation for the latter). By introducing a dynamic perspective, in which all kinds of information are preserved, we can aspire to a synthesis, in which computation lives together with spatial intuition, that is, real mathematics coexists with ideal one. It is a matter of facts that in most examples of spaces effectivity lies on the side of the base, and not on that of points. In a foundation without the powerset axiom, the base is indexed on a set S, while points form a collection which is not a set. So to maximize effectivity in mathematics our aim should be to develop as much as possible of topology basing on S rather than on points. This is the simple and deep reason explaining the pointfree approach. Pointfree definitions are obtained by depositing on S as much as possible of the structure of a (topological) space. The main notion is that of positive topology, provided with a cover and a positivity relation. Positive topologies sensibly enrich and generalize previous notions, such as locales and formal topologies. On any set S, we can define in a very general and effective way (starting from an arbitrary axiom-set) a cover by induction, and a positivity relation by coinduction so that the result is a positive topology. Baire space, real numbers, Zariski topology, Scott domains,... can all be defined in this pointfree effective way. Spatial intuition, for instance the ideal notion of choice sequence, is expressed by the notion of ideal point and ideal space over a positive topology. To maximize effectivity, one should pass to points as late as possible in the course of an argument. To save both effectivity and unlimited use of spatial intuition, one should prove a conservativity result, a sort of constructive and local Hilbert program: any statement on the pointfree side which is proved using ideal points, can also be obtained without.

Recorded Talk

The semantic Universal Krull Lemma (UKL) entails the corresponding syntactical conservation principle (Con) without further ado. We show that the computation using Con which is the core of an inductive  proof of UKL is in fact equivalent to Con. This adds evidence to Con being the computational content of UKL.

Recorded talk

(joint work with Ulrich Berger, Olga Petrovska and Hideki Tsuiki)

We illustrate IFP (intuitionistic fixed point logic) by examples of program extraction and show the ongoing work of the implementation of IFP in Haskell. IFP is a variant of the logic underlying the Minlog system that emphasizes more the operator approach  to inductive and coinductive definitions. It is a intuitionistic first-order logic with axioms and rules for the least and greatest fixed point predicates, and its main application is researches on constructive analysis. In IFP, we can reason about properties  of mathematical objects like natural numbers and real numbers and extract programs on those via realizability interpretation. 

(joint work with Ulrich Berger)

Pure Gray code is a unique coding of the unit interval with {0, 1, bot} where bot means undefinedness, and Gray code is an almost unique coding of the unit interval in that only binary rational numbers are represented redundantly and the redundancy is caused by allowing 0 or 1 to the unique bot in the presented sequence. Therefore, in these codes, each digit is representing a partial information and (Pure) Gray code is a (unique) coding as a collection of partial informations. In order to manipulate such a collection of partial informations, we need concurrent executions of partial programs computing digit values. CFP is a logic for such a concurrent execution of partial programs. We show how conversions between Signed digit / Pure Gray code / Grau code can be extracted from proofs in CFP. 

Recorded talk

I will present a general algorithm for computing a finite generating set for the syzygies of any finitely generated ideal of V[X_1,...,X_k] (V a valuation domain) which does not use Gröbner bases. This algorithm is based on a notion of "echelon form" which ensures its correctness. Its termination proof is combinatorial. 

Recorded talk