The Numerical Omniscience Scheme (NOS) is (n)[A(n)v-A(n)]->(n)A(n)v(En)-A(n), where A(n,...) is any formula in a given language. The scheme is of interest in systems based on intuitionistic logic. Bishop pointed out that all the theorems of classical analysis for which he found constructive substitutes follow from his constructive versions using the special case of this, (n)f(n)=0 v (En)-f(n)=0, called the Limited Principle of Omniscience (LPO).
The proof-theoretic strength of various systems with LPO and NOS have been studied in my article for the Handbook of Math. Logic and Friedman's article for the Kleene Symposium. A new system of interest using NOS has recently been introduced in the article by Coquand and Palmgren in Arch. Math. Logic 39 (2000) 53-74. It is an extension of Heyting Arithmetic in all finite types, HA^omega, by various schemes of choice, axioms for the set O of countable constructive tree ordinals, and NOS. They give a sheaf model of it in constructive type theory, but do not measure its proof-theoretic strength. Their system is closely related to the system T_Omega + (mu) of sec. 9 of the article by Avigad and myself on Goedel's functional("Dialectica") interpretation in the Handbook of Proof Theory. Using the methods explained there, I show that the strength of the Coquand-Palmgren system is the same as that of ID_1, even when one takes full scheme of choice in all types. It follows from this work that the Dialectica interpretation of NOS follows from that of LPO, so no strength is added thereby.
Reasoning and other logical tasks have a game-like character, as shows in the fact that people can 'win' or 'lose' debates. Conversely, general games (economic, recreational) have an interesting logical structure. We present a general view of interfaces between logic and game theory that are emerging these days. (Three workshops just this year.) The emphasis will be, not on 'application' either way, but on new types of result, i.e., possible joint offspring of this alliance.
Topics:
References:
Part I was on Tuesday April 11 under the title *Logic Games*.
We have looked at
Tuesday April 18 *Game Logics*
Topics will be:
References:
Tuesday April 25 *Logical Analysis of Games*
We look at imperfect information games (Hintikka, Osborne & Rubinstein), where players forget or cannot observe completely, and describe basic issues that arise when modeling them:
Reference:
Finally, many important aspects of game structure have not (yet) come to in our bottom-up approach: e.g., preferences, equilibrium, coalitions. Check the material on the web-page http:www.cwi.nl/~pauly/games.html
The first abstract definition of a Hilbert space was given by John von Neumann in a 1927 paper on the mathematical foundations of quantum mechanics. This was the beginning of ten years in which von Neumann was one of the most influential mathematicians in the world, and in which essentially all of his work was connected with quantum mechanics. In particular, considerations of measurements led him to prove the spectral theorem for unbounded operators in 1929, and some thermodynamic considerations eventually led him to his mean ergodic theorem of 1931. In this talk I follow these two developments through 1932, the year of both von Neumann's famous book on the Mathematical Foundations of Quantum Mechanics and his priority dispute with Birkhoff about the founding of ergodic theory. I also use the history to comment critically on two theses in the philosophy of math: the "indispensability" and "unreasonable effectiveness" of mathematics in natural science.
Given a self-adjoint operator T, can we compute its spectral family? Given a contraction T, can we compute the limit of the averages of its iterates? These questions are typical of constructive analysis in the style of Errett Bishop; in this talk I will survey the answers that have been given in two recent dissertations. Feng Ye (PhD Princeton 1999) has given constructive proofs of the spectral theorem, Stone's theorem, and the Kato-Rellich theorem; one of his key tools is an interesting reformulation of self-adjointness (Ran(T+iI) = Ran(T-iI) = H). Bas Spitters (PhD Nijmegen 2000) has given constructive proofs of von Neumann's mean, Birkhoff's pointwise, and Dunford-Schwartz's L^1-L^infinity ergodic theorems; all are shown equivalent to a procedure for computing distances to the eigenvalue-1 subspace of T. I consider these some of the nicest results in constructive analysis from the past fifteen years, and major progress towards the goal of showing that for every classical theorem of mathematical physics, there is a comparably elegant constructive counterpart. I will also say a little bit about my own work towards this goal, on representations of compact Lie groups.
In this talk we will briefly review what is known about the relationship of ordinal notations to bounded arithmetic. We will discuss in detail new results concerning provability of well-foundedness of total orderings on bounded (i.e. finite) domains in bounded arithmetic. The main results are that the orderings of ordinal notations for $\epsilon_0$ and $\Gamma_0$, if restricted to a finite domain, can be proved well-founded in the second level $S^2_2$ of the bounded arithmetic hierarchy, while the first level $S^1_2$ cannot do this, unless something bad happens like P=NP.