Schedule

Titles and Abstracts

Peter Aczel
Two possible principles for constructive set theory

In my talk I will formulate the two principles, discuss their significance for CST (Constructive Set Theory) and state some results concerning them.
The first principle, sigma-CP expresses a strong completeness property for intuitionistic propositional logic that implies the negations of LPO, WLPO, MP, SEP, etc, ..., but is nevertheless relatively consistent with CZF.
The second principle, RRS (Relation Reflection Scheme) is a consequence of RDC (Relative Dependent Choices Scheme) but appears not to be a choice principle, although it can be used where previously RDC has seemed to be needed.

Thorsten Altenkirch
Informative and non-informative existentials in Type Theory

Andrej Bauer
Continuity begets continuity (joint work with Alex Simpson)

Ulrich Berger
Strong normalisation via domain-theoretic computability predicates
It is well-known that intersection types on the one hand characterise the strongly normalisable lambda terms and on the other hand give rise to a syntactically defined domain model for the lambda calculus. Recently, Coquand and Spiwack have combined and extended these facts to give a domain-theoretic criteria for strong normalisability for the lambda calculus with recursively defined constants. In the talk I will show that their normalisation proof can also be carried out in an abstract axiomatic setting where the computability predicates are indexed by the elements of a (not syntactically presented) domain. The more abstract setting simplifies the proof considerably without sacrificing predicativity or constructivity.

Marian Baroni
Archimedean spaces
Archimedean ordered vector spaces are examined constructively. In the classical theory, if e is an order unit of an Archimedean space, then the Minkowski functional of the order interval [-e,e] is a norm with respect to which [-e,e] is the closed unit ball. Ishihara's theorems on the constructive existence of Minkowski functionals can be used to prove similar results constructively.

Douglas Bridges
Four seasons in constructive mathematics
Looking back over nearly 40 years as an aficionado of constructive mathematics, I will wax sentimental about a few results that brought me particular pleasure. The results will be drawn from approximation theory, complex function theory, integration theory, and mathematical economics.

Jesper Carlström
A constructive version of Birkhoff's theorem
The classical version of Birkhoff's theorem says that a class of algebras (in universal algebra) is closed under subalgebras, homomorphic images and products if and only if it is axiomatizable by equations. I will discuss a constructive version, with 'closed under inductive limits' added as a fourth condition. To get a predicative version, we also add the requirement that the class be 'set-based' in a sense typical for predicativity. Finally, I would like to comment on in which sense the proof lets us 'compute' a set of axioms for a class of algebras.

Francesco Ciraulo
A constructive semantical treatment of LJ-non-deducibility
Formal topologies have been used to give a constructive semantical characterization of deducibility in intuitionistic predicate calculus (Sambin, Coquand). I will show that the recently introduced notion of a binary positivity predicate (Sambin) is a natural tool in order to give a constructive semantic for non-deducibility (and for some related notions).

Thierry Coquand
Maximal and minimal prime ideals in constructive algebra
Using some ideas from point-free topology, one can interpret constructively the prime spectrum of a ring, and so analyse constructively proofs that use a prime ideal in a generic way. We present some analysis of proofs in commutative algebra that use a maximal or minimal prime ideal. One is a lemma used by Suslin in his solution of Serre's problem (following Yengui). The other examples are Traverso-Swan's theorem on seminormal rings, and a proof of Zariski Main Theorem due to Peskine. We present some remarks on the algorithms corresponding to these arguments, compared to algorithms corresponding to proofs using prime ideals generically.

