Carnegie Mellon University
Past Lectures

Past Ernest Nagel Lectures in Philosophy and Science

The Ernest Nagel Lectures in Philosophy & Science are held biennially. Through presentations by eminent philosophers and scientists, they highlight the deep connection between philosophical reflection and scientific activity.

Click here to view the current Ernest Nagel Lectures in Philosophy & Science.

2013 Lectures

Presented in March 2013 by Per Martin-Löf (Emeritus Professor of Logic, University of Stockholm and Member, Royal Swedish Academy of Sciences and Academia Europaea)


Click on the lectures below to watch the videos.
Lecture I, March 18
Lecture II, March 20
Lecture III, March 22


In a paper from 1934-35, printed in 1936, Lindenbaum and Tarski proved that every object which is definable in simple type theory is invariant under all automorphisms of the individual domain, that is, under all isomorphisms between the individual domain and itself. Thirty years later, in a lecture given at Buffalo in 1966, Tarski proposed to use isomorphism invariance as a criterion for distinguishing between logical and non-logical notions, a distinction the arbitrary character of which he was dissatisfied with in his well-known paper on the concept of logical consequence from 1936.

What happens if we replace classical simple type theory, which is impredicative, and which Lindenbaum and Tarski took to be extensional, by intuitionistic type theory, which differs from classical simple type theory, not only by being intuitionistic, or constructive, but also by being predicative and intensional? At first sight, there appears to be an insuperable obstacle to proving an analogue of the Lindenbaum-Tarski theorem for intuitionistic type theory, namely the presence in it of specific individuals, like zero, which is an element of the set of natural numbers, and zero and one, interpreted as the two elements of the two-element set. Clearly, they are not invariant under arbitrary isomorphisms. There is, however, a way out of this impasse, namely to understand by an isomorphism between two sets no more than a relation between the two sets, and to define a function to be isomorphism invariant if it is extensional, that is, if it yields isomorphic values when it is applied to isomorphic arguments. On this new interpretation of the concepts involved, it does become possible to demonstrate the following analogue of the Lindenbaum-Tarski theorem:

Every object that can be defined in intuitionistic type theory is invariant under isomorphism.

The demonstration takes the form of a model construction as a result of which each definable object gets accompanied by a proof that it is isomorphism invariant.

Lecture I will deal with the forms of judgement of intuitionistic type theory and the categories that correspond to them, making clear what elements of these forms are allowed to be reinterpreted in a non-standard model as opposed to those whose meaning has to remain untouched by any reinterpretation. Lectures II and III will be devoted to the details of the model construction which establishes the stated analogue of the Lindenbaum-Tarski theorem.


A. Lindenbaum and A. Tarski, Über die Beschränktheit der Ausdrucksmittel deduktiver Theorien, Ergebnisse eines mathematischen Kolloquiums, Heft 7 (für das Jahr 1934-35, erschienen 1936), pp.15-22.
A. Tarski, Über den Begriff der logischen Folgerung, Actes du Congrès International de Philosophie Scientifique, fasc. 7, Actualités Scientifiques et Industrielles, vol. 394 (1936), pp. 1-11.
A. Tarski, What are logical notions?, History and Philosophy of Logic, vol. 7 (1986), pp. 143-154.

Related Paper:
Essay on the Philosophical Work of Per Martin-Löf

2010 Lectures

Presented in October 2010 by Brian Skyrms

University of California, Irvine

Naturalizing the Social Contract, October 19
Signals: Evolution, Learning and Information, October 21
On Dynamics and Signaling, October 22

2004 Lectures

Presented in October 2004 by Terrence J. Sejnowski (Salk Institute for Biological Studies)

2002 Lectures

Presented in February 2002 by Bas van Fraassen (Princeton University)

2000 Lectures

Presented in March 2000 by Stuart Kauffman (Santa Fe Institute)

1997 Lectures

Presented in November 1997 by Parick Suppes (Stanford University)

About Ernest Nagel

Old NagelYoung NagelErnest Nagel (1901-1985), one of the most prominent philosophers of science in the 20th century, argued most strongly for the connection between philosophy and science. His book, The Structure of Science: Problems in the Logic of Scientific Explanation (1961) is a classic of the field. In the Encyclopedia of Philosophy, H. S. Thayes writes it is a masterly and complete exposition of his "analysis of explanation, the logic of scientific inquiry, and the logical structure of the organization of scientific knowledge, and it illuminates the cardinal issues concerning the foundation and the assessment of explanation in physics and in the biological and social sciences."

Related Papers:
Biographical Memoir of Ernest Nagel