Proof and Computation

Ludwig-Maximilians-Universität München 

5-6 November 1999

 

Abstracts

Peter Aczel (Manchester)
Forms of Full Impredicativity

As a working definition I call a theory fully impredicative if it is at least as strong, in the proof theoretic sense, as full higher order arithmetic (or possibly just full second order arithmetic). In the foundational context of constructive type theory/constructive set theory (CTT/CST) I will consider and compare some possible principles that `justify' full impredicativity; i.e. when a theory expressing CTT/CST is extended using such principles the theory becomes fully impredicative. One such principle is expressed by the rules for the impredicative type Prop in the calculus of constructions. This principle justifies full impredicativity and gives rise to theories stronger than various extensions of Zermelo set theory. Can it be used to justify ZF set theory?

Andrea Cantini (Firenze)
Untyped operations, reflection and weak induction

We consider applicative theories based on (untyped) combinatory logic, which comprise at least the type W of binary strings.
We study a reflection principle for W, which naturally enriches the structure of W-sets and implies a form of Weak König lemma for W-sets, together with suitable forms of bounded and safe induction.
We then prove bounding theorems for the class of the provably total operations (of binary strings).

Solomon Feferman (Stanford)
Kurt Schütte's way

Kurt Schütte's way was distinctive in its aims, its methodology, its style, and the success with which it was transmitted to students and researchers at large. As much as anyone, he was responsible for the remarkable transformation of proof theory in the latter half of the 20th century. I will begin with some personal reminiscences, and then examine various aspects of Schütte's legacy, leading up to the question: Where does it leave us now, and how shall we proceed from here?

Gerhard Jäger (Bern)
Metapredicativity

In this talk I will give a survey of some recent developments concerning metapredicative subsystems of set theory, second order arithmetic and explicit mathematics. I will concentrate on conceptual aspects rather than technical details.

Ulrich Kohlenbach (Aarhus)
Reverse mathematics and higher types

The program of so-called reverse mathematics as developed by H. Friedman, S. Simpson and others is traditionally carried out in the framework of second order arithmetic (whereas the original setting due to H. Friedman used function variables, subsequent work has been based on set variables instead). The restriction to a second order language has, however, the following disadvantages:
  1. it requires complicated encoding of higher mathematical objects;
  2. this encoding sometimes tacitly yields a constructive enrichment of the usual mathematical notions, in particular the encoding of continuous functions is not faithful for systems weaker than ACA_0;
  3. an explicit treatment of non-continuous functions is not possible.
We propose a finite type extension RCA^\omega_0 of (a version with function variables instead of set variables of) RCA_0 which is conservative over (this version of) RCA_0. Therefore, nothing is lost by working over RCA^\omega_0 instead of RCA_0 as base system. But 1)-3) can be addressed successfully in this setting. In particular, we will discuss 3), showing that uniform versions of many analytical principles are -- relative to RCA^\omega_0 -- equivalent to the existence of S. Feferman's non-constructive \mu-operator. This is due to a phenomenon known as `Grilliot's trick'.

Per Martin-Löf (Stockholm)
(Nonstandard Type Theory)

It will be shown how to formalize the nonstandard extension of type theory first considered in my paper Mathematics of Infinity, Springer Lecture Notes in Computer Science, Vol. 417, pp. 146-197.

Dag Normann (Oslo)
Is it fair to call any total object total?

A function is traditionally called total if it is defined on all (relevant) arguments. We will discuss how examples of domains with totality fits in with this original view. We aim to describe the category of evaluation structures; rich enough to capture the domains with totality used as interpretations of transfinite types, and narrow enough to support general proofs of important structural properties of these domains with totality.

Wolfram Pohlers (Münster)
Search Trees, a Byproduct of Schütte's Positive and Negative Parts

One of Schüttes preferred notions was that of a positive and a negative part of a formula. He invented this notion together with an adjusted notion of formal proof in order to combine the advantages of Gentzen's sequent calculus with the benefits of Hilbert's more mathematical oriented proof calculus. To test the efficiency of his notions he reproved the completeness theorem for first order predicate logic for his calculus. In this proof he developed a novel method of search trees. Today the notion of positive and negative parts are out of fashion. Search trees, however, have become a powerful tool in different parts of Mathematical Logic. We will give some examples for results which can be obtained by the method of search trees.

Michael Rathjen (Leeds)
Schütte's work on ordinal analysis in the '80s and '90s

There is an astounding body of research that Schütte carried out after he became Professor Emeritus. The talk will focus on his work on ordinal analysis in the '80s and '90s.

Anton Setzer (Uppsala)
Towards a type theory for stability

We introduce an extension of Martin-Löf type theory, which we conjecture to have the strength of Kripke-Platek set theory plus the existence of an ordinal \kappa which is \kappa+\alpha-stable for every \alpha < \kappa. Further extensions will be discussed.

Robert Stärk (Zürich)
Java bytecode verification without subroutine call stacks

Java bytecode is mechanically verified by a "bytecode verifier" before it is executed on the Java virtual machine (JVM). The reason is, that bytecode which is accepted by the verifier does not violate certain security constraints during execution on the virtual machine and therefore expensive run-time tests can be omitted. Nested try-catch-finally statements, however, complicate the verification process, since the so-called subroutines which implement them, have to be polymorphic in variables which they do not modify. Several type systems have already been presented to solve the problem. Most of them use a notion like subroutine call stack or subroutine history, and try to partition the bytecode into different subroutines. Our bytecode verifier does not use such notions. Instead, a new notion for the typing of return addresses is used in the soundness proof. [Joint work with E. Börger, J. Schmid and W. Schulte.]

Thomas Strahm (Bern)
Theories with self-application and computational complexity

Theories with self-application form the operational core of Feferman's systems of explicit mathematics. In this talk we discuss (unramified) bounded applicative systems which have a strong relationship to classes of computational complexity. We provide new applicative theories whose provably total functions coincide with the functions computable in polynomial time, polynomial space, polynomial time and linear space, as well as linear space.

Stan Wainer (Leeds)
Proof Theory and Complexity

This talk will describe some joint work with my students G. Ostrin and N. Cagman, on the proof theory of low subrecursive classes, between Grzegorczyk's E2 and E3. The basis is "A new recursion- theoretic characterization of the polytime functions" by Bellantoni and Cook (1992), in which it is shown that a natural two-sorted re- interpretation of the primitive recursion schemes characterizes polynomially bounded computation. We show that if Peano Arithmetic is instead formulated in this two-sorted fashion, with quantification allowed only over one sort ("safe" variables) and induction allowed only over the other ("normal" variables), then the provably recursive functions are exactly the E3 (elementary) functions. The provably recursive functions of the n-quantifier inductive fragments of this theory turn out to be closely related to the levels of Ritchie's hierarchy of "Predictably computable functions" (1963), with \Sigma_1 induction corresponding to the E2 (linear space) functions. This work is (clearly) related to other results of Buss, Bellantoni, Leivant, Beckmann and Weiermann, and others too. In addition it illustrates nicely the use of classical ordinal analysis techniques even at this low level. The difference with classical PA is that the separation of induction from quantification means that the bounding functions are now Slow Growing rather than Fast Growing. Below epsilon-0 the Slow Growing functions only give elementary bounds - hence the results.

Andreas Weiermann (Münster)
Variations on the slow growing hierarchy

We investigate the growth rate behaviour of the slow growing hierarchy with respect to its underlying system of fundamental sequences.

Back to home-page Proof and Computation, Schütte-Kolloquium