k-Provability in PA

Research output: Contribution to journalArticlepeer-review

1 Downloads (Pure)

Abstract

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.

Original languageEnglish
JournalLogica Universalis
DOIs
Publication statusAccepted/In press - Jun 2021

Keywords

  • Decidability
  • k-provability
  • Peano arithmetic
  • Proof-skeleton problem

Fingerprint

Dive into the research topics of 'k-Provability in PA'. Together they form a unique fingerprint.

Cite this