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 second series of Lindström Lectures was delivered in October 2013 by Joan Rand Moschovakis and Yiannis Moschovakis.
Joan Rand Moschovakis is Emerita Professor of Mathematics at Occidental College, Los Angeles, California. She obtained her undergraduate degree in mathematics at the University of California Berkeley, and completed her doctoral degree in mathematics at the University of Wisconsin, Madison, under the direction of Stephen Kleene. She has also taught in the Graduate Program in Logic and Algorithms at the University of Athens, Greece. Her research interests include Foundations of Intuitionistic Analysis, Intuitionistic Interpretations of Classical Mathematics, Classical Interpretations of Intuitionistic Mathematics, Admissible Rules of Intuitionistic Logic, and History and Philosophy of Intuitionistic Logic.
Yiannis Nicholas Moschovakis is Emeritus Professor of Mathematics at University of Southern California, Los Angeles. During 1996-2005 he also served as professor of mathematics at the University of Athens. He obtained his undergraduate and master’s degrees in mathematics at the Massachusetts Institute of Technology, and completed his doctoral degree at the University of Wisconsin, Madison, under the direction of Stephen Kleene. His research Interests include: Recursion Theory, Descriptive Set Theory, Foundations of Computer Science, Philosophy of Language and Mathematics.
-
Public Lindström Lecture: Joan Rand Moschovakis (Emerita Professor of Mathematics at Occidental College, Los Angeles, California)
Intuitionistic Analysis, Forward and Backward
-
Public Lindström Lecture: Yiannis Moschovakis (Emeritus Professor of Mathematics at University of Southern California, Los Angeles)
Frege’s sense and denotation as algorithm and value
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.
-
Research Lindström Lecture: Joan Rand Moschovakis (Emerita Professor of Mathematics at Occidental College, Los Angeles, California)
Now Under Construction: Intuitionistic Reverse Analysis
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.
-
Research Lindström Lecture: Yiannis Moschovakis (Emeritus Professor of Mathematics at University of Southern California, Los Angeles)
The logical form and meaning of attitudinal sentences
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.