Home Programme Directions Materials Photos

Peter Aczel  Constructive Set Theory  (-> abstract) Ryota Akiyoshi  On a relationship between cut-elimination proofs by W. Tait and W. Buchholz W. Tait proposed a new ordinal-free cut-elimination proof for Π-1-1 analysis by analysing a proof by G. Takeuti. Our aim is to explain new constructions in Tait's cut-elimination proof in terms of Buchholz' Omega-rule. This is joint work in progress with G. Mints. Toshiyasu Arai  Proofs and sets In this talk I will discuss proof-theoretic investigations on fragments of set theories, and interplay of set theory and proof theory. Douglas Bridges  Constructive Analysis  (-> abstract)  (-> presentation) Ruben van den Brink  Intuitionistic Independencies  (-> presentation) Classical metamathematical methods are often used to shed light on intuitionistic theories. The models that show independencies are significant only in as far as they can be constructively understood. We take Scott's paper on the topological interpretation as a starting point in the quest for new, truly intuitionistic models. Robin Havea  On the convexity of the numerical range It is claimed that every known (classical) proof of the Toeplitz-Hausdorff theorem is 'computational'. A proof by Halmos is thoroughly investigated showing where nonconstructive principles are used and how these can be repaired so that the proof is constructive. Limiting examples are presented showing that our proof is the best we can hope for in a constructive setting. Susumu Hayashi  Hilbert and Constructivity Hilbert's 1890 paper on algabraic forms is one of the earliest works of non-constructive algebra of 20th century modern algebra. We will elucidate in what extent it is constructive. Robert Lubarsky  Closed Sets of Reals with Few Points, and an Application to Riesz Spaces Coquand-Spitters proved a constructive version of the Stone-Yosida Representation Theorem, by which any separable Riesz space is embeddable in a space of continuous functions (cf. the Stone Representation Theorem for Boolean algebras). They asked whether their use of Dependent Choice was necessary. We re-cast this question in terms of paths through collections of (pseudo-)trees, using those objects formulate a choice principle equivalent with the existence of such representations, and then show it is consistent with constructive set theory for that choice principle to fail. The latter is achieved via a topological model. This is joint work with Fred Richman. Takako Nemoto  Weak weak Koenig's lemma in constructive reverse mathematics In classical reverse mathematics, weak weak Koenig's lemma is equivalent to the countable additivity of Lebesgue measure. Acutually, weak weak Koenig's lemma is weakend Brouwer's fan theorem. In this talk, we consider weaker version of the equivalence between Brouwer's fan theorem and positivity of infimum of positive uniformly continuous function defind on closed interval [0,1]. Kengo Okamoto  Frege, Brower and Wittgenstein on the Notion of Sequence It is widely held that logicists' conception of the "universe" of logic and mathematics (the domain of objects and functions in general, the collection of natural numbers and that of number theoretic functions in particular) was in square opposition to Brouwer's (i.e. his notions of spreads and of choice sequences). On the contrary, I would like to point out the following: 1) Frege's use of second-order quantification (especially as expounded in his early writings) in characterizing the natural number sequence and other inductively generated sequences naturally suggests that his intended domain of "properties" is something very close to the collection of open sets on a "tree" (i.e. spread) of choice sequences. 2) Later Wittgenstein's seemingly eccentric observations on the process of generation of natural number sequences, which originate from his critical re-examinations of Frege's accomplishments, are not only strongly influenced by Brower but also can be construed as an attempt to establish the conceptual legitimacy and indispensability of free choice. Erik Palmgren  Ramified Type Theory and Constructive Mathematics  (-> abstract)   (-> presentation) Dirk Pattinson  The computational use of non-smooth derivatives  (-> presentation) Second order methods for solving ordinary differential equations (ODEs) standardly require the differentiability of the vector field that defines the equation. Here, we show that replacing the classical derivative with the domain theoretic derivative allows us to use a second order method even if the vector field defining the equation is Lipschitz but not differentiable. Working in a domain-theoretic framework, this leads to a new algorithm for solving ODEs with guaranteed error bounds that is applicable to problems that lie outside the domain of other verified ODE solvers. In addition to the mathematical theory, we report on our experiences with an implementation of this new method and demonstrate its superiority by means of experimental data. Michael Rathjen  Lifschitz's realizability for set theories Lifschitz defined in 1979 a variant of realizability for HA which validates Church's thesis with uniqueness condition but refutes the general form of Church's thesis. This type of realizability was extended to second order Heyting arithmetic by van Oosten. The talk will be concerned with extending Lifschitz's realizability to full intuitionistic set theory IZF and to semi-intuitionistic set theories. One interesting aspect of this realizability notion is that the axiom of countable choice is invalidated but still the Cauchy reals and the Dedekind reals are isomorphic in the so-called Lifschitz topos (due to van Oosten). This is joint work with Ray-Ming Chen. Giovanni Sambin  The Basic Picture: recent developments (-> presentation) Formal topology was introduced over 20 years ago as an intuitionistic and predicative approach to pointfree topology. The basic picture extends formal topology in various directions, mainly by including pointwise topology, non-distributive lattices, and continuous relations. This has brought to several new structures and insights, which are new also classically. Topology can be seen as the result of the dynamics between a set of points X and a set of observables S, linked by an arbitrary relation (a basic pair). One can thus observe a duality between open and closed, and a symmetry between points and observables. Open and closed subsets are those which can be "translated" faithfully from X to S through existential or universal images. This brings in particular to a pointfree notion of closed subset. Similarly, a relation r between two sets of points X and Y is continuous precisely when it can be "translated" faithfully into a relation s between the corresponding sets of observables S and T. Or equivalently, when r and s form a commutative square diagram. Considering continuous relations rather than functions as morphisms has two outcomes. The logical structure of all topological notions remains clear (which is not possible with functions). One can give mathematical evidence to the claim that the pointfree approach is more general than traditional pointwise topology: the category BP of basic pairs is embedded in the category BTop of basic topologies. Proper (distributive) topology is obtained in a modular way, by considering the sub-categories in which convergence is preserved. The category of concrete spaces (=convergent basic pairs) with relations behaves better than the usual category Top, which is contained in it. In fact, the well-known adjunction between Top and Loc (category of locales), now becomes an ambedding of CSpa into the category FTop of formal topologies (=convergent basic topologies), which contains Loc. The constructive treatment of these results means in particular that one can further generalise them and put them in algebraic form. Masahiko Sato  Platonism with a flavor of constructivism  (-> presentation) Although platonists and constructivists view general mathematical objects in drastically different ways, it seems that linguistic objects are viewed rather similarly by both of them. With this in mind, we discuss the possibility of a construction of platonic mathematical objects. Since，for platonists, mathematical objects exist independent of our mind, the construction here is an idealistic reconstruction of mathematical objects for platonists. In this setting, we will show how mathematical objects like odinals and sets can be contructed by transfinitary inductive definition. Peter Schuster  Spectral Schemes as Ringed Lattices  (-> abstract) Helmut Schwichtenberg  Computational content of proofs We consider logical propositions concerning data structures. If such a proposition involves (constructive) existential quantifiers in strictly positive positions, then -- according to Brouwer, Heyting and Kolmogorov -- it can be seen as a computational problem. A (constructive) proof of the proposition then provides a solution to this problem, and one can machine extract (via a realizability interpretation) this solution in the form of a lambda calculus term involving recursion operators, which can be seen as (and translated into) a functional program. We concentrate on the question how to control at the proof level the complexity of the extracted programs. Dieter Spreen  Solving Domain Equations in the Category of Effectively Given Topological Spaces Solving domain equations is an important tool for constructing models for programming languages and higher-order logics. The construction of a solution usually requires the existence of colimits of Ω-chains where the connecting morphisms are embeddings. In this talk we present a notion of embedding so that the category of effectively given spaces has colimits of Ω-chains. Izumi Takeuti  Function-restricted Constructive Mathematics and Complexity-bounded Computable Analysis In constructive mathematics, we are intersted in the point how many functions a mathematical proof needs. Complexity-bounded computable analysis gives the model of function-restricted constructive mathematics. Thus, we can obtain results on the strength of function construction by studying complexity-bounded computable analysis. Makoto Tatsuta  Some Non-Recursively-Enumerable Sets and Their Types Klop's Problem and TLCA open problem 20 were solved recently by using the same techniques, coding primitive recursive functions by infinite objects and a countably infinite set of types. This talk discusses these techniques and gives future directions. Klop's Problem was finding a type for characterizing hereditary head normalizing terms, that is, lambda-terms whose Bohm trees do not contain the bottom. In the FLOPS2008 conference paper, Tatsuta proved that this problem does not have any solution by showing that the set of those terms is not recursively enumerable. The paper also gave a best-possible solution by providing an intersection type system with a countably infinite set of types such that typing in all these types characterizes hereditary head normalizing terms. TLCA open problem 20 was a problem of finding a type system that characterizes hereditary permutators. In the LICS2008 conference paper, Tatsuta showed that there does not exist such a type system by showing that the set of hereditary permutators is not recursively enumerable. Secondly this paper gave a best-possible solution by providing a countably infinite set of types such that a term has every type in the set if and only if the term is a hereditary permutator. This talk explains these techniques can be used to investigate types for streams, coinductively defined data, and infinite lambda-calculus. Mariko Yasugi  Effective uniformity and limiting recursion in computable analysis I will discuss the roles of "effective uniformity" and "limiting recursion" in computability problems in analysis. Under a certain prevailing condition, they yield the same results such as sequential computability of a Euclidean discontinuous function. I will also introduce some joint works regarding Fine computable functions. Keita Yokoyama  Integration and differentiation in second order arithmetic Within the system of recursive comprehension (RCA_0), we can deal with the real (or complex) number system and continuous functions on it. S. Simpson showed that weak Knig's lemma is sufficient and necessary to integrate continuous functions on the closed unit interaval. For differentiation, the situation is a litter more complex. In this talk, I will introduce some conditions for differentiation and integration and do reverse mathematics for differential and integral calculus. Satoru Yoshida  Sequential continuity and boundedness of generalized functions in constructive mathematics Sequential continuity and boundedness (i.e. uniform continuity) of generalized functions are equivalent in classical generalized function theory. In my talk, it is present that the sequential continuity implies the boundedness if and only if the principle BD-N holds, in Bishop's constructive mathematic, where BD-N is provable in classical mathematics, Brouwer's intuitionistic mathematics and constructive recursive mathematics of Markov's school but not in Bishop's framework. That is, the deference in some continuity properties can be clear in Bishop's one. To this end, we will investigate the representation theorem of generalized functions whose support consists of the origin.