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

[FRANCISCO MARIANO]

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<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.springer.com%2Fjournal%2F11787%2Fupdates%2F18988758&data=04%7C01%7Cassismariano%40mail.missouri.edu%7C560137a9abf1450fc5fa08d9892b2b10%7Ce3fefdbef7e9401ba51a355e01b05a89%7C0%7C0%7C637691640766311289%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=QRUMewddSC%2F1QZuLVytjoCdoFRunCmm0n9XlzuepF8k%3D&reserved=0>
Jean-Yves Beziau
Organizer of LUW and President of LUA
http://www.logica-universalis.org/LUAD<https://nam02.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.logica-universalis.org%2FLUAD&data=04%7C01%7Cassismariano%40mail.missouri.edu%7C560137a9abf1450fc5fa08d9892b2b10%7Ce3fefdbef7e9401ba51a355e01b05a89%7C0%7C0%7C637691640766311289%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=KGxKU41gMFCFDysHNuvP3ZZDd844ayNKK6cUHgVUYi0%3D&reserved=0>
>------------------------------------------------------------------------------------------------------------------------------------------------------------
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<https://nam02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flink.springer.com%2Farticle%2F10.1007%2Fs11787-021-00278-1&data=04%7C01%7Cassismariano%40mail.missouri.edu%7C560137a9abf1450fc5fa08d9892b2b10%7Ce3fefdbef7e9401ba51a355e01b05a89%7C0%7C0%7C637691640766321285%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=1o9BMXRGnqkS9XhcNVy8E1u4Uhd1jQvlT%2F9lW%2FU7zk4%3D&reserved=0>

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/20211007/0ea6d370/attachment-0001.html>