Workshop om formella sanningsteorier samlade logikforskare

Torsdagen den 6 december gästades Göteborgs universitet av forskare i logik som deltog i en workshop om formella sanningsteorier – Gothenburg-Warsaw workshop on truth.

Forskningsprojektet Reflection and Truth, vid institutionen för filosofi, lingvistik och vetenskapsteori, var värd för workshopen som har organiserats av forskarna Graham Leigh och Ali Enayat.

Forskare från Warsawa och Göteborg föreläste växelvis och här är sammanfattningar av några av dagens föredrag:

Constructive truth

Mattias Olsson (Gothenburg)
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.

Satisfaction classes via cut elimination

Cezary Cieśliński (Warsaw)
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.

FS & co-Nec

Anton Broberg (Gothenburg)
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.

Finite axiomatizability via the compositional truth predicate

Mateusz Łełyk (Warsaw) 
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.

Här finns hela föreläsningsprogrammet

Läs mer om forskningsprojektet Reflection and Truth.

Graham Leigh presenterar Cezary Cieśliński från Warsawa. Foto: Monica Havström