Fifth New College Logic Meeting

Syntax, Coding, and Incompleteness

19 and 20 September, 2023

Map of New College with directions for workshop venues

In logic we make claims about expressions in languages. In particular, we make claims about sentences and formulae, and say that they are provable, true, tautological, refutable, and so on. Even if the languages considered themselves are formal, the reasoning about the expressions in the languages and their properties are often informal. Tarski, Gödel, and others devised precise theories of syntax. Gödel showed how arithmetical theories can be used to prove syntactic claim indirectly by coding syntax in the natural numbers. This observation is at the basis of his famous incompleteness theorems. Of course, there are many different ways to code formulae of a countable language in the natural numbers, and different choices may lead to different results.

Sophisticated codings may be chosen. For instance, Visser defined codings with built-in diagonalization: For any formula A(x) there is a number n such that n is the code of A(n) where n is the numeral of the code of n. With such a coding there is no need to prove Gödel's diagonal lemma, because it is trivially given by the coding.

Others have tried to eliminate coding completely by working in a theory of syntax that is intended to make claims directly about syntactic objects, not via some coding.

In the workshop we look at the consequences of the different ways to code syntax and of reasoning about syntax on the incompleteness and related results, but also in the theory of truth and the paradoxes.

Speakers

Yong Cheng (Wuhan)

Balthasar Grabmayr (Tübingen)

Daniel Isaacson (Oxford)

Graham Leigh (Gothenburg)

Beau Mount (Oxford)

Carlo Nicolai (KCL)

Karl-Georg Niebergall (Berlin)

Fedor Pakhomov (Ghent, Moscow)

Albert Visser (Utrecht)

Lingyuan Ye (Amsterdam)

Tuesday 19 September 2023

Wednesday 20 September 2023

Venue: New College, Oxford, Noel Salter room (Lecture Room 4)

Everybody is invited to attend. We ask you to send an email to Lingyuan Ye at ye.lingyuan.ac at gmail.com or to Balthasar Grabmayr at balthasar.grabmayr at gmx.net if you intend to come, so we have an idea about the size of the audience.

We thank the New College Ludwig Fund for Humanities Research and the Faculty of Philosophy for the generous support of the workshop.

Abstracts

Dan Isaacson: Sentences in the language of arithmetic that can only be understood or proved in terms of coding 

Fedor Pakhomov: Second incompleteness theorem and formal theory of syntax

In this talk I'll present my old and unpublished result that Gödel's 2-nd incompleteness holds for any classical first-order theory of finite signature and provability predicate satisfying Hilbert-Bernays-Löb derivability conditions provided that the theory represents its own syntax in the following way. Given a finite signature O we could naturally identify its syntax with the absolutely free 3-sorted algebra Syn(O) consisting of a sort of for variables, a sort for terms, a sort for formulas, and the operations corresponding to Boolean connectives, quantifiers, applications of functional symbols to terms, etc. (or if the original signature was n-sorted, then the algebra would be (2n+1)-sorted). We identify representations of syntax with the interpretations of the atomic diagram of Syn(O).  

Albert Visser: Clash of the Titans: Markov versus Smullyan

What is a good Gödel numbering? This question has technical, didactical, and philosophical aspects.

In my talk, I zoom in on two concrete initial steps towards Gödel numberings, one due Andrey Markov (in 1954) based on \mathsf{SL}|_2(\mathbb N) and one due to Raymond Smullyan (in 1961) based on the length-first ordering. I will present these initial steps towards Gödel numberings in some detail and will discuss possible follow-up steps to obtain full Gödel numberings. Then, I use these two examples as illustration of various technical, didactical and philosophical issues. 

Lingyuan Ye: Diagonalisation and Well-founded Naming  

We investigate the conditions under which diagonal sentences can be taken to constitute paradigmatic cases of self-reference. We put forward well-motivated constraints on the diagonal operator and the coding apparatus which separate paradigmatic self-referential sentences, for instance obtained via Gödel’s diagonalization method, from accidental diagonal sentences. In particular, we show that these constraints successfully exclude refutable Henkin sentences, as constructed by Kreisel. 

Graham Leigh: A Compositional Theory of Falsity (joint work with Daichi Hayashi)

Compositional theories of truth tend to follow the Tarskian tradition, either the model-theoretic semantics for classical predicate logic or its natural generalisations to many-value and possible-worlds. Other realisations of truth, which includes computational interpretations and game semantics, have been largely ignored by truth theorists. In this talk I will present axiomatic rendering of Krivine’s “classical realisability”, a ‘truth as programs’ semantics for classical logic that validates extensions of Peano arithmetic. What sets this conception of truth apart from the Tarskian view is its treatment of falsity as primitive and truth as a derived notion.

Yong Cheng: The effect of numbering on incompleteness: logical incompleteness versus concrete incompleteness 

We first discuss the question `What is a good numbering' with respect to a test theorem (the incompleteness theorems G1 and G2) and examine the effect of numbering on G1 and G2. In the second part, we compare the role of coding in logical incompleteness and concrete incompleteness, and focus on the similarities and differences between logical incompleteness and concrete incompleteness based on technical evidences and philosophical reflections.  

Balthasar Grabmayr: Fixing Montague's Problem

Turing machines only operate directly on strings. Turing computation over any other domain therefore requires a notation system for the domain. Ever since Montague's (1960) observation that different notation systems in general yield different notions of Turing computability, the task of distinguishing those notation systems that are admissible for computation from those that are not continues to be an open problem in the philosophy of computation. In the first part of this talk, I will introduce a generalised version of Montague's problem. In the second part, I will formulate and defend a solution to this problem.  

Karl-Georg Niebergall: On a theory equivalent to PA and Z_2

I present a theory T which is equivalent to PA and equivalent to Z_2 (i.e. 2nd order number theory): Z_2 is „relatively interpretable“ in T, T is conservative over PA. T was not invented for this task; it was just there. I consider several applications of this example.  

Carlo Nicolai: Base Theories, Object Theories, Syntax Theories

When constructing formal theories of truth, falsity, validity, invalidity, (predicate-like, de dicto) modalities it's useful to take sentence types as the objects to which these notions apply. The talk discusses a number of questions arising from the choice of an optimal theory of sentence types in this context. I will first discuss the subtle distinction between object theories, base theories, and syntax theories, and what this distinction entails. I then move to the question of how to make philosophical and technical sense of the familiar claims that theories of finite sets, arithmetic, and concatenation are equally good theories of the object of truth, and that concatenation theories are "direct" axiomatizations of syntax. An important part of the discussion is whether adequate theories of the objects of truth should feature restricted non-logical schemata. The talk reports on a chapter of a book manuscript on recent research on formal theories of truth. 

Beau Mount: Stable and Unstable Theories of Truth and Syntax (joint work with Daniel Waxman) 

Recent work on formal theories of truth has revived an approach, due originally to Tarski, on which syntax and truth theories are sharply distinguished—‘disentangled’—from mathematical base theories. In this paper, we defend a novel philosophical constraint on disentangled theories. We argue that these theories must be epistemically stable: they must possess an intrinsic motivation justifying no strictly stronger theory. In a disentangled setting, even if the base and the syntax theory are individually stable, they may be jointly unstable. We contend that this flaw afflicts many proposals discussed in the literature; we defend a new, stable disentangled theory, double second-order arithmetic.