Ce mercredi 6 octobre à 16 h, une mouvelle séance du Webinaire Logica Universalis (LUW). Voir les détails ci-dessous. Tout le monde est le bienvenu ! Inscrivez-vous à l’avance ici : https://www.springer.com/journal/11787/updates/18988758 Jean-Yves Beziau Organisateur du LUW et Président de la LUA http://www.logica-universalis.org/LUAD >------------------------------------------------------------------------------------------------------------------------------------------------------------ Paulo Guilherme Santos & Reinhard Kahle NOVA School of Science and Technology, Caparica, Portugal and University of Tübingen, Germany "k-Provability in PA" Logica Universalis, On-line first June 09, 2021 https://link.springer.com/article/10.1007/s11787-021-00278-1
We study the decidability of k-provability in PA—the relation ‘being provable in PA with at most k steps’—and the decidability of the proof-skeleton problem—the problem of deciding if a given formula has a proof that has a given skeleton (the list of axioms and rules that were used). The decidability of k-provability for the usual Hilbert-style formalisation of PA is still an open problem, but it is known that the proof-skeleton problem is undecidable for that theory. Using new methods, we present a characterisation of some numbers k for which k-provability is decidable, and we present a characterisation of some proof-skeletons for which one can decide whether a formula has a proof whose skeleton is the considered one. These characterisations are natural and parameterised by unification algorithms. -- https://www.vidal-rosset.net/mailing_list_educasupphilo.html
