Remembering Thomas Strahm

Gerhard Jäger (University of Bern):

A brief overview of Thomas Strahm’s scientific activities and the impact of his work will be given.

Formalising the extended predicative Mahlo universe in the context of Martin-Löf Type Theory

Anton Setzer (Swansea University):

In previous talk (joint work with Reinhard Kahle) we have presented the extended predicative Mahlo universe, which allows to give a more predicative formalisation of the Mahlo universe in the setting of Feferman's system of Explicit Mathematics.

In this talk we formalise explicit mathematics using Martin-Löf extended by inductive recursive definitions. We formulate the construction in the theorem prover Agda based on Martin-Löf Type Theory. The formalisation is slightly adapted to be in accordance with the setting of Martin-Löf Type Theory. We will see that this formalisation doesn't entirely remove the underlying problem, for the formalisation of the extended predicative Mahlo universe itself we need non strictly positive inductive definitions. This is to be expected since when iterating this construction, which is possible, we would go beyond the strength inductive-recursive definitions.

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.

On the performance of axiom systems.

Set universes

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 ε₀. 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 ε₀ 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.

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.

Harvey Friedman (Ohio State University)

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.

Incompleteness in Type Theory

Thorsten Altenkirch (University of Nottingham):

I am discussing the issue of Leibniz incompleteness in Type Theory: we have two objects that satisfy the same properties, i.e. are indistinguishable but which cannot be shown to be equal. For example in Intensional Type Theory, extensionally equal functions cannot shown to be equal but they also cannot be distinguished. A more interesting example is the fact that isomorphic types cannot be distinguished but also cannot be shown equal (this also applies to Extensional Type Theory). The latter can be addressed by Voevodsky's univalence principle. This raises the question wether HoTT is Leibniz complete.

Levels of abstraction when defining type theory in type theory

Ambrus Kaposi (Eötvös-Loránd-University):

There are multiple levels of abstraction in which one can encode the syntax of type theory inside type theory. These include Gödel numbers, lists of lexical elements, abstract syntax trees, well-scoped syntax trees, well-typed syntax trees, well-typed syntax trees quotiented by the conversion relation, higher order abstract syntax. In this talk I will present these encodings, discuss their relationships, discuss which properties of the syntax can be proven at which level, and explain what features of type theory are needed to use them.

Type Theory in Set Theory, in Type Theory

Bruno Barras (Laboratoire Spécification et Vérification):

This talk is about encoding Type Theory in Type Theory via a translation to Set Theory. This breaks embeddings of Type Theory in itself in two steps: (1) a set-theoretical model of Type Theory, and (2) a representation of sets in Type Theory.  Those mutual encodings gives results on the relative strength of type and set theories.

We first recall previous works, such as Aczel's Constructive Zermelo Frankel (CZF) that corresponds to predicative type theories.  Werner has shown that ZFC (Zermelo Fraenkel with Choice) plus a hierarchy of inaccessible cardinals corresponds to the Calculus of Inductive Constructions (CIC) extended with 2 axioms.

The goal of our work is to find a restriction of intuitionistic ZF (IZF) such that we have a correspondence with impredicative type theories like CIC. For this purpose, we introduce IZF with functional replacement and well-founded recursion as a good candidate, and we discuss the issues related to the correspondence between type-theoretic universes and set-theoretical Grothendieck universes (or inaccessible cardinals).

Comparing general definitions of type theories

Peter LeFanu Lumsdaine (Stockholm University):

In recent years, several authors have introduced quite general definitions of dependent type theories.  A major goal is to allow a more unified study of type theories and their models, with theorems and constructions proven in a precise and broad generality, instead of (as currently) given for specific individual type theories and adapted to others as needed.

- Uemura (arXiv:1904.04097) gives an abstract categorical definition, *categories with representable maps*, together with a syntactic definition based on logical frameworks.

- Bauer–Haselwarter–Lumsdaine (arXiv:2009.05539) give a concrete syntactic definition, not LF-based (using Fiore-Plutkin-Turi or similar syntax with binding), and have also formalised this definition in Coq.  A similar definition was independently given by Brunerie (unpublished).

- Isaev (arXiv:1602.08504) gives an essentially-algebraic definition

I will concisely present these definitions, and survey the connections between them.

Video of the talk

Internal Models of Type Theory

Thierry Coquand (University of Gothenburg):

