The Lindström Lectures

About Per (Pelle) Lindström

This is a much condensed version of the obituary by Väänänen and Westerståhl in Theoria 2010 (76) pages 100-107. (Link to the obituary – pdf , 180 K)

Per Lindström, or Pelle Lindström as he insisted on being called, was born on April 9, 1936, and spent most of his academic life at the Department of Philosophy, University of Gothenburg, in Sweden, where he was employed first as a lecturer (‘docent’) and, from 1991 until his retirement in 2001, as a Professor of Logic.

Lindström is most famous for his work in model theory. In 1964 he made his first major contribution, the so-called Lindström’s test for model completeness. In 1966 he proved the undefinability of well-order in L_ω1ω (obtained independently and in more generality by Lopez-Escobar). The same year he also introduced the concept of a Lindström quantifier, which has now become standard in model theory, theoretical computer science, and formal semantics.

It was his 1969 paper ‘On extensions of elementary logic’ (in Theoria), where he presented his famous characterizations of first-order logic—Lindström’s Theorem—in terms of properties such as compactness, completeness, and Löwenheim-Skolem properties, that was first recognized as a major contribution to logic. It laid the foundation of what has become known as abstract model theory. The proof was based on Ehrenfeucht-Fraïssé games, a concept he came up with independently, and on a new proof of interpolation. Several other characterizations of first-order logic followed in later papers.

Beginning at the end of the 1970’s, Lindström turned his attention to the study of formal arithmetic and interpretability. He started a truly systematic investigation of this topic, which had been somewhat dormant since Feferman’s pioneering contributions in the late 1950’s. In doing so he invented novel technically advanced tools, for example, the so-called Lindström fixed point construction, a far-reaching application of Gödel’s diagonalization lemma to define arithmetical formulas with specific properties.
Pelle Lindström had an exceptionally clear and concise style in writing mathematical logic. His 1997 book, Aspects of Incompleteness, remains a perfect example: it provides a systematic introduction to his work in arithmetic and interpretability. The book is short but rich in material.

Throughout his life, Pelle Lindström also took an active interest in philosophy. He participated in the debate following Roger Penrose’s new version of the argument that Gödel’s Incompleteness Theorems show that the human mind is not mechanical. He presented his own philosophy of mathematics, which he called ‘quasi-realism’, in a paper in The Monist in 2000. It is based on the idea that the ‘visualizable’ parts of mathematics are beyond doubt (and that classical logic holds for them). He counted as visualizable not only the ω-sequence
of natural numbers but also arbitrary sets of numbers, the latter visualizable as branches in the infinite binary tree, whereas nothing similar can be said for sets of sets of numbers, for example.

Pelle Lindström passed away in Gothenburg, Sweden, on August 21, 2009, after a short period of illness.

Lindström Lectures 2023

Invited guest speaker was Rineke Verbrugge, Professor of Logic and Cognition, Bernoulli Institute of Mathematics, Computer Science and Artificial Intelligence, University of Groningen. The public lecture took place in Humanisten on 11 May 2023 followed by the research lecture on 12 May.

Public lecture: Combining probability and provability logic

It has been shown in the late 1960s that each formula of first-order logic without constants and function symbols obeys a zero-one law: As the number of elements of finite models increases, every formula holds either in almost all or in almost no models of that size. For modal logics, limit behavior for models and frames may differ. In 1994, Halpern and Kapron proved zero-one laws for classes of models corresponding to the modal logics K, T, S4, and S5. They also proposed zero-one laws for the corresponding classes of frames, but their zero-one law for K-frames has since been disproved, and so has more recently their zero-one law for S4-frames.

Provability logic was one of the main interests of Per Lindström. In this talk, we prove zero-one laws for provability logic with respect to both model and frame validity. Moreover, we axiomatize validity in almost all irreflexive transitive finite models and in almost all irreflexive transitive finite frames, leading to two different axiom systems. In the proofs, we use a combinatorial result by Kleitman and Rothschild about the structure of finite (strict) partial orders: almost all of them consist of only three layers. Finally, we present empirical results in order to give an idea of the number of elements from which onwards a formula’s almost sure validity or almost sure invalidity stabilizes in such three-layer Kleitman-Rothschild frames. We also discuss possible extensions of the zero-one laws to the modal logics S4 and K4.

