LUW October 6 : being provable in Peano Arithmetic with at most k steps

[jean-yves beziau]

This coming Wednesday, October 6, at 4 pm CET,  one more session of the Logica Universalis Webinar (LUW).

See details below. Everybody is welcome to join !

Register in advance here:

https://www.springer.com/journal/11787/updates/18988758

Jean-Yves Beziau

Organizer of LUW and President of 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.