The notion of definitional equality plays an important role in the formulation of dependent type theory. This makes it difficult to build models (e.g. Kleisli models) of type theory in an intensional framework, where one would like to see the model construction as a purely syntactical transformation of the type systems into itself. 
In the past 10 years however, several internal models have been built, such as the parametricity and exception models. 
Some class of nominal/presheaf models, where restriction maps are substitutions, also preserve the intensional character of type theory, and I will explain how this internal model technique can be used to build various models of univalence in an intensional and constructive setting.

Video of the talk

Ulrich Berger (Swansea University): From Brouwer's Thesis to the Fan Functional

Video of the talk

From Gödel's incompleteness theorems and foundational reductions to applications in core mathematics

Ulrich Kohlenbach (TU Darmstadt):

Gödel's 2^nd incompleteness theorem established that Hilbert's program to prove the consistency of arithmetic, analysis and even set theory by finitistic means, cannot be carried out globally. However, Gödel himself achieved important foundational reductions to reduce e.g. the consistency of classical number theory to that of intuitionistic number theory (Gödel 1933) and of the latter to that of a quantifier-free calculus of primitive recursive functionals of finite types which had been first defined by Hilbert in 1926 (Gödel 1941,1958). 

These foundational reductions have (with many subsequent extensions and adaptations) been used during the last two decades in the systematic program of 'proof mining', i.e. the extraction of new effective data such as bounds from prima facie noneffective proofs, in a number of areas of core mathematics. Extended case studies have revealed that whole areas of e.g. nonlinear analysis are largely based on proofs which actually do have a computational content of low and (with very few exceptions) at most primitive recursive complexity. This shows that locally large parts of ordinary mathematics in fact do allow for a 'finitization' as Hilbert had envisaged.

We will sketch some of the reasons for this proof-theoretic tameness often observed in ordinary mathematics and present recent - essentially polynomial - rates of convergence extracted from proofs in geodesic geometry and nonsmooth optimization respectively.

Video of the talk

Spectra and radicals

Daniel Wessel (LMU Munich):

Radical theory offers rich tools to encode properties of rings and their modules through suitable classes of ideal objects. By analogy, we discuss spectra that arise from non-deterministic axioms over complete lattices, and break down the corresponding radicals into their constituent parts. The intention is twofold: complement the approach taken in dynamical algebra, and contribute to a revised Hilbert programme.

This talk is partly based on joint work with Peter Schuster.

Paul Lorenzen's reception of Gödel's incompleteness theorems

Stefan Neuwirth (Université de Franche-Comté):

Video of the talk

Proof Analysis with CERES

Anela Lolic (TU Wien)

The method CERES is an efficient cut-elimination method based on resolution and has beendefined for various proof calculi. The original method was constructed for classical first-order logic, and the result of CERES (a proof in atomic cut normalform) was used for proof analysis by the extraction of variations of Herbrand's theorem.

The method CERES has been extended to several logics, and the proof analysis methods have been considerably simplified by extracting the Herbrand information from proofs that are not in normalform. In fact, it was shown that the Herbrand information can be obtained from the cut-free parts of a proof, which are represented by the so-called projections in the CERES method.

The most recent development was the extension of the methods to classical first-order logic with induction. Using the proof analysis methods for CERES it was possible to define a structure representing a variant of Herbrand's theorem.

Video of the talk

The Number of Axioms

Jan Bydzovsky (TU Wien)

Following Goedel's incompleteness theorem no recursive notion of a proof can be efficient enough to ensure that every provable first-order formula A is also provable by a proof its length is recursively bounded in the number of symbols in A. However, this does not directly give much inside into the structure of long proofs when a particular proof system is fixed. I will comment on a new result together with Juan P. Aguilera and Matthias Baaz that for cut-free sequent calculus one of the sources of hardness to prove a formula is the number of (instances) of the axioms one needs to use. I will also comment on what the situation is for sequent proofs with cuts and sequent proofs from theories like Robinson arithmetic, PA or ZFC.

The landscape of Gödel's incompleteness theorems

Yong Cheng (Wuhan University)

Presentation Slides

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 
theorem (G2).

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.

Video of the talk

References:
Yong Cheng, Incompleteness for Higher-Order Arithmetic: An Example Based on 
Harrington's Principle, Springer series: Springerbrief in Mathematics, 
Springer, 2019.

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.

Generalization of arithmetical proofs

Lorenzo Sauras (TU Wien): 

