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

jean-yves beziau beziau100 at
Mon Oct 4 19:12:51 EDT 2021

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:
Jean-Yves Beziau
Organizer of LUW and President of LUA
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

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211004/9d619673/attachment-0001.html>

More information about the FOM mailing list