We investigate the bimodal logics sound and complete under the interpretation of modal operators as the provability predicates in certain natural pairs of arithmetical theories . Carlson characterized the provability logic for essentially reflexive extensions of theories, i.e. for pairs similar to . Here we study pairs of theories such that the gap between and is not so wide. In view of some general results concerning the problem of classification of the bimodal provability logics we are particularly interested in such (...) pairs that is axiomatized over by ∏1-sentences only, and, for each n 1, proves the n-times iterated consistency of . A complete axiomatization, along with the appropriate Kripke semantics and decision procedures, is found for the two principal cases: finitely axiomatizable extensions of this sort, like e.g. ), ), etc., and reflexive extensions, like ¦n 1\s}), etc. We show that the first logic, ICP, is the minimal and the second one, RP, is the maximal within the class of the provability logics for such pairs of theories. We also show that there are some provability logics lying strictly between these two. As an application of the results of this paper, in the last section the polymodal provability logics for natural recursive progressions of theories based on iteration of consistency are characterized. We construct a system of ordinal notation , which gives exactly one notation to each constructive ordinal, such that the logic corresponding to any progression along coincides with that along natural Kalmar elementary well-orderings. (shrink)

For every sequence |p n } n of formulas of Peano ArithmeticPA with, every formulaA of the first-order theory diagonalizable algebras, we associate a formula 0 A, called the value ofA inPA with respect to the interpretation. We show that, ifA is true in every diagonalizable algebra, then, for every, 0 A is a theorem ofPA.

A nonempty sequence T1,...,Tn of theories is tolerant, if there are consistent theories T 1 + ,..., T n + such that for each 1 i n, T i + is an extension of Ti in the same language and, if i n, T i + interprets T i+1 + . We consider a propositional language with the modality , the arity of which is not fixed, and axiomatically define in this language the decidable logics TOL and TOL. It is (...) shown that TOL (resp. TOL) yields exactly the schemata of PA-provable (resp. true) arithmetical sentences, if (A1,..., An) is understood as (a formalization of) PA+A1, ..., PA+An is tolerant. (shrink)

The undecidability of the first-order theory of diagonalizable algebras is shown here.

The duality theory established by Halmos in [2] for boolean hemimorphism applies of course to the diagonalizable algebra, because ντν is an hemimorphism. For commodity in working on diagonalizable algebras we recall the basic facts and give the characteristic conditions on the dual of ντν.

In a recent paper, Montagna proved the undecidability of the first-order theory of diagonalisable algebras. This result is here refined — the set of finitely refutable sentences is shown effectively inseparable from the set of theorems. The proof is quite simple.

We prove that the diagonalizable algebras of PA and ZF are not isomorphic.

Dzhaparidze, G., A generalized notion of weak interpretability and the corresponding modal logic, Annals of Pure and Applied Logic 61 113-160. A tree Tr of theories T1,...,Tn is called tolerant, if there are consistent extensions T+1,...,T+n of T1,...,Tn, where each T+i interprets its successors in the tree Tr. We consider a propositional language with the following modal formation rule: if Tr is a tree of formulas, then Tr is a formula, and axiomatically define in this language the decidable logics TLR (...) and TLRω. It is proved that TLR yields exactly the schemata of PA-provable sentences, if Tr is understood as “Tr is tolerant”. In fact, TLR axiomatizes a considerable fragment of provability logic with quantifiers over ∑1-sentences, and many relations that have been studied in the literature can be expressed in terms of tolerance. We introduce and study two more relations between theories: cointerpretability and cotolerance which are, in a sense, dual to interpretability and tolerance. Cointerpretability is a characterization of ∑1-conservativity for essentially reflexive theories in terms of translations. (shrink)