In this paper we prove that the preordering $\lesssim $ of provable implication over any recursively enumerable theory $T$ containing a modicum of arithmetic is uniformly dense. This means that we can find a recursive extensional density function $F$ for $\lesssim $. A recursive function $F$ is a density function if it computes, for $A$ and $B$ with $A\lnsim B$, an element $C$ such that $A\lnsim C\lnsim B$. The function is extensional if it preserves $T$-provable equivalence. Secondly, we prove a (...) general result that implies that, for extensions of elementary arithmetic, the ordering $\lesssim $ restricted to $\Sigma_{n}$-sentences is uniformly dense. In the last section we provide historical notes and background material. (shrink)

We generalize a well-knownSmullyan's result, by showing that any two sets of the kindC a = {x/ xa} andC b = {x/ xb} are effectively inseparable (if I b). Then we investigate logical and recursive consequences of this fact (see Introduction).

We prove that for each recursively axiomatized consistent extension T of Peano Arithmetic and \, there exists a \ numeration \\) of T such that the provability logic of the provability predicate \\) naturally constructed from \\) is exactly \ \rightarrow \Box p\). This settles Sacchetti’s problem affirmatively.

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 provability logic is exactly the normal modal logic \. Secondly, we introduce a new normal modal logic \ which is a proper extension of \, and prove that there exists a Rosser provability predicate whose provability logic includes \.

In this paper, we show how to construct for a given consistent theory U a $$\varSigma ^0_1$$ Σ 1 0 -predicate that both satisfies the Löb Conditions and the Kreisel Condition—even if U is unsound. We do this in such a way that U itself can verify satisfaction of an internal version of the Kreisel Condition.

In this paper we study proofs of some general forms of the Second Incompleteness Theorem. These forms conform to the Feferman format, where the proof predicate is fixed and the representation of the set of axioms varies. We extend the Feferman framework in one important point: we allow the interpretation of number theory to vary.

Franco Montagna, a prominent logician and one of the leaders of the Italian school on Mathematical Logic, passed away on February 18, 2015. We survey some of his results and ideas in the two disciplines he greatly contributed along his career: provability logic and many-valued logic.

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

This paper develops the philosophy and technology needed for adding a supremum operator to the interpretability logic ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document} of Peano Arithmetic. It is well-known that any theories extending PA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {PA}$$\end{document} have a supremum in the interpretability ordering. While provable in PA\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {PA}$$\end{document}, this fact is not reflected in the theorems of the modal (...) system ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document}, due to limited expressive power. Our goal is to enrich the language of ILM\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {ILM}$$\end{document} by adding to it a new modality for the interpretability supremum. We explore different options for specifying the exact meaning of the new modality. Our final proposal involves a unary operator, the dual of which can be seen as a provability predicate satisfying the axioms of the provability logic GL\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\mathsf {GL}$$\end{document}. (shrink)