Trimester Seminar

Friday, August 17th, 11:00

Rigorous Numerical Computing with Ariadne

Pieter Collins (Maastricht)

Abstract

In this talk I will give an overview of Ariadne, a software tool originally developed for verification of hybrid nonlinear dynamic systems. Since this is a challenging problem involving many fundamental problems of continuous mathematics, the computational kernel contains general-purpose numeric, functional, and geometric calculi for working with real numbers, continuous functions, and open and compact subsets of Euclidean space. The semantics of the data types and operations is based on the framework of computable analyis, yielding clean and theoretically-sound interfaces. Concrete implementations use rigorous numerical methods such as interval arithmetic and Taylor function models, and include functionality for linear algebra, automatic differentiation, solution of algebraic and differential equations, and nonlinear constrained optimization. Throughout the talk I will explain the main concepts used in the implementation, and give examples of the use of Ariadne, from simple real-number arithmetic to systems verification.

Wednesday, August 15th, 15:00

Unification of the Lambda-Calcululs and Combinatory Logic

Masahiko Sato (Kyoto University)

Abstract

The lambda-calculus and combinatory logic have been studied as two closely related but distinct systems of logic and computation.  In this talk, however, we will argue that they are in fact one and the same calculus. We substantiate our argument by introducing what we will call the external syntax and the internal syntax for the two calculi. The external syntax will be given as a natural common extension of syntax for the lambda-calculus and combinatory logic. The terms defined by the internal syntax will be characterized as the closed αη normal terms of the external syntax. Thus, the external syntax provides us with human-readable syntax containing all the traditional lambda-terms and combinatory-terms, and the internal syntax is suitable for the infrastructure of a proof assistant. 

This is an ongoing joint work with Takafumi Sakurai and Helmut Schwichtenberg.

Wednesday, August 1st, 15:00

Towards a computational model of HoTT

G. Rosolini (Genova)

Abstract

I shall sketch an "intutitive" model of Homotopy Type Theory based on groupoids of assemblies. It is clearly related to the original groupoid model of Martin-Löf Type Theory introduced by Martin Hofmann and Thomas Streicher. This is joint work in progress with Jacopo Emmeneger.

Wednesday, July 25th, 15:00

The continuity problem - essential proof steps

Dieter Spreen (Siegen)

Abstract

By definition, functions in Markov-style constructive mathematics are extensional computable transformations of constructions of the objects the function is defined. We say in this case that the function is Markov-computable.

The continuity problem is the question whether Markov-computable functions are effectively pointwise continuous. The problem has been studied by many authors, and results of different generality and for different kinds of spaces have been presented. More or less all proofs follow a common pattern which will be exhibited in the talk.

Tuesday, July 24th, 15:00

Intuitionistic Sequential Compactness?

Douglas Bridges (University of Canterbury)

Abstract

After a brief look at Brouwer's intuitionistic substitutes for sequential compactness, I will discuss the relatively recent anti-Specker property, which shows some promise of applicability in intuitionistic analysis. In particular, I will deal with its relation to continuity properties and to a fan theorem.

Wednesday, July 18th, 15:00

Reverse mathematics of Gödel's completeness theorem

Hugo Herbelin (Paris Diderot)

Abstract

We shall survey a couple of results about the reverse mathematics of Gödel's completeness theorem, investigating why it is proved to be equivalent to Excluded Middle (EM) + the Prime Ideal Theorem (PIT) in IZF (Henkin, McCarty, Espindola, ...), claimed to be equivalent to Weak König Lemma in RCA₀ (Simpson), claimed to be equivalent to the Weak Fan Theorem (WFT) in WKV (Loeb-Veldman), claimed to imply Markov's Principle (MP) in intuitionistic logic (Gödel-Kreisel).

To explain the compatibility of these apparently contradictory results, we shall distinguish between the valid-implies-provable and the consistent-implies-model formulations, we shall isolate the impact of the presence of the absurdity connective (MP) or of the disjunction connective (PIT, WFT), we shall analyse the impact of considering non recursively enumerable theories (EM) or of uncountable languages. In particular, we shall introduce a weaker propositional-based variant of the Weak Fan Theorem sufficient to prove completeness in the countable case in the absence of disjunction. We shall also investigate how these results apply to completeness of intuitionistic logic with respect to Kripke or Beth semantics.

Monday, July 16th, 15:00 

Predicative Exponentials: A Topological Approach

Amir Tabatabai (Prague)  

Abstract

The intuitionistic implication and hence the notion of function space in constructive disciplines is both non-geometric and impredicative. In this talk we try to solve both of these problems by first introducing weak exponential objects as a formalization for predicative function spaces and then by proposing modal spaces as a way to introduce a natural family of geometric predicative implications based on the interplay between the concepts of time and space. This combination then leads to a brand new family of modal propositional logics with predicative implications and then to topological semantics for these logics and some weak modal and sub-intuitionistic logics, as well. Finally, if time permits, we will lift these notions and the corresponding relations to a higher and more structured level of modal topoi and modal type theory.

Friday, July 13th, 15:00

Brouwer's continuity principle in constructive reverse mathematics

