Seminar: Logic and Theoretical Computer Science

Three applicative theories of words which correspond to three weak complexity classes will be presented. They prove totality exactly for the functions in the logarithmical hierarchy, alternating logarithmical time and polynomial time respectively.
The systems differ in their induction rules which justify different forms of concatenation recursion resulting in different proof-theoretical strengths.
I hope that the talk can convince you that the applicative setting is able to account for weak complexity classes in a more transparent and elegant way than bounded arithmetic.

Sharkovski's theorem states that whenever there is a pair (n,m) in SR (Sharkovski-Relation) and a (uniform) continuous function f:R->R has a periodic point of primitive period n, then f has also a periodic point of primitive order m. In this talk it is shown that within Bishop style analysis the uniform continuous case of this theorem is equivalent with the lesser limited principle of omniscience (LLPO).

The proof-theoretic analysis of a formal theory involves meta-mathematical arguments and concepts that have to be justified, especially if infinitary methods occur. Usually, this justification means a reduction to a weak base theory like that of primitive recursive arithmetic (PRA) that involves encodings and reasoning on such encodings. (Moreover, augmented by the scheme of transfinite induction up to certain ordinals that can be represented in this base theory.)
Such a reduction is also relevant if the provability or unprovability of certain true sentences is to be retrieved directly from the proof-theoretic analysis (e.g., the provably recursive functions of number theory). In this basic and introductory talk, I show you a method of W. Buchholz how this reduction can be achieved without too much dependency on encodings. Namely within the framework of finitary proof theory and for the well-known proof-theoretic analysis of number theory as an example.

We present a term calculus with explicit contraction and weakening, which is typed by deep-inference derivations. Using a version of the medial rule of deep-inference we give a set of reduction rules that are atomic, in the sense that they never copy or erase unbounded subterms. Finally, we give an interpretation of our calculus in terms of the lambda calculus and show how our reduction can simulate beta reduction.