Explicit Proofs in Formal Provability Logic

2007 ◽  
pp. 241-253
Author(s):  
Evan Goris
Keyword(s):  
Provability Logic

scholarly journals The omega-rule interpretation of transfinite provability logic

2018 ◽  
Vol 169 (4) ◽  
pp. 333-371
Author(s):  
David Fernández-Duque ◽  
Joost J. Joosten
Keyword(s):  
Provability Logic

scholarly journals A Finitary Treatment of the Closed Fragment of Japaridze's Provability Logic

2005 ◽  
Vol 15 (4) ◽  
pp. 447-463 ◽  
Author(s):  
Lev D. Beklemishev ◽  
Joost J. Joosten ◽  
Marco Vervoort
Keyword(s):  
Provability Logic

scholarly journals On propositional quantifiers in provability logic.

1993 ◽  
Vol 34 (3) ◽  
pp. 401-419 ◽  
Author(s):  
Sergei N. Artemov ◽  
Lev D. Beklemishev
Keyword(s):  
Provability Logic ◽  
Propositional Quantifiers

PROVABILITY LOGICS RELATIVE TO A FIXED EXTENSION OF PEANO ARITHMETIC

2018 ◽  
Vol 83 (3) ◽  
pp. 1229-1246
Author(s):  
TAISHI KURAHASHI
Keyword(s):  
Peano Arithmetic ◽  
Provability Logic ◽  
Consistent Extension ◽  
Image Position ◽  
Computably Enumerable

AbstractLet T and U be any consistent theories of arithmetic. If T is computably enumerable, then the provability predicate $P{r_\tau }\left( x \right)$ of T is naturally obtained from each ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of T. The provability logic $P{L_\tau }\left( U \right)$ of τ relative to U is the set of all modal formulas which are provable in U under all arithmetical interpretations where □ is interpreted by $P{r_\tau }\left( x \right)$. It was proved by Beklemishev based on the previous studies by Artemov, Visser, and Japaridze that every $P{L_\tau }\left( U \right)$ coincides with one of the logics $G{L_\alpha }$, ${D_\beta }$, ${S_\beta }$, and $GL_\beta ^ -$, where α and β are subsets of ω and β is cofinite.We prove that if U is a computably enumerable consistent extension of Peano Arithmetic and L is one of $G{L_\alpha }$, ${D_\beta }$, ${S_\beta }$, and $GL_\beta ^ -$, where α is computably enumerable and β is cofinite, then there exists a ${{\rm{\Sigma }}_1}$ definition $\tau \left( v \right)$ of some extension of $I{{\rm{\Sigma }}_1}$ such that $P{L_\tau }\left( U \right)$ is exactly L.

A realization theorem for the Gödel-Löb provability logic

2016 ◽  
Vol 207 (9) ◽  
pp. 1344-1360 ◽  
Author(s):  
D S Shamkanov
Keyword(s):  
Provability Logic
Sign in / Sign up

Export Citation Format

Share Document