Hajime Ishihara (JAIST, Ishikawa)

Abstract

We reconsider Ishihara (1991, 1992) within a weak formalised framework of constructive reverse mathematics, focusing on Brouwer's continuity principle for a mapping from Baire space into the natural numbers.

Wednesday, July 11th, 16:45

Two futures: pattern and chaos

Peter Koellner (Harvard University)

Location: Hausdorff Kolloquium, Endenicher Allee 60, Raum 1.016 (Lipschitz-Saal)

Abstract

Set theory is presently at a cross roads, where one is faced with two radically different possible futures.

This is first indicated by Woodin's HOD Dichotomy Theorem, an analogue of Jensen's Covering Lemma with HOD in place of L. The HOD Dichotomy Theorem states that if there is an extendible cardinal, δ, then either HOD is "close'' to V (in the sense that it correctly computes successors of singular cardinals greater than δ) or HOD is "far'' from V (in the sense that all regular cardinals greater than or equal to δ are measurable in HOD). The question is whether the future will lead to the first or the second side of the dichotomy. Is HOD "close'' to V, or "far'' from V?

There are two opposing research programs leading to opposite sides of the dichotomy. The first program is the program of inner model theory. In recent years Woodin has shown that if inner model theory can reach one supercompact cardinal then it "goes all the way", and he has formulated a precise conjecture - the Ultimate-L Conjecture - which, if true, would lead to a fine-structural inner model that can accomodate all of the standard large cardinals. This is the future where pattern prevails.

The second program is the program of large cardinals beyond choice. Kunen famously showed that if AC holds then there cannot be a Reinhardt cardinal. It has remained open whether Reinhardt cardinals are consistent in ZF alone. In recent work - joint with Bagaria and Woodin - the hierarchy of large cardinals beyond choice has been investigated. It turns out that there is an entire hierarchy of choiceless large cardinals of which Reinhardt cardinals are only the beginning, and, surprisingly, this hierarchy appears to be highly ordered and amenable to systematic investigation. Perhaps it is even consistent... The point is that if these choiceless large cardinals are consistent then the Ultimate-L Conjecture must fail. This is the future where there can be no fine-structural understanding of the standard large cardinals. This is the future where chaos prevails. 

Tuesday, July 10^th, 15:00

Program extraction from proofs: the fan theorem for uniformly coconvex bars

Helmut Schwichtenberg (München)

Abstract

Proofs can have computational content, and the most direct method to extract it is via a realizability interpretation in the form given by Kreisel. After a short introduction into the subject we present a recent case study on Brouwer's fan theorem for uniformly coconvex bars.
As an application we prove a constructive version of the Heine-Borel Theorem, for uniformly coconvex coverings.

Friday, June 29th, 10:30 

Gödel's incompleteness theorems in the light of his shorthand notebooks

Jan von Plato (Universität Helsinki)

Location: Oberseminar Mathematische Logik, Endenicher Allee 60, Raum 1.008

Abstract

The Gödel papers in Princeton contain some 250 pages of notes on incompleteness. They stem from the early summer of 1930 to the time of completion of Gödel's great paper later the same year. A study of these notes shows how Gödel's idea of incompleteness, how to prove it, and how to present the result, evolved in this relatively short time.

Wednesday, June 27th, 15:15

Proofs as objects: Hilbert’s pivotal thought

Wilfried Sieg (Carnegie Mellon University)

Location: Hausdorff Kolloquium, Endenicher Allee 60, Raum 1.016 (Lipschitz-Saal)

Abstract

The rigor of mathematics lies in its systematic organization that makes for conclusive proofs of assertions on the basis of assumed principles. Proofs are constructed through thinking, but can also be taken as objects of mathematical investigation; that was the key insight underlying Hilbert’s call for a theory of the “specifically mathematical proof” in 1917. This pivotal thought was rooted in revolutionary developments of mathematics and logic, but it also shaped the new field of mathematical logic. It grounded, in particular, Hilbert’s proof theory. The emerging investigations led over time to computability theory, artificial intelligence and cognitive science. Within this broad framework, I will describe first the pursuit of Hilbert’s proof theory with “reductive” foundational goals and then some recent, tentative steps towards a theory of the “specifically mathematical proof”. Those steps have been made possible by a confluence of proof theoretic investigations in the tradition of Gentzen’s work on natural deduction and computer implementations of mechanisms in which proofs can be (automatically) constructed. Here, at the intersection of automated proof search and interactive verification, is a promising avenue for exploring the structure of mathematical thought.

Wednesday, June 27th, 11:00 

Completeness is overrated

Hannes Diener (University of Canterbury, New Zealand)  

Abstract

It is a common theme in constructive mathematics that adding completeness to the assumptions often allows us to prove otherwise constructively unprovable statements. In this talk we show that we actually only need a very weak version of completeness is enough. We also show that there is an enormous amount of spaces that aren't complete, but satisfy the weakened version of completeness, thus generalising many theorems of constructive analysis including the Kreisel-Lacome-Shoenfield theorem.

Monday, June 25th, 14:00 - 16:00

Two work-in-progress reports:

