Logic Seminar Abstracts

Parigot's lambda mu calculus is a proof-term calculus for classical logic, in much the same way as the lambda calculus is for intuitionistic logic. It has an appealing interpretation as a programming language with control operators. The first part of this talk will be a tutorial on the lambda-mu calculus. In the second part, I will describe a categorical model of the simply-typed labmda-mu calculus, which generalizes the well-known correspondence between the simply-typed lambda calculus and cartesian-closed categories. I will show that the call-by-name lambda mu calculus forms an internal language for these categories. Moreover, the call-by-value lambda mu calculus forms an internal language for the dual co-control categories. As a consequence, one obtains a syntactic, isomorphic translation between call-by-name and call-by-value which preserves the operational semantics, answering a question of Streicher and Reus. This result makes precise the intuitive duality between data-driven and demand-driven computation.

Last week, I introduced the simply-typed lambda-mu calculus and described intuitively how one evaluates expressions, and why the type system corresponds to classical logic. This time, I will define the semantics of the lambda-mu calculus more carefully. I will distinguish between the call-by-value and call-by-name calculi. In each case, I will define a reduction relation (beta-reduction), and an equivalence relation (beta-eta-equivalence). I will give their basic properties, and then hopefully get to categorical models.

Abstract (adapted from the author's abstract):
The article is concerned with the study of (unramified) bounded applicative theories which have a strong relationship to classes of computational complexity. New applicative systems [based on an untyped partial combinatory algebra] are proposed whose provably recursive functions conicide with the functions computable in polynomial time, polynomial space, polynomial time and linear space, as well as linear space. The theories can be regarded as applicative analogues of traditional systems of bounded arithmetic. Higher type systems can also be translated directly into these applicative systems; in particular, it is shown that Cook and Urquhart's system PV^omega is directly contained in a natural applicative theory of polynomial time strength.

Abstract (adapted from the author's abstract): The article is concerned with the study of (unramified) bounded applicative theories which have a strong relationship to classes of computational complexity. New applicative systems [based on an untyped partial combinatory algebra] are proposed whose provably recursive functions coincide with the functions computable in polynomial time, polynomial space, polynomial time and linear space, as well as linear space. The theories can be regarded as applicative analogues of traditional systems of bounded arithmetic. Higher type systems can also be translated directly into these applicative systems; in particular, it is shown that Cook and Urquhart's system PV^omega is directly contained in a natural applicative theory of polynomial time strength.

....

The applicative systems in question were described at the Feb. 6 meeting, and the lower bound arguments were outlined. This time, the upper bound arguments will be sketched using cut-elimination and realizability methods.

Abstract: Camille Jordan's proof (1893) of the theorem in his Cours d'Analyse was heavily criticized by his contemporaries as not satisfying the then newly found standards of rigour. We give a proof which follows closely Jordan's ideas but does so in a nonstandard context removing thus the epsilontic burden of the approximations required for the proof. In such a context Jordan's proof becomes concise, clear and absolutely elementary. The talk will have three parts: (1) some remarks about the result and its historical background, (2) exposition of the nonstandard proof, (3) - depending on the audience and time permitting - an outline of recent work on nonstandard axiomatic set theories can be given.

The epsilon substitution method was proposed by Hilbert and attracted the attention of many researchers interested in the foundations of mathematics including J. von Neumann, H. Weyl, Th. Skolem, and W. Ackermann. Nevertheless the problem of extension of this method to analysis, stated by Hilbert, is still open.

This talk presents an extension of Hilbert's epsilon substitution method to first order arithmetic with free predicate symbols. This is a stage in an extension to analysis. Termination of this method is a consequence of earlier results for predicate logic.

After a brief flirtation with logicism in 1917-1920, David Hilbert proposed his own program in the foundations of mathematics in 1920 and developed it, in concert with collaborators such as Paul Bernays and Wilhelm Ackermann, throughout the 1920s. The two technical pillars of the project were the development of axiomatic systems for ever stronger and more comprehensive areas of mathematics and finitistic proofs of consistency of these systems. Early advances in these areas were made by Hilbert (and Bernays) in a series of lecture courses at the University of Göttingen between 1917 and 1923, and notably in Ackermann's dissertation of 1924. The main innovation was the invention of the epsilon-calculus, on which Hilbert's axiom systems were based, and the development of the epsilon-substitution method as a basis for consistency proofs. The talk traces the development of the "simultaneous development of logic and mathematics" through the epsilon-notation and provides an analysis of Ackermann's consistency proofs for primitive recursive arithmetic and for the first comprehensive mathematical system, the latter using the substitution method. It is striking that these proofs use transfinite induction not dissimilar to that used in Gentzen's later consistency proof as well as non-primitive recursive definitions, and that these methods were accepted as finitistic at the time.