Research lecture: Aspects of provability and interpretability

In 1994, Rineke Verbrugge did a postdoc in Gothenburg, as a scientific guest of Professor Per Lindström, who was writing his landmark book Aspects of Incompleteness at the time. Even though the two of them did not co-author any papers that year, there was still significant mutual influence and there were very lively discussions in the weekly seminars of the logic group. In this research lecture, Rineke Verbrugge will present some of the questions and results around bounded arithmetic, provability and interpretability logic that she was working on that year, for example, a small reflection principle for bounded arithmetic and the lattice of feasible interpretability types.

The Lindström Lectures 2022

Invited guest speaker was Sara Negri, Professor of Mathematics at the University of Genoa. The public lecture occurred on 20 June 2022 followed by the research lecture on 22 June. Both lectures were held in Humanisten.

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 [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 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, Π¹₁ 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.

The Lindström Lectures 2013

The Lindström Lectures series was inaugurated 2013 with lectures by Wilfrid Hodges, Emeritus Professor of Mathematics, Queen Mary, University of London. He is best known for his influential and wide-ranging work in mathematical logic, as expounded in his exquisitely crafted papers and books, including a definitive 780-page graduate text on model theory. His recent research work has focused on general semantics, cognitive aspects of logic, and history of logic, especially Arabic logic.

Professor Hodges attended New College, Oxford (1959–65), where he received degrees in both Literae Humaniores and (Christianic) Theology. In 1970 he was awarded a doctorate for a thesis in Logic. He lectured in both Philosophy and Mathematics at Bedford College, University of London. He was Professor of Mathematics at Queen Mary, University of London from 1987 to 2006. He has held visiting appointments in the department of philosophy at the University of California and in the department of mathematics at University of Colorado. He was President of the British Logic Colloquium, of the European Association for Logic, Language and Information and of the Division of Logic, Methodology, and Philosophy of Science. In 2009 he was elected a Fellow of the British Academy.

Public Lecture: Wilfrid Hodges on Ibn Sina on the foundations of logic

Ibn Sina (Avicenna, 11th century Iran) believed that the foundations of logic lie in metaphysics. He complained bitterly that this has led people to confuse logic itself with its foundations and dress up metaphysics as logic. His own description of the foundations of logic is in overtly ontological language. But from a modern perspective it becomes clear that in fact he is talking about methodological issues, like how to represent occurrences of a component within a compound, and whether the primitive notions of a theory should be stipulated from outside (as in Tarski) or incorporated into the objects (as in web ontology and object-based programming). This all has strong implications for any project to formalise Ibn Sina's logic. My own readings of some key passages are different from the traditional metaphysical ones, and seem to me more intelligible and highly comparable with some modern metalogical and metalinguistic views; but then I have a deaf ear for metaphysics.

Research Lecture: Wilfrid Hodges on Ibn Sina on discharging assumptions in proofs

Ibn Sina (Avicenna, 11th century Iran) wrote thousands of pages of commentary on Aristotle's logical works. Among them is a short section on how to understand proofs by reductio ad absurdum. For Ibn Sina the problem is how to read an RAA proof so that the conclusion self-evidently follows from the premises, making minimal changes to the written form of the proof. In remarks almost certainly based on the Arabic Euclid, he observes (like Frege) that an assumption is stated so as not to have to keep repeating it at every stage of the argument. He infers that to see what is really meant in the argument, one should restore the assumption at every step where it is used. (Again this parallels Frege, though the motivation is different.) A key question is how Ibn Sina knows that adding these assumptions preserves validity. Writing out the answer as a metaprinciple yields a powerful rule of inference, which needs not much else added to give a complete sequent calculus for first-order logic - though Ibn Sina would have strongly disapproved of treating it that way.