Latest results in applications of proof-theoretic techniques to problems in mathematics
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:
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.
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$.
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.