In this talk, I will explain how to apply Baaz’s generalization method to proofs of universal sentences from elementary number theory. This procedure has resulted to have a considerable potential in revealing arithmetical patterns, that got reflected in theorems (for example, sufficient conditions for a value to be a divisor of an arbitrary Fermat number) and conjectures (mainly about integer sequences).

Video of the talk

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.

Video of the talk

On the second incompleteness theorem and provability predicates

Taishi Kurahashi (Kobe University)

Gödel's second incompleteness theorem states that every consistent computably axiomatized theory containing Peano Arithmetic cannot prove a sentence claiming the consistency of the theory. This statement is of course ambiguous in that it does not specify what a sentence claiming the consistency of a theory is. In this talk, we investigate relationships between several versions of the second incompleteness theorem and the derivability conditions for provability predicates.

The Formalized Consistency Statement Revisited

Reinhard Kahle (University of Tübingen)

We discuss the limitations of the standard formalization of consistency (of a theory T) when it is supposed to express the consistency of T.

Video of the talk

Numeral Completeness

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.

Video of the talk

Missing Proofs and the Provability of Consistency

Sergei Artemov (Graduate Center, CUNY):

We argue that there is a class of widely used and readily formalizable arithmetical proofs of universal properties which are not accounted for in the traditional unprovability of consistency analysis.
On this basis, we offer a mathematical proof of consistency for Peano Arithmetic PA and demonstrate that this proof is formalizable in PA. This refutes the wide spread belief that there exists no consistency proof of a system that can be formalized in the system itself. Gödel’s Second Incompleteness theorem yields that PA cannot derive the consistency formula ConPA. This does not interfere with our formalized proof of PA-consistency which is not a derivation of the consistency formula ConPA.

 Slides

Video of the talk

The Diagonalization Lemma — Demystified Hopefully

Saeed Salehi (University of Tabriz): 

Slides

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.

Video of the talk


References

·       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).
 

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.

Video of the talk

What Replaces Diagonalisation in Boolos’ Proof of the First Incompleteness Theorem?

Helen Preiß (Technical University of Darmstadt):

In a short note, Boolos sketched a proof of Gödel's First Incompleteness Theorem based on Berry's Paradox. He distinguishes his argumentation from Gödel's as it "does not involve diagonalization". In this talk we discuss the replacement for diagonalization Boolos is using.

Video of the talk

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.

Video of the talk
 

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. 

Video of the talk

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.

Video of the talk

Recurrence without structuralism, and the delineation of finitism and feasibility

Daniel Leivant (Indiana University Bloomington):

Primitive recursion is umbilically related to actual infinite totalities, viz the functions being defined. Yet Tait's Thesis (1981) identifies finitism with primitive-recursive mathematics.  We start by showing that this conflict is a non-issue, by defining a generic formal theory for finite data, with a companion imperative programming language, free of implicit assumptions about actual infinities, yielding fresh strong arguments in support of Tait's Thesis.

We further refine our programming language with a ramification discipline, obtaining algorithmically broad imperative programming languages for PTime and PSpace, depending on the strictness of the ramification condition.

Video of the talk

Gödel and the Lengths of Proofs

Sam Buss (University of California, San Diego):

The lengths of proofs and the complexity of proofs are of great interest due to its connections to complexity theory and theorem proving. Gödel was the first one to consider lengths of proofs. This talk will discuss three results in lengths of proofs related to Gödel's writings. The first is upper and lower bounds on the lengths of partial consistency statements (due to P. Pudlak and H. Friedman). The second is Gödel's separation of higher order theories of arithmetic. The third is a claim made by Gödel in a letter to von Neumann related to the question of whether P=NP.

Video of the talk

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.

Video of the talk

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.

Video of the talk

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.
Video of the talk

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.

Video of the talk

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.  

Video of the talk

Gödel’s functional interpretation in context

Maria Hämeen-Ant­tila (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.

Video of the talk

Gödel's first steps in logic: From Carnap's axiomatic exercises to incompleteness

Jan von Plato (University of Helsinki)

Recent findings in the Gödel papers show that his active involvement with logical questions began with Carnap's "Axiomatics exercises" in the summer of 1928, with formalizations of second-order arithmetic, Hilbert's geometry, and point set topology. These show already the effect of Hilbert-Ackermann's book, from which he then found the completeness problem, solved by the end of January 1929. The extension of completeness to higher-order logic failed but led instead, from early summer 1930 to November, to the now famous incompleteness article published 90 years ago.

Video of the talk