The Lindström Lectures 2022
Invited guest speaker was Sara Negri, Professor of Mathematics at the University of Genoa.
Public lecture: Syntax and semantics in synergy
Syntax and semantics, often considered as conflicting aspects of logic, have turned out to be intertwined in a methodology for generating complete proof systems for wide families of non-classical logics. In this formal semantics, models can be considered as purely mathematical objects with no ontological assumptions upon them. More specifically, by the “labelled formalism”, which now is a well-developed methodology, the semantics is turned into an essential component in the syntax of logical calculi. Thus enriched, the calculi not only constitute a tool for the automatisation of reasoning, but can also be used at the meta-level to establish general structural properties of logical systems and direct proofs of completeness up to decidability in the terminating case. The calculi, on the other hand, can be used to find simplified models through conservativity results. The method will be illustrated with gradually generalised semantics, including topological ones such as neighbourhood semantics.
Research lecture: On modal embeddings
Motivated by the difficulty in proving faithfulness of various modal embeddings (starting with Gödel's translation of intuitionistic logic into S4), we use labelled calculi to obtain simple and uniform faithfulness proofs for the embedding of intermediate logics into their modal companions, and of intuitionistic logic into provability logic, including extensions to infinitary logics.
The Lindström Lectures 2019
The 2019 Lindström Lectures was delivered by Johan van Benthem, University Professor of Logic, emeritus (University of Amsterdam), Henry Waldgrave Stuart Professor of Philosophy (Stanford University), Jin Yuelin Chair (Tsinghua University Beijing).
Van Benthem obtained his PhD from University of Amsterdam in 1977. His work since then has contributed to a remarkably wide range of topics within logic, including modal and temporal logic, logic and epistemology/philosophy of science, logical semantics and syntax of natural language, logics of space, and dynamic logics of information, computation and communication. Van Benthem has published over 500 articles and 10 edited books in logic, and has supervised over 80 PhD students in the field. He is founding director of the Institute for Logic, Language and Computation (ILLC, University of Amsterdam), first chair of the European Foundation for Logic, Language and Information (FoLLI), chair of the first Dutch national research program in cognitive science, and is co-director of the Amsterdam–Tsinghua Research Center for Logic.
Public Lecture: Logic and Agency: The Promises and The Challenges
Abstract: One face of logic is turned toward truth and eternal consequence, but another face is dynamic, looking toward activities of reasoning and information handling by agents. In this lecture, I will develop the dynamic perspective, showing how key aspects of rational agency fit in the agenda of logic, such as handling and integrating information from various sources, revising erroneous beliefs, and balancing information with preferences and goals. In this lecture, the vehicle for achieving this will be dynamic-epistemic logics for various sorts of update. These mesh eventually with richer logics of games and strategic interaction. After all, much of reasoning is a social multi-agent process: 'intelligence seldom comes alone'. I end this part by noting how the two faces of logic share the same methodology, and are in fact complementary.
However, 'more logic' is just one way to go in studying agency. I briefly discuss current challenges from the 'less logic' camp, where successful behavior is explained by dynamical systems with very simple agents, or from learning systems that may not have a logical formulation at all. I hope to show that logic retains a valuable role even in that stormy setting.
Research Lecture: Dynamic Logics of Model Change
Abstract: Information update and real-world action suggest a universe of changing models, where finding the valid dynamic laws involves logical languages with modalities for model change. I will discuss two families of such dynamic modal logics, stating some typical results, as well as open problems.
Dynamic-epistemic logics add dynamic superstructure to existing static logics, and tend to not increase complexity of satisfiability and model checking. Logics of graph change, arising e.g. in the study of games or of languages that change their own models under evaluation, tend to jump to higher complexities, becoming undecidable or worse. I will report some recent results that zoom in on the border line between the two kinds of system, and end with some issues about redesign and restoring decidability for more complex logics of action and information dynamics.
The 2019 Lindström Lectures was co-located with the conference Circularity in Syntax and Semantics.
The Lindström Lectures 2018
The 2018 Lindström Lectures was delivered by Michael Rathjen, Professor of Pure Mathematics at University of Leeds. He obtained his Ph.D. (1988) and Habilitation (1992) at University of Münster. Rathjen is renown for his fundamental contributions to Proof Theory, especially cut elimination for infinitary proof systems, ordinal analysis of impredicative theories and calibration of set-existence strength of combinatorial principles. He has also carried out penetrating investigations in intuitionistic and constructive mathematics, including Martin-Löf type theory.
Public Lecture: Progressions of theories and slow consistency
Abstract: The fact that “natural” theories, i.e. theories which have something like an ‘idea’ to them, are almost always linearly ordered with regard to logical strength has been called one of the great mysteries of the foundation of mathematics. Using paradoxical methods, e.g. self-reference Rosser-style, one can distill theories with incomparable logical strengths and show that the degree structure of logical strengths is dense in that between two theories S<T one can always find a third Q such that S<Q<T. But are there ‘natural’ examples of such phenomena? We also know how to produce a stronger theory by adding the consistency of the theory. Can we get a stronger theory by adding something weaker than consistency that is still “natural”? These and other questions will be broached in the talk.
Research Lecture: Bounds for the strength of the graph minor and the immersion theorem
Abstract: The graph minor theorem, GM, is arguably the most important theorem of graph theory. The strength of GM exceeds that of the standard classification systems of RM known as the “big five”. The plan is to survey the current knowledge about the strength of GM and other Kruskal-like principles, presenting lower and upper bounds.
The Lindström Lectures 2017
The 2017 Lindström Lectures was delivered by Albert Visser, Emeritus Professor of Philosophy at Utrecht University, where he served as professor of logic, philosophy of mathematics, and epistemology in the period 1998-2016. He obtained his Ph.D. in 1981 under the direction of Dirk van Dalen at Utrecht University, the Netherlands. His research centers on arithmetical theories, interpretability, constructivism, foundations of mathematics and topics in the philosophy of language. He is a member of the Royal Netherlands Academy of Arts and Sciences, and the editorial board of the Notre Dame Journal of Formal Logic.
Public Lecture: De Interpretatione
Per Lindström’s work on interpretations has great beauty. He was a grand master of dazzling diagonal arguments. In this talk we will explain the basic setting underlying Per’s work. We introduce the notion of interpretation and provide some examples of interpretations. We show how, in the context of arithmetic, the notion of interpretability has an almost unrecognizable equivalent. This equivalence is known as the Orey-Hájek Characterization.
We will discuss some results of Per and have a look at further developments.
Research Lecture: The Second Incompleteness Theorem in a (somewhat) General Setting
We study the Second Incompleteness Theorem, G2, in the Feferman-style. This means that we work with a fixed provability-predicate but allow the representations of the axiom set to vary. Feferman observed that the axiom set of Peano Arithmetic, PA, has a Pi^0_1-representation for which PA proves its own consistency.
We isolate a condition that Feferman’s example fails to satisfy. This condition gives a reasonably general version of G2. We show that this version yields a proof of G2 for Sigma^0_1-semi-numerations of the axiom set which works even if the theory itself is not recursively enumerable. We discuss an interesting example that illustrates that we may have G2 even in the absence of the Löb conditions.
The Lindström Lectures 2014
The second series of Lindström Lectures will be delivered 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 lecture of Joan Rand Moschovakis:
Intuitionistic Analysis, Forward and Backward
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.
Public lecture of Yiannis Moschovakis:
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  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 lecture of Joan Rand Moschovakis:
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 lecture of Yiannis Moschovakis:
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.