On the strength of some systems with numerical omniscience scheme

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.

Logic and Games: close encounters of the third kind. Part I

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:

- Games and strategies as unifying notions inside logic (evaluation, model construction, model comparison, proof)
- General algebra of game operations (Parikh, Abramsky) (game extensions of dynamic logics and process algebra)
- Imperfect information games (Hintikka, Rubinstein) (a current area of controversy over interpretation)
- and if time permits: Further interactions between logic and game theory (rationality, equilibrium, preference, probability)

References:

- J. van Benthem, 1999, "Logic and Games", electronic course notes, http://turing.wins.uva.nl/~johan/teaching
- some new manuscripts - to be posted as we proceed
- Marc Pauly's 'Logic and Games at Amsterdam' WWWpage (with pictures!): http://www.cwi.nl/~pauly/games.html
- M. Osborne & A, Rubinstein, 1994, "A Course in Game Theory", MIT Press, Cambridge (Mass.).

Logic and Games, Parts II and III

Part I was on Tuesday April 11 under the title *Logic Games*.

We have looked at

- Introduction: general connections logic/games/game-theory
- First-order evaluation games, and some general issues
that they give rise to (properly viewed):
- determinacy,
- notions of game equivalence,
- natural sequential game operations.

- Model construction games, and some further issues:
- the unifying role of strategies ('models', proofs)
- the use for a general strategy calculus,
- possible use for parallel game operations.

- Model comparison games, and yet two more issues:
- removing 'E-sickness' by making strategies explicit,
- 'E=H-square': constructions that relate logic games.

- The main drift of to-day's story for logicians: 'Games and Strategies in Elementary Logic', http://turing.wins.uva.nl/~johan/Taiwan.ps
- A related version written for criminal lawyers: http://turing.wins.uva.nl/~johan/Cardozo.ps

Tuesday April 18 *Game Logics*

Topics will be:

- Dynamic logics for game structure,
- A notion of game equivalence 'bisimulating' players' powers generating a basic decidable sequential game logic.
- The other route: linear game logic of parallel operations.
- An analysis of first-order logic as a general decidable game calculus on top of more specific principles about fact-testing and object-picking games.

References:

- 'When are two games the same?' http://turing.wins.uva.nl/~johan/TORINO.ps
- 'Basic game algebra inside predicate logic' http://turing.wins.uva.nl/~johan/game-algebra.ps

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:

- Interplay of knowledge and action,
- Update of players' information as the game proceeds,
- Game equivalence under uncertainty.

Reference:

- '"Hintikka Self-Applied": an essay on the logic of imperfect information games' http://turing.wins.uva.nl/~johan/H(H).ps

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

What Mathematics Owes to Quantum Mechanics: the work of John von Neumann, 1927-1932

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.

Ergodic Theory and Spectral Theory from a Constructive Point of View

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.

Ordinal notations and well-orderings in bounded arithmetic

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.

Last modified: Tue May 23 14:28:22 PDT 2000