Séminaire

Séminaire Philmath

Séance en l'honneur de F. Pataut.

Nous aurons le plaisir d'accueillir Mariana Girlando, Université d'Amsterdam et Carlo Nicolai, King's College London.

Le séminaire se déroulera en deux temps :

- 11h : Marianna Girlando (ILLC, Amsterdam).

Title : Decision procedures and proof theory: the case of intuitionistic K

Abstract :
A decision procedure for a logic is an algorithm establishing whether a formula is valid or not in the logic. Proof systems, and in particular sequent calculus, can be used to define such procedures, by implementing finitary proof search for formulas. If a proof is found the formula is valid. Otherwise, one can usually construct a countermodel for the formula at the root from a finite branch of a failed proof search tree.

In this talk we consider intuitionistic modal logic IK. This logic is the intuitionistic variant of modal logic K proposed by Fisher Servi, Plotkin and Stirling, and studied by Simpson. Semantically, the logic is characterised by bi-relational frames, comprising a preorder relation, as in intuitionistic possible-worlds models, and a binary relation, representing the modal accessibility relation.

There is no known sequent calculus proof system for IK. Instead, we shall present proof systems for IK defined by enriching the sequent calculus formalism: a fully labelled sequent calculus, explicitly representing the two relations of IK-models, and a bi-nested calculus, having one syntactic connective for each relation. Both proof systems give rise to decision procedures for logic IK, which we shall briefly describe and compare.

This talk is based joint work with:
- Roman Kuznets, Sonia Marin, Marianela Morales, and Lutz Straßburger: https://inria.hal.science/hal-04569308v1
- Han Gao and Nicola Olivetti (work in progress)

- 15H : Carlo Nicolai (King's College London).

Title : Determinate Truths

Abstract :

I present some observations on the theory of classical determinate truth recently introduced by Fujimoto and Halbach (CD+). The observations aim to show that there is a precise sense in which the primitive determinate predicate of CD+ could be dispensed with without compromising the logical strength and motivation of the theory. In particular, there's a precise sense in which the axioms of CD+ are a notational variant of the classical closure of Kripke-Feferman truth. This is joint work with Luca Castaldo.