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. -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAF2zFLDkmBFXy3Mz%3DcDjMtxMsUEJb4h9rSjzbD__%2BFaogwsENA%40mail.gmail.com.
