Title and Abstract of Tutorial Lectures
Logics with explicit evidence (slides)
by Melvin Fitting (Dept of Maths and Computer Science, Lehman College, City Univ of New York, USA)Sergei Artemov has developed a logic that he calls LP, for Logic of Proofs. It has infinitely many "proof polynomials" each of which behaves like a (non-normal) modal operator. If t is a proof polynomial, t:X is read "t is a proof of X." Part of the formal machinery of LP is a set of operations on proof polynomials, corresponding to operations on formal proofs, such as combining a proof of A with one for A -> B to produce a proof of B. The logic LP was formulated axiomatically, and also via Gentzen sequents. Among Artemov's results are the following. 1. LP has a connection with explicit provability in Peano arithmetic analogous to the connection between GL (Godel-Lob Logic) and provability in Peano arithmetic. 2. If one applies a "forgetful" functor to a theorem of LP, replacing all proof polynomials by a modal necessity operator, one gets a theorem of S4. 3. If one begins with a theorem of S4, there is always a way of replacing occurrences of the necessity operator with proof polynomials to produce a theorem of LP. Thus LP makes the bridge between Peano arithmetic and S4, which is something whose existence Godel suggested long ago. Since intuitionistic logic has an interpretation in S4, this provides an arithmetic semantics for that.
Artemov's work was proof theoretic. I have since supplied a natural Kripke-style semantics for LP, and provided semantic arguments for Artemov's results. In doing so, it became clear that LP is really an example of a logic of explicit evidence, wherein evidence is restricted to proofs. It is this direction that has been explored more recently. LP is one of a family of logics of explicit evidence, all of which are related to logics of knowledge generally. They provide a natural mechanism for avoiding the so-called "logical omniscience" problems. The consequences of things that are known are also known but evidence for them is more complex, and so one can place natural bounds on the complexity of evidence we wish to consider.
I will discuss the background of LP and its importance for the completion of the program initiated by Godel to provide a foundation for intuitionistic logic using the notion of provability. Then I will present the Kripke-style semantics, and sketch how it can be used to give alternative proofs of things like cut elimination for LP. And finally, I will discuss work currently in progress by Artemov, myself, and other colleagues, concerning the general notion of logics of explicit evidence and their relationships with logics of knowledge.
Curry-Howard correspondence in classical set theory
by Jean-Louis Krivine (Preuves-Programmes-Systèmes, Université Paris 7, France)We develop a theory of realizability in classical logic which appears to be a non trivial generalization of set-theoretical forcing; indeed, usual forcing is a degenerate case of realizability. In this setting, conditions are terms in an extended lambda-calculus. In this way, we can extract programs from proofs in ZF. We obtain also new "generic" models of ZF (but no new independence result) with strange features: for example, the generic may be a new integer with very interesting properties.
How to analyze expressiveness of logics over finite models
by Leonid Libkin (Department of Computer Science, University of Toronto, Canada)In the early days of finite model theory, proving any bound on the expressiveness of a logic was a big deal, because it usually involved playing games, and nontrivial combinatorial arguments. But the subject has come of age, and now most proofs that looked hard two decades ago are easy and can be given as exercises to students. In this introductory talk I shall survey some "off-the-shelf" techniques for proving expressivity bounds for logics over finite structures.
A simple substitution method for ID1
by Grigori Mints (Depts of Philosophy, and Computer Science, Stanford University, USA)We present a new termination proof of Hilbert's epsilon substitution method for the system ID1 of iterated inductive definitions. This provides witnesses for \Sigma^0_1 theorems and proves that the theory is consistent.
The proof is non-effective, but is much shorter than other proofs. The definition of the process is effective, and avoids the use of history, proof-theoretic ordinals, and collapsing techniques required for effective proofs (in particular, [Arai 1999]).
We show that an infinitely long process would have to include guesses at existential formulas more complicated than any the process could generate. This implies that the substitution process actually employs only finite substitutions and terminates in finitely many steps.
(Joint work with Henry Towsner)
Infinitesimals in Model Theory
by Thomas Scanlon (Mathematics Department, University of California at Berkeley, USA)A. Robinson's nonstandard analysis is credited with defending infinitesimals from the calumny of inconsistency. While nonstandard analysis is founded on the compactness theorem, the sine qua non of first-order logic, its study seems to have little more to do with logic. Moreover, by and large, geometers have been content to develop an alternate theory of nilpotent infinitesimals.
In his initial approach to the theory of Zariski geometries, extending his earlier work on totally categorical theories, Zilber proposed a "nonstandard analysis" interpretation complete with infinitesimal neighborhoods and tangency. To date, no analogue of Robinson's legitimization of Leibniz's formalism has been achieved for Zilber's abstract infinitesimal analysis, but in many theories of geometric interest analyzable via Zariski geometries the key results may be proven using differential methods in the geometers' sense.
The Strange Logic of Random Graphs (slides)
by Joel Spencer (Courant Institute, New York, USA)We give the Erd\H{o}s-R\'enyi notion of the random graph $G(n,p(n))$ [$n$ vertices, adjacency probability $p=p(n)$] and examine it from a first order perspective. For any first order property $A$ we consider the limit of the probability of $A$ as $n$ approaches infinity. For some $p=p(n)$ (e.g., $p=n^{-\alpha}$ with $\alpha\in (0,1)$ irrational) we show that this limit is always zero or one. This leads to a complete theory and a discussion of countable models. For other $p=p(n)$ (e.g., $p=c/n$ with $c$ a positive constant) the limit always exists and is of a prescribed form. A link is made to playing the Ehrenfeucht game (which we shall define) on two random structures.
We also briefly explore other random structures, such as random unary predicates (or bit strings) and random ordered graphs.
Note: In this tutorial lecture a knowledge of random graphs shall not be assummed.
Last modified: July 21, 2005, 11:10:20 GMT-0300.