We say that two arithmetical formulas A, B have the Σ1-interpolation property if they have an ‘interpolant’ σ, i.e., a Σ1 formula such that the formulas A→σ and σ→B are provable in Peano Arithmetic PA. The Σ1-interpolability predicate is just a formalization of this property in the language of arithmetic.Using a standard idea of Gödel, we can associate with this predicate its provability logic, which is the set of all formulas that express arithmetically valid principles in the modal language with (...) two modal operators, □ for provability in PA and for Σ1-interpolability. In this paper we determine this provability logic .It turns out that this problem appears to be quite similar to the problem of such modal description of relative interpretability, a problem, solved by Berarducci and Shavrukov. However, the present case is sometimes easier. In particular, we prove in this paper the fixed point property and the Craig interpolation property for our modal system ELH. (shrink)

PA is Peano Arithmetic. Pr(x) is the usual Σ1-formula representing provability in PA. A strong provability predicate is a formula which has the same properties as Pr(·) but is not Σ1. An example: Q is ω-provable if PA + ¬ Q is ω-inconsistent (Boolos [4]). In [5] Dzhaparidze introduced a joint provability logic for iterated ω-provability and obtained its arithmetical completeness. In this paper we prove some further modal properties of Dzhaparidze's logic, e.g., the fixed point property and the Craig (...) interpolation lemma. We also consider other examples of the strong provability predicates and their applications. (shrink)

In this paper we present a general theory of normal forms, based on a categorial result for the free monoid construction. We shall use the theory mainly for proposictional modal logic, although it seems to have a wider range of applications. We shall formally represent normal forms as combinatorial objects, basically labelled trees and forests. This geometric conceptualization is implicit in and our approach will extend it to other cases and make it more direct: operations of a purely geometric and (...) combinatorial nature will be introduced in order to give a mathematical description of the basic logical/algebraic constructions .We begin by recalling the above-mentioned categorial construction: we need a careful inspection of it because in the various examples considered later we plan to deduce from it in a uniform way the normal forms and the description of finitely generated free algebras. This method always works whenever we can describe the category of algebras corresponding to the logic under consideration as a T-objects category. When this simple description seems not to be available, still the general theory might be of some interest, because a description of the category of algebras as a T-objects category plus equation is possible .The central part of the paper is more advanced and specific: we show how the general approach presented here can provide some insights even in the basic case of the modal system K. Section 4 contains a contribution to the theory of normal forms, namely the description of the uniform substitution. This result will enable us to give a duality theorem for the category of finitely generated free modal algebras and in Section 5 to provide a characterization of the collections of normal forms which happen to be normal forms for a logic, thus giving a description of the lattice of modal logics.Section 6 deals with some applications: we shall show how to use normal forms in order to prove for the modal system K the definability of higher-order propositional quantifiers and of the tense operator F .As to the prerequisites, the paper is almost self-contained. The reader is only assumed to have familiarity with standard techniques in algebraic logic ). Knowledge of the basic facts about adjoint functors is required too, see e.g. McLane or the appendix. (shrink)

A. M. Pitts in [Pi] proved that HA op fp is a bi-Heyting category satisfying the Lawrence condition. We show that the embedding $\Phi: HA^\mathrm{op}_\mathrm{fp} \longrightarrow Sh(\mathbf{P_0,J_0})$ into the topos of sheaves, (P 0 is the category of finite rooted posets and open maps, J 0 the canonical topology on P 0 ) given by $H \longmapsto HA(H,\mathscr{D}(-)): \mathbf{P_0} \longrightarrow \text{Set}$ preserves the structure mentioned above, finite coproducts, and subobject classifier, it is also conservative. This whole structure on HA op (...) fp can be derived from that of Sh(P 0 ,J 0 ) via the embedding Φ. We also show that the equivalence relations in HA op fp are not effective in general. On the way to these results we establish a new kind of duality between HA op fp and a category of sheaves equipped with certain structure defined in terms of Ehrenfeucht games. Our methods are model-theoretic and combinatorial as opposed to proof-theoretic as in [Pi]. (shrink)