Archive of events from 2014

The language L over a fixed vocabulary K is an (applied) typed λ-calculus with additional constructs for acyclic recursion and attitudinal application, an extension of Montague’s Language of Intensional Logic LIL as formulated by Daniel Gallin. It is denotationally interpretable in the classical typed λ-calculus over K, but intensionally richer: in particular, it can define the referential intension of each term A, an abstract algorithm which computes the denotation of A and provides a plausible explication of its meaning.

The key mathematical construction of L is an effective reduction calculus which compiles each term A into an (essentially) unique canonical form cf(A), a denotational term which explicates the logical form of A and from which the referential intension of A can be read off. The central open problem about L (over a finite, interpreted vocabulary) is the decidability of global synonymy - and it is a problem about the classical, interpreted typed λ-calculus.

Each variety of reverse mathematics attempts to determine a minimal axiomatic basis for proving a particular mathematical theorem. Classical reverse analysis asks which set existence axioms are needed to prove particular theorems of classical second-order number theory. Intuitionistic reverse analysis asks which intuitionistically accepted properties of numbers and functions suffice to prove particular theorems of intuitionistic analysis using intuitionistic logic; it may also consider the relative strength of classical principles which do not contradict intuitionistic analysis.

S. Simpson showed that many theorems of classical analysis are equivalent, over a weak system PRA of primitive recursive arithmetic, to one of the following set existence principles: recursive comprehension, arithmetical comprehension, weak Konig’s Lemma, arithmetical transfinite recursion, Π11 comprehension. Intermediate principles are studied also. Intuitionistic analysis depends on function existence principles: countable and dependent choice, fan and bar theorems, continuous choice.

The fan and bar theorems have important mathematical equivalents. W. Veldman, building on a proof by T. Coquand, recently showed that over intuitionistic two-sorted recursive arithmetic BIM the principle of open induction is strictly intermediate between the fan and bar theorems, and is equivalent to intuitionistic versions of a number of classical theorems. Intuitionistic logic separates classically equivalent versions of countable choice, and it matters how decidability is interpreted. R. Solovay recently showed that Markov’s Principle is surprisingly strong in the presence of the bar theorem. The picture gradually becomes clear.

In his classical 1892 article On sense and denotation, Frege associates with each declarative sentence its denotation (truth value) and also its sense (meaning) “wherein the mode of presentation [of the denotation] is contained”. For example, 1+1=2 and there are infinitely many prime numbers are both true, but they mean different things - they are not synonymous. Frege [1892] has an extensive discussion of senses and their properties, including, for example, the claim that the same sense has different expressions in different languages or even in the same language; but he does not say what senses are or give an axiomatization of their theory which might make it possible to prove these claims. This has led to a large literature by philosophers of language and logicians on the subject, which is still today an active research topic. A plausible approach that has been discussed by many (including Michael Dummett) is suggested by the “wherein” quote above: in slogan form, the sense of a sentence is an algorithm which computes its denotation. Coupled with a rigorous definition of (abstract, possibly infnitary) algorithms, this leads to a rich theory of meaning and synonymy for suitably formalized fragments of natural language, including Richard Montague’s Language of Intensional Logic. My aim in this talk is to discuss with as few technicalities as possible how this program can be carried out and what it contributes to our understanding of some classical puzzles in the philosophy of language.

In the early 20th century the Dutch mathematician L. E. J. Brouwer questioned the universal applicability of the Aristotelian law of excluded middle and proposed basing mathematical analysis on informal intuitionistic logic, with natural numbers and choice sequences (infinitely proceeding sequences of freely chosen natural numbers) as objects. For Brouwer, numbers and choice sequences were mental constructions which by their nature satisfied mathematical induction, countable and dependent choice, bar induction, and a continuity principle contradicting classical logic. Half a century later, S. C. Kleene and R. E. Vesley developed a significant part of Brouwer’s intuitionistic analysis in a formal system FIM. Kleene’s function-realizability interpretation proved FIM consistent relative to its classically correct subsystem B, facilitating a detailed comparison of intuitionistic with classical analysis C. Continuing Brouwer’s work into the 21st century, Wim Veldman and others are now developing an intuitionistic reverse mathematics parallel to, but diverging significantly from, both classical reverse mathematics as established by H. Friedman and S. Simpson, and constructive reverse mathematics in the style of E. Bishop. This lecture provides the basics of intuitionistic analysis and a sketch of its reverse development.

The 33rd meeting of JAF (Journées sur les Arithmétiques Faibles) was held in Gothenburg, Sweden, June 16-18 2014.