Séminaire Philmath du 24 juin 2024

La prochaine séance du séminaire PHILMATHse tiendra le lundi 24 juin 2024, Salle de conférences, de 11hà 17h à l’IHPST : Université Paris 1 Panthéon-Sorbonne, Maison de la Philosophie – Marin Mersenne, 13 rue du Four, 2ème étage (salle de conférence), 75006 Paris.

Séminaire en l’honneur de Fabrice Pataut.

Exceptionnellement la séance se déroulera en deux temps : 

Nous aurons le plaisir d’accueillir : 

–  11h00  – Marianna Girlando (Université d’Amsterdam)

Titre : 

Decision procedures and proof theory: the case of intuitionistic K

Résumé : 

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 the 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)

– 15h00 – Carlo Nicolai (King’s College London)

Titre : 

Determinate Truths

Résumé : 

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 thereby 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.

Lien zoom :

https://pantheonsorbonne.zoom.us/j/97024277517?pwd=eGwyYW9sZVpzdldzZVRaZEs5eVY5Zz09

ID réunion : 970 2427 7517

Code d’accès : 549311

Un pot suivra les deux séances. Nous espérons vous voir nombreuses et nombreux. 

Organisation : 

Francesca Poggiolesi (IHPST)

Fabrice Pataut (SND)