14:00
Relating the Effective Topos with HoTT

Giuseppe Rosolini (Università di Genova)  

15:00
Zorn's Lemma as a Purely Heuristic Principle

Peter Schuster (Università degli Studi di Verona)  

Friday, June 22nd, 14:30 

Category theory as a programming language

Mohamed Barakat (Universität Siegen)  

Wednesday, June 20th, 16:30 

Making the use of maximal ideals constructive

Ihsen Yengui (Università degli Studi di Verona)   

Abstract

I will explain how to make the use of maximal ideals constructive by treating the two main aspects of utilization of maximal ideals: localizing at a generic maximal ideal or quotienting by a generic maximal ideal. For the first aspect, as guiding example, I will give a dynmical method for computing the syzygy module of polynomials over Dedekind rings using the notion of dynamical Gröbner bases. For the second aspect, as academic example, I will decipher constructively a lemma of Suslin which played a central role in his solution to Serre's conjecture.

Wednesday, June 20th, 15:00 

Bounded Comprehension and Constructive Mathematics

Takaka Nemoto (JAIST, Ishikawa)   

Abstract

(Γ-BCA) is the following axiom:  

∀ m ∃ s ∈ {0,1}* (|s|=m ∧ ∀ i < m (s(i)=0 ↔ A(x))),  for any formula A in Γ  

It has recently turned out that Γ-BCA characterizes many mathematical theorems. For example, Σ⁰₁-BCA is equivalent to each of the following over EL₀:  

 1.Δ(Σ⁰₁)-IND plus Σn-LEM : B(x) ∨ ¬B(x)  for B ∈ Σ⁰₁;   

 2.Σn-IND plus Δ(Σ⁰n)-LEM;   

 3.Σn-LNP:  ∃ x B(x) → ∃ x (B(x) ∧ ∀ y<x ¬B(y)) for B ∈ Σ⁰₁;  

 4. Every bounded monotone sequence of rational numbers is a weak Cauchy sequence;  

 5. Every bounded monotone sequence of real numbers is a weak Cauchy sequence;   

 6. If a set X⊆N has an upperbound, then X is finite, i.e., there are a natural number n and a bijection f : {x:x<n} → X,  

where Δ(Γ) is the smallest class of formulae containing Γ and closed under ∧, ∨, →, ∀ x < t and ∃ x < t, and where a sequence (xn)n is weak Cauchy if ∀ k ∃ N ∀ m,n ≥ N ( |xm - xn| < 2-k ).  

In this talk, I will explain the above equivalences and consider further applications. 

References  

Hajime Ishihara and Takako Nemoto, The monotone completeness theorem in constructive reverse mathematics, submitted.  

Takako Nemoto, Finite sets and infinite sets in weak intuitionistic arithmetic, submitted.  

Friday, June 15th, 16:45 (coffee and cake will be served at 16:15)

Colloquium in commemoration of Felix Hausdorff

An Overview of Homotopy Type Theory

Steve Awodey (Carnegie Mellon University), Introduction by Peter Koepke

Location: Endenicher Allee 60, Raum 1.016 (Lipschitz-Saal)

More information

Wednesday, June 13th, 16:30 

On a hybrid concept of entailment relation

Daniel Wessel (Università degli Studi di Verona) 

Abstract

Some potential applications of Scott's entailment relations in abstract algebra seem to call for an extension that allows for arbitrary sets of succedents (rather than the usual finite ones). We discuss a possible development, hint at some issues that over constructive set theory would need attending to, address (the lack of) completeness, and go through a couple of examples to illustrate why this might be a road worth taking.

Wednesday, May 30th, 16:30 

Modeling Techniques for Constructivism, and an Application to the Fan Theorem

Bob Lubarsky (Florida Atlantic University) 

Abstract

For building models of constructive mathematics, the known techniques are realizability, Kripke, and Heyting-valued models. This talk will present a construction that combines all of those three. This will then be used to prove a separation between two fragments of the Fan Theorem.

Wednesday, May 23rd, 16:30 

The BHK interpretation: looking through Gödel's classical lens

Amir Tabatabai (Czech Academy of Sciences) 

Abstract

In 1933, Gödel introduced a provability interpretation of propositional intuitionistic logic to establish a formalization for the BHK interpretation, reading constructions as the usual classical proofs. But instead of using any concrete proof he used the modal system, S4, as a formalization of the intuitive concept of provability and then translated IPC into S4 in a sound and complete manner. His work suggested the problem to find the missing concrete provability interpretation of the modal logic S4 to complete the formalization of the BHK interpretation.

In this talk, we will try to solve this problem. We will generalize Solovay's provability interpretation of the modal logic GL to capture other modal logics such as K4, KD4 and S4. Then we will use these results to find a formalization for the BHK interpretation and we will show that the BHK interpretation is nothing but a plural name for different interpretations of different propositional logics such as Intuitionistic logic, minimal logic and Visser-Ruitenburg's basic logic. Moreover, we will show that there is no provability interpretation for any extension of KD45 and also there is no BHK interpretation for the classical propositional logic.

Tuesday, May 15^th

Welcome Meeting