The Gothenburg–Warsaw workshop on truth was held on Thursday, 6 December 2018 at the Department of Philosophy, Linguistics and Theory of Science at the University of Gothenburg. See below for the schedule.
The meeting was sponsored by the research project Reflection and Truth funded by the Knut och Alice Wallenberg Stiftelse and the University of Gothenburg.
Organisers: Graham Leigh and Ali Enayat.
The morning session will take place in room H821 of Humanisten (main building of the Humanities) nearby the department. The room can be hard to find, so there will be a group leaving from the main entrance of FLoV at about 10.
In the afternoon the workshop will be in room T307 of FLoV (the usual venue of the logic seminar).
There will be a workshop dinner on Thursday evening. The venue is to be finalised. Please get in touch with one of the organisers if you wish to attend.
In the afternoon of Wednesday 5 December there will be two talks and opportunities for less formal discussions. The first talk will be held in T304; the remainder of the afternoon in room T340 (of FLoV).
Abstracts of the announced talks:
15:15. Ali Enayat (Gothenburg). How far is a truth theory from its base? Abstract. In the first part of the talk, I will review some basic results about conservativity and interpretability of truth theories in relation to their base theory. In the second part, I will report on recent joint work with Mateusz Łełyk and Bartosz Wcisło on feasible proof- theoretic reduction of the following theories to PA: (1) Compositional truth over PA (with no extra induction); (2) Friedman-Sheard truth over PA (with no extra induction); and (3) Kripke-Feferman truth over PA (with no extra induction).
10:15. Bartosz Wcisło (Warsaw).
11:15. Mattias Olsson (Gothenburg). Constructive truth + open discussion Abstract. The result that intuitionistic ID1-hat, and in particular its subtheory intuitionistic KF, is conservative over Heyting arithmetic (HA) has apparently been folklore for some time, though it seems to have been proved only quite recently in a series of papers by Buchholz, Rüede and Strahm, and Arai. After a motivational digression into classical logic we present work in progress on a proposal for a different proof of this result, or a substantial part of it, based on realisability in HA. The idea is to show that every theorem of ID1-hat has a realiser and that realisability is disquotational for certain classes of formulae.
13:15. Cezary Cieśliński (Warsaw). Satisfaction classes via cut elimination Abstract. The objective is to present a fully classical construction of a satisfaction class for the language of first-order arithmetic. In the construction, we will be using cut elimination as the fundamental proof technique. The main challenge is to modify the cut elimination method in such a way that it can be applied to a proof system processing possibly non- standard arithmetical formulas.
14:45. Anton Broberg (Gothenburg). FS & co-Nec Abstract. It is an open question whether the rule CONEC (Co-Necessitaion) is superfluous in Friedman and Sheard’s system FS. We will present a proof-sketch that answer this question positively. First the problem is reduced by showing that we can put some restrictions on the proofs of FS without limiting the strength of FS. Then this reduced problem is shown via ordinal analysis on a system formulated in an infinitary proof calculus. This is joint work with G. Leigh and is very much in progress.
15:45. Mateusz Łełyk (Warsaw). Finite axiomatizability via the compositional truth predicate Abstract. Occasionally in the literature one can find the claim that the easiest way to find a finite axiomatization of an extension Th of PA is to consider CT−(Th) (extension of Th with the Tarski-style compositional axioms for the newly added truth predicate) and add the sentence saying “All axioms of Th are true”. We show that this claim is false as there are very natural arithmetical theories Th for which CT−(Th)+ “All axioms of Th are true.” is non-conservative over Th. Then we show that for every r.e. theory Th there exists a recursive axiomatization A such that CT−(Th)+ “All sentences from A are true.” is conservative over Th. Then we study the question: which theories Th are the arithmetical parts of CT−(PA)+ “All sentences from A are true.”, where A is an axiomatization of PA which is proof-theoretically reducible to (the standard axiomatization of) PA.
17:00. Graham Leigh (Gothenburg). Reflexions on formal truth