The topics of the conference comprise all areas of logic relating in a narrower or wider sense to Gödel's incompleteness results. This includes the history of logic, proof theory, philosophy of mathematics, aspects of incompleteness in computer science and others.
The conference is organised as a collection of workshops for these specific topics.
On April 26, 2021 Thomas Strahm, a dear friend and close colleague of the organizers and many participants of this meeting, passed away at the age of 57 after prolonged health problems. His research was in the best tradition of Gödel's work and we will remember him at this meeting. You find an obituary at the University of Bern.
The conference is planned as a hybrid event, taking place online and on site in Tübingen during the week from 5 to 9 July 2021.
- 5.7. Monday afternoon: Opening. Higher proof theory after Gödel
- 6.7. Tuesday morning: Computation in face of incompleteness
- 6.7. Tuesday afternoon: Type theory in type theory
- 7.7. Wednesday morning: Cut-elimination and Herbrand's Theorem
- 7.7. Wednesday afternoon: Provability predicates
- 8.7. Thursday morning: Diagonalization
- 8.7. Thursday afternoon: Recursion-theoretic approaches to computation and complexity
- 9.7. Friday morning: Philosophy of mathematics after Gödel
- 9.7. Friday afternoon: Aspects of Gödel's unpublished work; Closing Lecture by Jan von Plato
Gödel’s Introduction to Deduction: Logic Lectures at Notre Dame
Miloš Adžić (University of Belgrade):
Gödel taught a one-semester course in basic logic at the University of Notre Dame in the spring of 1939. Among his unpublished writings in the Princeton University Library one can find notebooks with the manuscript of his notes for that course. Together with Kosta Došen, we have prepared an edition of the notes of which we will offer a brief summary and address some of their importance. We will also comment upon parts of Gödel’s manuscript unavailable to us previously, which were only recently brought to our attention by Jan von Plato.
Gödel’s functional interpretation in context
Maria Hämeen-Anttila (University of Helsinki):
Gödel’s functional interpretation of intuitionistic arithmetic was first introduced in a 1958 article published in the journal Dialectica under the title “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes”. However, the interpretation itself was first discovered by Gödel in 1941, when he was preparing a lecture course on intuitionistic logic at Princeton.
The main sources for the interpretation that Gödel calls ∑ are the Princeton lecture notes, another lecture (“In what sense is intuitionistic logic constructive?”) given in Yale in April 1941, as well as shorthand notes in the notebook series Arbeitshefte and, to a lesser extent, Resultate Grundlagen. In my presentation, I will discuss the historical development of the functional interpretation based on the lecture notes and the shorthand notebooks. The aim is to give a general idea of what there is to be found in the fragmentary notes contained in the Arbeitshefte series, and how they might be used to better understand the early functional interpretation and the problems Gödel encountered while working on it.
The Set Theory in Gödel’s Resultate Grundlagen
Akihiro Kanamori (Boston University):
Most of the four notebooks of Gödel’s 1940-1942 Resultate Grundlagen have to do with set theory, and we find here incisive work of remark- able breadth and depth, much of it replicating the best results achieved at the time or anticipating major avenues of research later. Especially conspicuous are his constructions of an Aronszajn tree and a paradoxical decomposition of the sphere, his formulation of relative constructibility and pointwise definability leading to minimal models, his results in Ramsey-type infinite combinatorics, and his exploration of scales of orders of growth in connection with the Contin- uum Hypothesis. On this last, we now see that his intriguing 1970 remarks on the continuum problem had definite anticipations here.
Gödel's theological notes
Tim Lethen (Saarland University):
In the winter semester of 1937/38, Gödel attended about 30 theological lectures, taking notes which are preserved in his Nachlass in Princeton. These notes are supplemented by an extensive list of theological literature as well as by two lists of literally hundreds of remarks and questions concerning the Catholic Church, the Bible, dogmatics, and theology in general.
The talk will present passages from these sources and attempt to shed light on two of Gödel's main theological concerns. The first one focuses on the idea of formalising theology by capturing a few basic terms and concepts, which are then fixed by a set of axioms and developed into a theory by appropriate rules of inference. In a second approach, Catholic dogmas take on the role of axioms, thus allowing – for example – for a logical investigation of differences between the Western and Eastern Church.
Finally, the talk will present material – recently discovered in Gödel's Nachlass – which reveals his remarkably intensive biblical studies.
The landscape of Gödel's incompleteness theorems
Yong Cheng (Wuhan University)
In the first part of the talk, we will give a brief overview of recent
research on Gödel's incompleteness theorems from the following aspects: (1)
the influence of Gödel's incompleteness theorems on foundations of
mathematics, philosophy and mathematics; (2) different proofs of Gödel's
incompleteness theorems; (3) generalizations of Gödel's incompleteness
theorems; (4) the limit of the applicability of the first incompleteness
theorem (G1); (5) the intensionality problem of Gödel's second incompleteness
In the second part of the talk, we will focus on our recent work of finding
the limit of the first incompleteness theorem (G1) w.r.t. interpretation. We
examine the interpretation degree structure of weak r.e. theories for which
G1 hold, and especially on the question whether there is a minimal r.e. theory
for which G1 holds. We find that the answers depend on the signature of
language and the class of theories we consider.
Yong Cheng, Incompleteness for Higher-Order Arithmetic: An Example Based on
Harrington's Principle, Springer series: Springerbrief in Mathematics,
Yong Cheng, Finding the limit of incompleteness I.
Bulletin of Symbolic Logic, Volume 26, Issue 3-4, December 2020, pp. 268-286.
Yong Cheng, Current research on Gödel's incompleteness theorem, online in The
Bulletin of Symbolic Logic, DOI: 10.1017/bsl.2020.44, 2021.
Helen Preiß (Technical University of Darmstadt):
The Diagonalization Lemma — Demystified Hopefully
Saeed Salehi (University of Tabriz):
The diagonal lemma says that when a computable and injective Gödel coding # is available from the formulas to the closed terms of a fixed language, then for every formula F(x), with x as the only free variable, there exists a sentence S such that S ↔ F(#S) holds. Holding may mean that the above equivalence is true in the standard model of natural numbers (the semantic diagonal lemma) or may mean that the equivalence is provable in a sufficiently strong theory such as Robinson's Arithmetic (the syntactic diagonal lemma).
The so-called lemma, first proved by Gödel (1931) for a particular formula F(x), that of unprovability, and explicated by Carnap (1934) for every formula F, has a (couple of) very short but extremely tricky and easy-to-forget proof(s). The (classical) proof is mysterious and a kind
of magical (pulling a rabbit out of a hat), which adds to the confusion on and about the lemma. It can be even said that once this lemma has been mastered and grasped, then the proofs of the theorems of Gödel's first incompleteness, Tarski's undefinability of truth, and Rosser's (strengthening of Gödel's) incompleteness can be easily understood.
In this talk we will give some alternative proofs for the semantic form of this lemma and for its weak syntactic forms. We will see that the lemma is actually equivalent, in a sense, to the above mentioned theorems of Gödel, Tarski, and Rosser. These new results, we hope, will help us in demystifying this wonderful and prolific lemma; though its classic proof may remain in shadow, our new proofs will hopefully shed some light on the true nature of the diagonal lemma.
· SAEED SALEHI, On the Diagonal Lemma of Gödel and Carnap, The
Bulletin of Symbolic Logic 26:1 (2020) 80—88.
· SAEED SALEHI, Tarski’s Undefinability Theorem and the Diagonal
Lemma, Logic Journal of the IGPL (forthcoming).
Diagonalization, Fixed Points, and Self-reference
Noson S. Yanofsky (Brooklyn College, CUNY):
Some of the most profound and famous theorems in mathematics and computer science of the past 150 years can simultaneously be seen as a consequence of diagonalization, as a fixed-point theorem, and as an instance of a self-referential paradox. These results include Cantor's theorems about different levels of infinity; Russell's paradox; Gödel's incompleteness theorem; Turing's halting problem; and much more. Amazingly, all these diverse theorems and all viewpoints can be seen as instances of a single simple theorem of basic category theory. We describe this theorem and show some of the instances. A large part of the talk will be a discussion of diagonalization proofs, fixed point theorems, and self- referential paradoxes that fail to be an instance of this categorical theorem. We will meet another categorical idea that unifies some of these ideas. No category theory is needed for this talk.
A Uniform Picture of Gap Condition and Collapsing Functions
Anton Freund (Technical University of Darmstadt):
As Gödel showed, in any formal theory for the foundations of mathematics, there are concrete statements that can neither be proved nor
refuted. Mathematical examples of such statements include Kruskal's tree theorem and its strengthening by a gap condition, as shown by H. Friedman. These mathematical independence results are intimately connected to ordinal analysis. The present talk presents a new and very uniform picture of this connection: First, Kruskal's theorem and the Bachmann-Howard ordinal arise by the same construction, applied to partial and linear orders, respectively. Secondly, by iterating this construction, we obtain the gap condition and ordinal collapsing functions. The talk aims to explain the grand lines of this picture in an accessible way. Parts of it are based on joint work with M. Rathjen and A. Weiermann.
Strong Normalization of Gödel's T
Annika Kanckos (University of Helsinki)
Following (Wilken &) Weiermann's proofs of SN of Gödel's T the main problems with SN can be located to the λ-formulation of T and the generality of the recursor reductions in the successor case. These problems typically lead to a non-unique (ordinal) number assignment showing termination. We will, based on an observation of how to implement Howard's permutation lemma, sketch how a unique assignment can be constructed for the full system T.
On the performance of axiom systems.
Wolfram Pohlers (University of Münster):
One of the aims of proof theory is to characterize axiom systems by invariants. Due to Gödel’s second incompleteness theorem it is to be expected that such invariants are unlikely to be finite. Pioneering work in this directions had then been done by Gerhard Gentzen who characterized the axiom system for Peano Arithmetic by the transfinite ordinal ε0. Our aim is to investigate in how far proof–theoretic or- dinals can serve as measures for the performance of axiom system with respect to their intended standard models. The key observation is the “No Enhancement Theorem” which states that the proof–theoretic ordinal of an axiom system will not grow, even if we strengthen it by arbitrary sentences of the elementary diagram of its standard model. Thus the Peano axioms and D(ℕ), the elementary diagram of ℕ augmented by the scheme of Mathematical Induction, share the proof–theoretic ordinal ε0 although D(ℕ) should know everything about ℕ which, due to Gödel, cannot be true for the Peano axioms.
This indicates that the proof–theoretic ordinal of an axiom system A can hardly be a measure for the performance of A with respect to its standard model. It turns out that it rather measures the performance of A with respect to “universes above” its intended standard model. So called impredicative axiom systems axiomatize more than just one universe above its standard model and thus induce a spec- trum of proof–theoretic ordinals. In a previous paper (which will appear in the volume Axiomatic Thinking II, Springer 2021) we studied axiom systems in the language of arithmetic and their spectra in “analytical universes”, i.e. universes whose sets are sets of natural numbers. In the present talk we will indicate how to extend these studies to axiom systems for set theory and set theoretical—especially admissible—universes. We obtain a bridge to abstract α–recursion theory in so far, that the spectra of the investigated axiom systems contain exactly the ordinals which are closed under the α–recursive functions whose totality is provable in the axiom system.
Potentialism and Critical Plural Logic
Øystein Linnebo (University of Oslo):
Potentialism is the view that certain types of entity are successively generated, in such a way that it is impossible to complete the process of generation. What is the correct logic for reasoning about all entities of some such type? Under some plausible assumptions, classical first-order logic has been shown to remain valid, whereas the traditional logic of plurals needs to be restricted. Here I seek to answer the open question of what is the correct plural logic for reasoning about such domains. The answer takes the form of a critical plural logic. An unexpected benefit of this new logic is that it paves the way for an alternative analysis of potentialism, which is simpler and more user-friendly than the extant modal analysis.
Truth in mathematics
Mirna Džamonja (IRIF, CNRS & Université de Paris)
Hilbert’s programme was the holy grail of logic in the late 19th century and the early 20th century. It sought to find common logical foundation to the whole of mathematics, where all the mathematical truths would be derivable from the system through a commonly accepted notion of a proof, preferably in an algorithmic manner. Gödel’s Incompleteness theorems, along with Turing’s undecidability, have put an end to this dream. Logic has been integrating that reality ever since. Logicians have learned how to deal with incompleteness, although not everybody has the same philosophical position on it.
In this talk, we shall move focus on the dual of completeness: the soundness. Formally, there is no reason to question the soundness of our proofs. Heuristically, there is an elephant in the room. Our proofs are becoming uncheckable due to their length, level of sophistication and the partition of the mathematical community into small and very specialised groups which can hardly understand the announcements of each other's theorems. The traditional system of refereeing does not seem to be sufficiently prepared, so serious journals take years to publish as the referees take years to verify and the less serious kind of journals proliferate, feeding on the « publish or perish » credo driven by financial needs of the universities.
It is difficult to propose remedies to this situation. Some of the world’s top mathematicians have noticed and have reacted: Voevodsky, Perelman, the Lean community and yours truly in a joint with Koutsoukou-Argyraki and Paulson.
All of these are tries and, in our opinion, due to the difficulty of implementation which is mostly manual, not likely to resolve the situation in real time. It seems that the soundness problems should be attacked differently. We feel that it is logic that should take over at this point. The logic should help us understand the uncertainty that high level mathematics has become.
Inexhaustibility and Implicit Commitment
Carlo Nicolai (King's College London):
Gödel's incompleteness theorems are often taken to indicate that our mathematical commitments are inexhaustible. Soundness assertions for a mathematical theory T cannot be established in T. However, they appear to be implicit in the acceptance of T. This notion of implicit commitment is often associated with highly technical studies but it remains, so far, an elusive notion. For instance, it is often claimed that the acceptance of a mathematical theory implicitly commits one to the acceptance of a Uniform Reflection Principle for it. However, logicians and philosophers agree that a satisfactory conceptual analysis of the transition from a theory to its reflection principle is still lacking. In the talk I will survey recent proposals to analyse and justify the transition from a theory to its soundness assertions and present some new results and observations. The original material will mainly concern two ways of articulating the notion of implicit commitment: a direct axiomatization of (minimal) implicit commitment, and the analysis of implicit commitment via a primitive truth predicate.
The application of mathematics in Gödel and beyond
Gabriella Crocco (Aix-Marseille Université) and Paola Cantù (CNRS):
The question of the applicability of mathematics to the empirical sciences is crucial in Gödel's philosophy and constitutes a key problem in contemporary philosophy of mathematics. In the first part, the paper emphasizes the importance of applicability in Gödel, suggesting a new reading of Gödel's criticism to Carnap in The Logical Syntax of Language and a comparison with some passages from the unpublished philosophical notebooks Max Phil. In the second part, the paper shows that the question was already central in Frege, Helmholtz and Bettazzi and analyzes its legacy with reference to neologicism and structuralism.
Provability according to Kreisel, Löb, Feferman
Albert Visser (Utrecht University):
In this talk, I discuss three sets of conditions for being a provability predicate: the Kreisel Condition, the Löb Conditions, and Feferman’s Framework for Provability. We review the conditions, have a look at some separating examples and, briefly, discuss the role and place of the sets of conditions.
Secondly, we present the result that every consistent RE theory extending Peano Arithmetic has a provability predicate satisfying all three sets of conditions. We show that this predicate is part of an interesting bi-modal logic. We discuss some applications of the result. If there is still time, we have a brief look at its proof.
Yablo's Paradox Revisited
Paulo Santos (FCT NOVA, University of Tübingen)
Stephen Yablo proposed a paradox which, according to his evaluation, does not depend on self-reference. In this talk, we render Yablo’s paradox, first, by the use of an order relation, showing that it does not rely on arithmetic. Secondly, we formalise it in Linear Temporal Logic and in Modal Logic. These formalisations uncover the underlying logical structure of Yablo’s paradox.
Paulo Santos (FCT NOVA, University of Tübingen)
We will present a numeral completeness result that holds for weak theories of arithmetic; more precisely, we are going to prove that, starting from a true sentence, one can express the fact that the sentence is true inside the weak theory using numerals. As an immediate consequence, we will obtain a numeral form of provable consistency. The third main result that we will present shows that there is a primitive recursive function (we will see that this function can also be Kalmar elementary) that outputs, for each n, a proof that n is not a proof of a contradiction in a fixed consistent theory. We will relate our result with late versions of Hilbert's Program.
Characterising Probabilistic Termination
Simona Ronchi della Rocca (University of Turin):
In the probabilistic setting, termination has a double nature. Namely we speak about Almost Sure Termination (AST) in case the probability of divergence is null, and about Positive Almost Sure Termination (PAST) if the time to termination is finite. PAST implies AST but not viceversa. A powerful tool for proving program termination are intersection type assignment systems, which have been successfully applied to various kind of deterministic calculi. Here I will show how they can be tailored in order to be applied to the probabilistic case: a unique type assignment system, where the intersection is non idempotent, gives a complete characterisation of both kinds of termination. More specifically, any type derivation for a given term M supplies both a lower bound to the expected time to termination for M, and a lower bound to M’s probability of termination. The system is designed for a call-by-value lambda-calculus, enriched with a probabilistic choice, but all the results are robust and hold for the call-by-name calculus too.
Linear Two-Sorted Constructive Arithmetic
Helmut Schwichtenberg (LMU Munich)
We consider a term system in the style of Goedel's system T together with a computation model that allows to faithfully represent
polynomial-time algorithms. To this end we follow a tradition initiated by Simmons (1988) and developed by Bellantoni and Cook (1992), where two sorts of variables are admitted, here called output and input variables. The idea is that input variables are the general ones which may be recursed on and used many times, whereas output variables cannot be recursed on and can be used only once. These ideas have been extended to a higher type setting and hence – via the Curry-Howardcorrespondence – to a linear two-sorted arithmetical system in the style of Heyting arithmetic in all finite types. Here we further extend this setup with the aim to also include certain nonlinear algorithms (like treesort), given by constants defined by equations involving multiple recursive calls.
A Note on Generalized Algebraic Theories and Categories with Families
Peter Dybjer (University of Gothenburg):
We give a new syntax independent definition of the notion of a finitely presented generalized algebraic theory as an initial object in a category of categories with families (cwfs) with extra structure. To this end we define inductively how to build a valid signature Σ for a generalized algebraic theory and the associated category CwF_Σ of cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notions of uniform family of contexts, types, and terms. Furthermore, we show how to syntactically construct initial cwfs with Σ-structures. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of dependent type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual categories with families.
This is joint work with Marc Bezem, Thierry Coquand, and Martin Escardo.
The conference is organised by:
- Carl Friedrich von Weizsäcker Center
- Kurt Gödel Society
- the ERC-funded project Gödel Enigma: Rediscovering Kurt Gödel through his unpublished works, headed by Jan von Plato
Matthias Baaz, Reinhard Kahle, Thomas Piecha, Jan von Plato