Workshop on Proof Theory and Algorithms, Edinburgh March 23-28, 2003

Latest results in applications of proof-theoretic techniques to problems in mathematics

Basic Concepts in Quantum Computations

Quantum computer may be the next revolution in the computer industry. Simplest quantum computers have already been constructed, but there is little evidence so far that quantum model of computation improves our chances to solve hard computational problems. The purpose of this talk is to give a review of basic concepts, definitions, and notations in Quantum Computing. The following topics are going to be discussed:

- Quibits, Gates, Measurements, Notations.
- Quantum Model of Calculations, Complexity.
- Quantum Parallelism, Entanglement, Coding, Teleportation.
- Examples: Grover^Rs Quantum Search algorithm, Deutsch-Jozsa algorithm, Quantum Fourier Transform, Shor^Rs Factoring algorithm.
- Class BQNP and complete problems, Quantum K-CNF problem.

RATIONAL DYNAMICS: game-theoretic equilibria as logical fixed-points of repeated announcements

Many of the current contacts between logic and game theory have to do with explaining the emergence and stability of game-theoretic equilibria in terms of epistemic assumptions. In this talk, we analyze game-theoretic equilibria as arising in the limit from repeated announcements by players of their own rationality. This idea is made precise in a dynamic logic of information update. More technically, this analysis leads to connections between different notions of game equilibrium and different fixed-point logics: monotonic or inflationary.

On the intuitionistic strength of monotone inductive definitions

In his 2002 Ph.D. thesis M. Moellerfeld has shown that the second-order $\mu$-calculus, a theory axiomatizing least fixed points of positively defined monotone operators, when based on classical logic, has the strength of $\Pi^1_2$ comprehension axiom, which is the current limit of ordinal analysis. His methods are based on Generalized Recursion Theory, and as such are not amenable to intuitionistic reasoning. However, the $\mu$-calculus presented very little problems for the Goedel-Gentzen-Kolmogorov double-negation translation, so we prove that the intuitionistic theory is proof-theoretically equally strong.

Further interpretation of the intuitionistic $\mu$-calculus in the system $T_0^i+UMID$ of Explicit Mathematics provides a first breakthrough into intuitionistic strength of monotone inductive definitions in those theories, showing that one should expect that this strength is as big as the classical one. This question was posed by S. Feferman in 1982, but up to now virtually nothing was known in this area. On the classical side, it came as a surprise when M. Rathjen proved in a series of papers of 1996--2002 that the strength is essentially that of $\Pi^1_2$-CA. Our work determines the exact strength of the intuitionistic $T_0^i(restr.)+UMID_N$.

The equational theory of fixed points

We argue that all cartesian fixed point models in computer science, including ordered, metric and categorical models, share the same equational properties. The models satisfying these equational properties are called iteration categories. We provide an axiomatic treatment and discuss decidability and complexity issues. We also provide several applications to concurrency and language theory.

Last modified: Mon Jun 23 14:18:33 PDT 2003