Arithmetical Soundness and Completeness for $$\varvec{\Sigma }_{\varvec{2}}$$ Numerations

We prove that for each recursively axiomatized consistent extension T of Peano Arithmetic and \(n \ge 2\), there exists a \(\Sigma _2\) numeration \(\tau (u)\) of T such that the provability logic of the provability predicate \(\mathsf{Pr}_\tau (x)\) naturally constructed from \(\tau (u)\) is exactly \(\mathsf{K}+ \Box (\Box ^n p \rightarrow p) \rightarrow \Box p\). This settles Sacchetti’s problem affirmatively.     

On Inclusions Between Quantified Provability Logics

Studia Logica - We investigate several consequences of inclusion relations between quantified provability logics. Moreover, we give a necessary and sufficient condition for the inclusion relation...     

Arithmetical Completeness Theorem for Modal Logic $$\mathsf{}$$

We prove that for any recursively axiomatized consistent extension T of Peano Arithmetic, there exists a \(\Sigma _2\) provability predicate of T whose provability logic is precisely the modal logic \(\mathsf{K}\). For this purpose, we introduce a new bimodal logic \(\mathsf{GLK}\), and prove the Kripke completeness theorem and the uniform arithmetical completeness theorem for \(\mathsf{GLK}\).     

Rosser-Type Undecidable Sentences Based on Yablo’s Paradox

It is widely considered that Gödel’s and Rosser’s proofs of the incompleteness theorems are related to the Liar Paradox. Yablo’s paradox, a Liar-like paradox without self-reference, can also be used to prove Gödel’s first and second incompleteness theorems. We show that the situation with the formalization of Yablo’s paradox using Rosser’s provability predicate is different from that of Rosser’s proof. Namely, by using the technique of Guaspari and Solovay, we prove that the undecidability of each instance of Rosser-type formalizations of Yablo’s paradox for each consistent but not Σ₁-sound theory is dependent on the choice of a standard proof predicate.     

Rosser Provability and Normal Modal Logics

Studia Logica - In this paper, we investigate Rosser provability predicates whose provability logics are normal modal logics. First, we prove that there exists a Rosser provability predicate whose...     

Liar-type Paradoxes and the Incompleteness Phenomena

We define a liar-type paradox as a consistent proposition in propositional modal logic which is obtained by attaching boxes to several subformulas of an inconsistent proposition in classical propositional logic, and show several famous paradoxes are liar-type. Then we show that we can generate a liar-type paradox from any inconsistent proposition in classical propositional logic and that undecidable sentences in arithmetic can be obtained from the existence of a liar-type paradox. We extend these results to predicate logic and discuss Yablo’s Paradox in this framework. Furthermore, we define explicit and implicit self-reference in paradoxes in the incompleteness phenomena.