Incompleteness and completeness

Formalizing Logic and Analysis in Type Theory

6 October 2009

Nijmegen, the Netherlands

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

Update

Program

The workshop will be held on 6th of October.

Tuesday, October 6th

Abstracts

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

• How to interpret classical mathematics in a fragment of constructive mathematics.
• How this classical fragment is useful when developing constructive analysis.
• Why classical mathematicians want to increase their expressiveness by adding the constructive existential quantifier to their language.
• Why constructive mathematics is helpful language for computer scientists who want to prove programs correct.

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.

Organisers

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.

Hotels

We have good experiences with:

Slightly more expensive is:

There also is a web page with alternative accomodation.

Getting to the Workshop

The workshop will be held at
Gymnasion.

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