third CORE meeting

programme

dinner

abstracts

• Hajime Ishihara, Coequalisers in the category of basic pairs
  Ishihara and Kawai constructed coequalisers in the category BP of basic pairs in an extension of the constructive Zermelo-Fraenkel set theory (CZF), founded by Aczel, using the notion of a set-generated class and its characterisation by a generalised geometric theory introduced in Aczel et al. In this talk, we propose a kind of the non-deterministic inductive definition principle (NID) introduced by van den Berg, and show that it is in between NID for elementary rules and that for nullary rules introduced by Ishihara and Nemoto, and that it is equivalent to the existence of coequalisers in BP over a subsystem of CZF.
• Takako Nemoto, Baire category theorem and nowhere differentiable continuous functions
  In constructive mathematics, Baire Category Theorem has at least the following two forms:
  A. Let (U_n) be a sequence of dense open sets in a complete metric space X. Then the intersection U = ∩ _{n ∈ ℕ} U_n is also dense in X.
  B. Let (V_n) be a sequence of nowhere dense closed sets in a complete metric space X. Then the union V = ∪ _{n ∈ ℕ} V_n is also nowhere dense in X.
  In [1], a constructive proof of A is given. In this talk, we will show that there exist nowhere differentiable continuous functions densely in C[0,1], using the above A.
  [1] E. Bishop, Foundations of Constructive Analysis, McGraw-Hill, New York, 1967
• Paulo Oliva, On the computational interpretation of weak König’s lemma
  Weak König’s lemma (WKL) is a widely studied ineffective analytical principle, known in Reverse Mathematics to be equivalent (over RCA) to standard mathematical theorems such as Heine-Borel and Brouwer’s fixed point theorem. In this talk I’ll discuss computational interpretations of this principle, mainly based on Howard’s functional interpretation which uses a weak form of bar recursion [1] and my adaptation of this construction when working with a “feasible” (polynomial-time computable) based theory [2]. I’ll also discuss the recent computable restriction of WKL to convex trees.
  [1] W. A. Howard. Ordinal analysis of simple cases of bar recursion. Journal of Symbolic Logic, 46(1):17-30, 1981.
  [2] P. Oliva. Polynomial-time algorithms from ineffective proofs, Proceedings of LICS, 128-137, 2003.
• Peter Schuster, On an Intermediate Lindenbaum Lemma (joint work with Daniel Wessel)
  Carrying over the Jacobson ideal from commutative rings to logical calculi has brought about a somewhat unusual variant of Lindenbaum's Lemma that relates classical validity and constructive provability. Syntactical interpretations include Glivenko's original theorem and Goedel's extension with double negation shift. This gives the first clue on what the authors and Rinaldi's syntactical conservation criterion (Bull. Symb. Logic 2017 & Indag. Math. 2017) might mean for logic.
• Helmut Schwichtenberg, The fan theorem for uniformly coconvex bars
  Josef Berger and Gregor Svindland gave a constructive proof of the fan theorem for coconvex bars. Motivated by the many applications of the fan theorem and the related weak Lemma of König (WKL), we take a close look at the construction involved in this proof. In fact, we will modify the underlying notions, with the goal to make this construction as clear and efficient as possible. As is to be expected, the data types (i.e., free algebras given by their constructors) used play a crucial role when analyzing the computation. Here we deviate from the standard view of paths in a binary tree as functions from the natural numbers to booleans, which are of type level one. Instead, we view paths as cototal objects in the data type of streams of booleans, and hence as ground type objects (i.e., of type level zero). The natural way to generate such objects is corecursion, which corresponds to usage of some form of choice in the function-based setup.