Giovanni Curi
On some peculiar aspects of the category of formal spaces
In contrast with what happens in the topos-theoretic context, in constructive settings the category of locales or formal spaces is not locally small. A particular example shows that, as a second important difference, not every locale can be presented by a site in the sense of Johnstone (equivalently, not every formal space can be inductively generated). I will present results aimed at deepening the comprehension of these peculiarities, and at evaluating, in each case, the extent of the divergence. In particular, I will show that no Boolean formal space (=formal space whose associated frame is a Boolean algebra) can be inductively generated. This provides us with a `topologically' relevant example of a non-inductively generated formal space for any given formal space, namely its least dense sub-formal space. It will also be shown how one can use similar arguments for proving, in topoi as in type theory, that Boolean formal spaces cannot be compact or open, and (as already known) cannot have a point. Similar results hold true for De Morgan (i.e. extremally disconnected) locales (with some intriguing nuances, though). It can also be shown that products of non-inductively generated formal spaces can sometimes be constructed (e.g. the self-product of the Dedekind-MacNeille formal topology), thus answering a problem left open in T.Coquand et al., "Inductively generated formal topologies". In the second part of the talk I will briefly survey some results concerning the size of hom-sets in the category of formal spaces.

Fredrik Dahlgren
Effective Distribution Theory via Domain Theory
The theory of distributions is central to the modern theory of ordinary and partial differential equations. Thus, to be able to show that solution operators to certain well-known differential equations are effective, we need an effective theory of distributions. We will use the theory of effective domains and domain representability to introduce a notion of effectivity on test functions, and on distributions. We will show that many of the standard operations on distributions are effective in this setting.

Hannes Diener
Generalising compactness
We will present recent work on extending the notion of compactness into a more general setting than the uniform/metric space one.

Martin Escardó
Closed sublocales in constructive topology.
I'll examine notions of closed subspace in various flavours of constructive topology, and relate it to other topological notions.

Peter Hancock
Representations of continuous functions on final coalgebras
Brouwer's bar theorem contains a representation of continuous functions from Baire space to a discrete space by elements of an inductively defined datatype. This can be generalised to a representation of continuous functions between final coalgebras for a certain class of functors, by means of a datatype in the definition of which least fixed points are nested within greatest fixed points.

Robin Havea
On firmness of the state space and positive elements of a Banach algebra
Following Bridges and Havea, this is an investigation of positive elements in a Banach algebra. Under the firmness of the state space of a Banach algebra, it is shown that even powers of positive Hermitian elements are in fact positive.

Hajime Ishihara
The uniform boundedness theorem and a boundedness principle
In Bishop's constructive mathematics, one can prove the contraposition of the classical uniform boundedness theorem. We show that the original classical uniform boundedness theorem is equivalent to the boundedness principle, called BD-N, which was introduced as an equivalent of a continuity principle: every sequentially continuous mapping from a (complete) separable metric space to a metric space is pointwise continuous, and hence is provable both in intuitionistic mathematics and in constructive recursive mathematics.

Henri Lombardi
What is a real closed field?

Angus Macintyre
Issues of Constructivity in HardCore Number Theory
I will survey the number-theoretic and logical problems concerning the effective content of Finiteness Theorems in arithmetic.

Milly Maietti
Towards a minimal two-level foundation for constructive mathematics (Joint work with Giovanni Sambin)
We propose a proofs-as-programs foundation equipped with a level given by an intensional type theory, and a level given by an extensional theory, that is minimal (at the appropriate level) among relevant existing foundations for constructive mathematics.

Erik Palmgren
Locally compact metric spaces as formal topologies
We show that the category of locally compact metric spaces may be embedded in the category of formal topologies via a full and faithful functor. The proof is constructive in the sense of Bishop's constructive mathematics BISH. This makes it possible to directly use results from BISH in formal topology. A crucial construction is Steve Vickers' notion of a localic completion of a metric space.

Michael Rathjen
On solving A=A->A

Giovanni Sambin
Basic picture as invariance

Helmut Schwichtenberg
A direct proof of the equivalence between Brouwer's fan theorem and König's lemma with a uniqueness hypothesis
From results of Ishihara it is known that the weak (that is, binary) form of König's lemma (WKL) implies Brouwer's fan theorem (Fan). Moreover, Berger and Ishihara [MLQ 2005] have shown that a weakened form WKL! of WKL, where as an additional hypothesis it is required that in an effective sense infinite paths are unique, is equivalent to Fan. The proof that WKL! implies Fan is done explicitely. The other direction (Fan implies WKL!) is far less directly proved; the emphasis is rather to provide a fair number of equivalents to Fan, and to do the proofs economically by giving a circle of implications. Here we give a direct construction. Moreover, we go one step further and formalize the equivalence proof (in the Minlog proof assistant). Since the statements of both Fan and WKL! have computational content, we can automatically extract terms from the two proofs. It turns out that these terms express in a rather perspicuous way the informal constructions.

Dieter Spreen
Effectivity and effective continuity of multifunctions
Multifunctions are used with great success in analysis and logic. In the talk different effectivity notions for such functions are discussed as well as effective version of various continuity notion proposed in the literature. A general result on the effective continuity of effective multifunctions is presented and some important special cases are considered.
The results extend those presented on a similar workshop in Venice some years ago.

Thomas Streicher
Independence Results for BISH

Ruben van den Brink
Characterizing finite subsets of N and compact subsets of N by logical schemes

Wim Veldman
Perhaps: the subtlety of intuitionistic mathematics

Steve Vickers
The Vietoris powerlocale and compact intervals of the localic reals
(This is part of an investigation into localic real analysis with Martin Escardo.) In classical real analysis, some basic results such as the intermediate value theorem can be derived from the fact that closed intervals [a,b] are compact and connected.
The proofs are thoroughly classical, but I shall describe how similar ideas can be used in a constructive localic approach to the reals. The techniques used appear also to be suitable for translation to inductively generated formal topology.
The fundamental tool is the Vietoris powerlocale V(X), whose points are certain sublocales of X. It is analogous to hyperspaces or powerdomains. A clopen sublocale V+(X) comprises the non-empty points of V(X), I shall also describe a sublocale Vc(X), comprising the connected points of V(X).
In the case of the localic real line R, the points of V(R) correspond classically to the compact subspaces of the reals. These can also be described localically as metric completions.
Some classical constructions can now be described localically.
* There are locale maps inf, sup: V+(R) -> R calculating infimum and supremum of points of V+(R).
* Let LEQ be the sublocale of RxR comprising those pairs (x,y) for which x <= y. Then there is a locale map [-,-]: LEQ -> Vc(R) mapping each point (a,b) to the closed interval [a,b]. (Hence [a,b] is compact and connected.)
The intermediate value theorem can now be stated as follows. Let f: R -> R be a locale map, and let a <= b be such that f(a) <= 0 <= f(b). Then inf(V+(|f|)([a,b])) = 0. (|f| is f composed with the absolute value map. Remember also that the powerlocale is functorial, so V+(| f|): V+(R) -> V+(R).)
Similarly, Rolle's theorem. Let f: R -> R have continuous first derivative f'. (This can be expressed localically using Caratheodory's characterization. We have some g: RxR -> R such that
f(y) - f(x) = (y - x) * g(x,y)
and then f'(x) = g(x,x).)
If a < b and f(a) = f(b) then inf(V+(|f'|)([a,b])) = 0.