English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Propositional modal provability logics like  G  and  Grz  have arithmetical interpretations where □φ can be read as ‘formula φ is provable in Peano Arithmetic’. These logics are decidable but are characterized by classes of Kripke frames which are not first‐order definable. By abstracting the aspects common to their characteristic axioms we define the notion of a formula generation map  F(P)  in one propositional variable. We then focus our attention on the properly displayable subset of all (first‐order definable) Sahlqvist modal logics. For any logic  L  from this subset, we consider the (provability) logic  LF  obtained by the addition of an axiom based upon a formula generation map  F(P)  so that  LF = L  +  F(P) . The class of such logics includes  G  and  Grz . By appropriately modifying the right introduction rules for □, we give (not necessarily cut‐free) display calculi for every such logic. We define the pseudo‐displayable subset of these logics as those whose display calculi enjoy cut‐elimination for sequents of the form ⊤ ⊢ φ for any formula φ. We then show that for any provability logic  LF  having a conservative tense extension, there is a map   f   on formulae such that  LF  is pseudo‐displayable if and only if   f   maps theorems of  LF  to theorems of the underlying logic  L  and vice versa. By using a standard renaming technique we can guarantee that there is a polynomial‐time translation from  LF  into  L . All proofs are purely syntactic and show the versatility of display calculi since similar results using traditional Gentzen calculi are not possible for as broad a range of logics and require further conditions. Our maps generalize previously known maps from  G  into  K4 . An application of our results gives an   O   ( n.log n ) 3 )  translation from the (‘second order’) provability logic  Grz  into a decidable subset of first‐order logic. Since each of our logics  L  is a Sahlqvist logic, it is first‐order definable, and hence each  L  has a translation into first‐order logic. Our results therefore show that all pseudo‐displayable logics  LF  are ‘essentially first‐order’ even though their characteristic axiom may not be first‐order definable.

Theoremhood‐preserving Maps Characterizing Cut Elimination for Modal Provability Logics