Arithmetical completeness theorems for monotonic modal logics

2022/08/06 by Haruka Kogure, Kogure, Haruka, Taishi Kurahashi +1 · 3 citations
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Formal Methods in Verification

paper · pdf · doi:10.48550/arxiv.2208.03555

Abstract

We investigate modal logical aspects of provability predicates Pr_T(x) satisfying the following condition: M: If T \vdash φ→ ψ, then T \vdash Pr_T(\ulcorner φ\urcorner) → Pr_T(\ulcorner ψ\urcorner). We prove the arithmetical completeness theorems for monotonic modal logics MN, MN4, MNP, MNP4, and MND with respect to provability predicates satisfying the condition M. That is, we prove that for each logic L of them, there exists a Σ₁ provability predicate Pr_T(x) satisfying M such that the provability logic of Pr_T(x) is exactly L. In particular, the modal formulas P: ¬ \Box \bot and D: ¬ (\Box A ∧ \Box ¬ A) are not equivalent over non-normal modal logic and correspond to two different formalizations ¬ Pr_T(\ulcorner 0=1 \urcorner) and ¬ (Pr_T(\ulcorner φ\urcorner) ∧ Pr_T(\ulcorner ¬ φ\urcorner) ) of consistency statements, respectively. Our results separate these formalizations in terms of modal logic.

Cited by

• Provability interpretation of non-normal modal logics having neighborhood semantics
• Modal logical aspects of provability predicates and consistency statements
• Refinements of provability and consistency principles for the second incompleteness theorem

Related

• Provability interpretation of non-normal modal logics having neighborhood semantics
• Modal logical aspects of provability predicates and consistency statements
• Arithmetical completeness for some extensions of the pure logic of necessitation
• Completeness theorems for modal logic in second-order arithmetic
• The Modal Logic of Provability and Forcing