###
15th meeting on Synbolic Logic And Computger Sciences

(SLACS'98)

14 -- 16 Oct. 1998

Kawai Hall, Math. Inst., Tohoku Univ.,

Sendai, JAPAN
[Programme]
[Abstracts of contributed talks]

Invited Talks

Stanley S. Wainer (University of Leeds, UK)

Tilte: Proof Theory and Complexity

This talk will describe some joint work with my student

G. Ostrin, on the proof theory of low subrecursive classes.

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 normal 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 (the "safe"

variables) and induction allowed only over the other ("normal"

variables), then the provably computable functions are exactly

the Kalmar elementary functions E(3). The provably computable

functions of the Sigma_n Inductive fragments of the 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 linear space functions

E(2). This work is related to other results of Buss, Bellantoni,

Beckmann and Leivant, but in addition it clearly illustrates

the use of classical ordinal analysis techniques at this low level.

The difference with classical Peano Arithmetic is that it is now

the Slow Growing Hierarchy which supplies the bounding functions,

rather than the Fast Growing Hierarchy which arises in the classical

case.

Andreas Weiermann (Westfaelische Wilhelms-Universitaet Muenster, Deutschland)

Title: Sharp bounds for the lengths of reduction sequences in Goedel's T

Abstract: Using ideas from infinitary proof theory and based on Howard's

weak normalization proof for Goedel's system T we define

a numbertheoretic function f such that for two given terms

a and b of T the following holds:

If a rewrites to b then f(a) is strictly larger than f(b).

f ensures termination of T and, in addition,

it yields optimal upper bounds for the lengths of

reductions in Goedel's T.

Jananese Page

Organiser:
slacs-kanji@sato.kuis.kyoto-u.ac.jp