Title and Abstract of Invited Talks
Logics with explicit evidence : A Quantified Logic of 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.
A program for the axiom of dependent choice
by Jean-Louis Krivine (Preuves-Programmes-Systèmes, Université Paris 7, France)The axiom of dependent choice ADC is fundamental in mathematical analysis; therefore, we must give a program for ADC, if we want to extract programs from proofs in analysis. This problem is solved by adding new instructions to lambda-calculus, which are very well known in the programming world: the clock and the signature. We show that application of ADC corresponds to the process of "updating files".
Locality of queries and transformations
by Leonid Libkin (Department of Computer Science, University of Toronto, Canada)It was proved by Gaifman in 1981 that first-order formulas only express local properties; that is, they cannot distinguish tuples with small isomorphic neighborhoods. This result has found many applications, especially in computer science, and has been extended to other logics as well. In this talk I shall describe two recent variations on the locality theme. The first question asks whether a logic is strongly local in the sense that its formulas cannot distinguish tuples whose small neighborhoods are indistinguishable in the logic itself. Although intuitively this should be true for any local logic, the real picture is much more complicated. The second question asks about locality of transformations, rather than queries definable by formulas. The notion of strong locality turns out to be the right one for dealing with transformations, and we present some recent results together with a few applications.
Intuitionistic Frege Systems are Polynomially Equivalent
by Grigori Mints (Depts of Philosophy, and Computer Science, Stanford University, USA)It is possible to simulate polynomially (in a Frege system) every intuitionistically admissible schematic rule stated with standard connectives comjunction, disjunction,negation,implication and show that any two intuitionistic Frege systems polynomially simulate each other.
(Joint work with A. Kozhevnikov)
Groups in Nonstandard Complex Manifolds
by Thomas Scanlon (Mathematics Department, University of California at Berkeley, USA)A compact complex manifold given with predicates for each closed analytic subset of each Cartesian power is a Zariski-type structure. As such, it satisfies the Zilber trichotomy for its minimal types, as does any elementary extension. That is, every nontrivial minimal type is nonorthogonal to the generic type of a field or of a locally modular group. We refine this trichotomy by classifying the minimal groups interpretable in elementary extensions of compact complex manifolds showing that any such minimal group is either a one-dimensional algebraic group over the nonstandard complex numbers or is "compact" in a precise and natural sense. [This talk is based on joint work with Matthias Aschenbrenner and Rahim Moosa.]
Short Descriptions of Random Structures
by Joel Spencer (Courant Institute, New York, USA)We define the complexity $f(S)$ of a finite structure $S$ as the lowest quantifier depth of a first order sentence that fully describes the structure. We examine $f(S)$ where $S$ is chosen from a variety of random models. In particular, we examine the random graph $G(n,p)$, the random ordered graph $G_{<}(n,p)$, and the random unary predicate $U(n,p)$, all with $p=\frac{1}{2}$. The complexities are $\Theta(\ln n)$, $\Theta(\ln^*n)$ and $\Theta(\ln\ln n)$ in these cases.
Last modified: July 21, 2005, 11:16:20 GMT-0300.