9:44 | opening | |
---|---|---|

9:45-10:30 | Klaus Mainzer | Constructive Operations Research. Bridging Logic, Mathematics, Computer Science and Philosophy. |

10:45-11:30 | Vasco Brattka | The computational content of the Hahn-Banach Theorem: some known results, some open questions |

11:45-12:30 | Hajime Ishihara | Coequalisers in the category of basic pairs |

14:00-14:45 | Takako Nemoto | Baire category theorem and nowhere differentiable continuous functions |

15:00-15:45 | Paulo Oliva | On the computational interpretation of weak König’s lemma |

16:15-17:00 | Peter M. Schuster | Extension by Conservation |

17:15-18:00 | Helmut Schwichtenberg | title |

- 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.

jb 11
january 2018