2019/11/11 by Mojtaba Mojtahedi, Mojtahedi, Mojtaba · 1 citation
Computer Science · #semigroups and automata theory #Cryptography and Data Security #Formal Methods in Verification
paper · pdf · doi:10.48550/arxiv.1911.04284
Let PL(\sf T,\sf T') and PLΣ1(\sf T,\sf T') respectively indicates the provability logic and Σ1-provability logic of \sf T relative in \sf T'. In this paper we characterize the following relative provability logics: PLΣ1(\sf HA,ℕ), PLΣ1(\sf HA,\sf PA), PLΣ1(\sf HA^*,ℕ), PLΣ1(\sf HA^*,\sf PA), PL(\sf PA,\sf HA), PLΣ1(\sf PA,\sf HA), PL(\sf PA^*,\sf HA), PLΣ1(\sf PA^*,\sf HA), PL(\sf PA^*,\sf PA), PLΣ1(\sf PA^*,\sf PA), PL(\sf PA^*,ℕ), PLΣ1(\sf PA^*,ℕ) (see Table \refTable-Theories). It turns out that all of these provability logics are decidable. The notion of \em reduction for provability logics, first informally considered in \citereduction. In this paper, we formalize a generalization of this notion (\CrefDefinition-Reduction-PL) and provide several reductions of provability logics (See diagram \refDiagram-full). The interesting fact is that PLΣ1(\sf HA,ℕ) is the hardest provability logic: the arithmetical completenesses of all provability logics listed above, as well as well-known provability logics like PL(\sf PA,\sf PA), PL(\sf PA,ℕ), PLΣ1(\sf PA,\sf PA), PLΣ1(\sf PA,ℕ) and PLΣ1(\sf HA,\sf HA) are all propositionally reducible to the arithmetical completeness of PLΣ1(\sf HA,ℕ).