Logic Seminar Abstracts

We consider a number of topics based around the idea of seeking a good notion of abstract syntax for programming and other formal languages. The usual notion of the `abstract syntax' of a language is that it is given by the terms of a multi-sorted first-order signature. This has many advantages. Terms can be represented naturally as data structures of trees and one can then do meta-programming (e.g. in LISP or ML). One has the apparatus of equational logic, and, more widely first-order logic, for specification and other purposes. One can define programming languages by rewriting techniques, or by structural operational semantics. One can account for compositional denotational semantics by means of initial algebras and homomorphisms. Finally, one has a good notion of syntax-directed translation between different languages (as given by different signatures).

We argue, however, that this is far from enough to account for many phenomena in programming or logical languages. For example there is no account of operations (e.g. integration, or quantification) that bind variables. Again there is no account of structured types, where types are themselves given by expressions of some formal language. We introduce and explore a notion of `binding algebras' to overcome the first difficulty. If there is time we will also discuss how `dependent algebra' may serve to overcome the second one.

Skolemization of an existential quantifier is sound and faithful (provides conservative extension) in the classical logic and in the intuitionistic logic $LJ$ without equality. For intuitionistic logic $LJ^=$ with equality the extension is not conservative and a complete axiomatization was given by C. Smorynski based on the author's previous work. We present here a simple completeness proof for C. Smorynski's axiomatization. This proof can be easily simplified into a completeness proof of the ordinary Skolemization for $LJ$. Smorynski's axioms are intuitionistically derived from the existence of function values and decidability of equality. This proves the completeness of ordinary Skolemization for $LJ^=$ with equality.

1. I will discuss a conception of the reflection principle (RP)
   forall X [phi(X) implies exists beta phi(X)^(V_beta)]

   which admits its natural extension from X of order at most 2 to higher orders (contrary to the doubts Bill Reinhardt express about this in 1974).

2. For eacn n>1, RP, applied to formulas of a certain class G_n, yields the partition property
   kappa arrow (stationary)^n_2.

3. RP applied to G_n is valid in V_kappa when kappa is measurable.
4. Please, somebody, get interested in this conception of constructing numbers from below.

We study extensions of first-order logic with the choice construct (choose x : F(x)). We prove some results about Hilbert's epsilon operator, but in the main part of the paper we consider the case when all choices are independent.

Systems of explicit mathematics (to be reviewed briefly) are extended by variables and suitable principles for higher classes in a certain sense. This is done in such a way that every model of the former expands to a model of the latter. By starting with a model interpreted constructively, several applications--previously treated by other means--can be obtained; the following will be sketched.

1. Semantics of (predicative) polymorphism.
2. Bishop-Cheng constructive measure theory.
3. Constructive functors and natural transformations.
4. Mahlo-style hierarchies of constructive universes.

Our starting point is the Danos-Regnier characterization of cut-free Multiplicative Linear Logic (MLL) proofs as a semantics for MLL. We give a bijection between the essential switchings of an MLL theorem and its expressions as formulas built from variables using only tensor and two implications, o- and -o, where A o- B is equivalent to A' -o B'. Then, following a suggestion of G. Plotkin to interpret the states of a Chu space as evidence against, we take the formulas expressible in this language as the types of a linear lambda-calculus in which a:A denotes evidence a *for* proposition A while x..A denotes evidence x *against* A. This system, which following Goedel and de Paiva we call the dialectic lambda-calculus, differs from other linear lambda-calculi in the literature in having a straightforward axiomatization.

Every deduction in the !-free classical MLL is (the result of an obvious translation of) a deduction in the intuitionistic MLL. This is a joint work with Sergei Soloviev (University of Toulouse)