Incompleteness and completeness

Formalizing Logic and Analysis in Type Theory

Workshop for the PhD-defense of Russell O'Connor (October 5th, 13:30 in the Aula).

6 October 2009

Nijmegen, the Netherlands

The workshop will be held at the campus of the Radboud University Nijmegen


Slides are now available below.


The workshop will be held on 6th of October.

Tuesday, October 6th

12:00-13:00 Lunch De Refter
13:00-14:00 Helmut Schwichtenberg) Simultaneous inductive/coinductive definition of continuous functions
14:00-15:00 Norbert Mueller) Enhancing imperative exact real arithmetic with functions and logic
15:00-15:30 Coffee
15:30-16:30 Russell O'Connor How to Understand What Classical Mathematicians Say
16:30-17:30 John Harrison) Decidability and undecidability in theories of real vector spaces
17:30-18:30 Drinks
19:00 Dinner Vurrukkuluk
The location of the dinner:


Russell O'Connor McMaster University

How to Understand What Classical Mathematicians Say

Usually people consider constructive mathematics as a restriction of classical mathematics where the law of the excluded middle is disallowed. However, I believe that constructive mathematics is better as an extension of classical mathematics which adds constructive existential quantifier and a constructive function space.
In my talk will cover

Norbert Muller Universitaet Trier

Enhancing imperative exact real arithmetic with functions and logic

In the near past, there have been many approaches to `implement' constructive analysis, many of them with the use of functional programmig languages. In this paper we present a similar approach based on the iRRAM-package which has been acknowledged as a fast package for exact real arithmetic in C++. A major concern here is the reduction of space requirements for computations with real numbers.

Helmut Schwichtenberg Universitaet Muenchen

Simultaneous inductive/coinductive definition of continuous functions

When extracting computational content from proofs in constructive analysis it can be helpful to use simultaneous inductive/coinductive definitons of the real numbers and of (uniformly) continuous real functions. The talk reports on an attempt to design the underlying theory, based on recent work of Ulrich Berger.

John Harrison Intel Corporation

Decidability and undecidability in theories of real vector spaces

The known decidability of various elementary theories of real numbers leads to practical decision procedures that are genuinely useful in formal proofs. Linear real arithmetic is a staple of verification systems, and recently there has been increasing interest in the automation of nonlinear arithmetic via various techniques (quantifier elimination, sum-of-squares decomposition or more heuristic means).
For many purposes, particularly in geometry, it's natural to wonder whether these results can be extended to analogous theories of real vector spaces, formulated in a 2-sorted first-order language with a sort for vectors and another for real numbers. In joint work, Solovay, Arthan and the speaker have systematically surveyed various theories of this kind. It turns out that the theories of vector spaces and inner product spaces are decidable and even admit quantifier elimination in a suitably expanded language, whereas similar-looking theories of normed spaces are spectacularly undecidable, at least as difficult as second-order arithmetic. The universal "linear" theory of normed spaces, however, is fairly efficiently decidable, and a decision procedure for this theory has been found to be very useful.


Herman Geuvers Nicole Messink Bas Spitters.
Please contact Nicole Messink for practical matters.

Getting to Nijmegen

Most of you will be arriving at Amsterdam Schiphol airport. The easiest way to get to Nijmegen from there is by train. The train station is under the airport. Just check the screens.

The train trip is 1 hour and 30 - 45 minutes.

There is a train planner on the web.


We have good experiences with:

Hotel Apollo

Bisschop Hamerstraat 14

6511 NB Nijmegen

Tel.: +31 (0)24 - 323 35 94

Fax: +31 (0)24 - 323 31 76

Slightly more expensive is:

Hotel Courage

Waalkade 108-112

6511 XR Nijmegen

Tel.: +31 (0)24 - 360 49 70

Fax: +31 (0)24 - 360 71 77

There also is a web page with alternative accomodation.

Getting to the Workshop

The workshop will be held at

It is located at lecture room GN2.

In case you enjoy walking the campus is 30 minutes walk from the city center.

There is a bus going to the campus. The buses that run through the Heyendaalseweg are lines 1 (direction Molenhoek) and 11 (direction Brakkenstein), 10 (Heyendael Shuttle), 3,4 (Wijchen via Noord/Zuid) all stop outside the "Bloedbank" opposite our building.

page maintained by Bas