The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.

Given an argumentation network we associate with it a modal formula representing the 'logical content' of the network. We show a one-to-one correspondence between all possible complete Caminada labellings of the network and all possible models of the formula.

The system GLS, which is a modal sequent calculus system for the provability logic GL, was introduced by G. Sambin and S. Valentini in Journal of Philosophical Logic, 11, 311–342,, and in 12, 471–476,, the second author presented a syntactic cut-elimination proof for GLS. In this paper, we will use regress trees in order to present a simpler and more intuitive syntactic cut derivability proof for GLS1, which is a variant of GLS without the cut rule.

We suggest an algebraic approach to proof-theoretic analysis based on the notion of graded provability algebra, that is, Lindenbaum boolean algebra of a theory enriched by additional operators which allow for the structure to capture proof-theoretic information. We use this method to analyze Peano arithmetic and show how an ordinal notation system up to 0 can be recovered from the corresponding algebra in a canonical way. This method also establishes links between proof-theoretic ordinal analysis and the work which has been (...) done in the last two decades on provability logic and reflection principles. Because of its abstract algebraic nature, we hope that it will also be of interest for non-prooftheorists. (shrink)

The bimodal provability logics of analysis for ordinary provability and provability by the ω-rule are shown to be fragments of certain ‘polymodal’ logics introduced by G.K. Dzhaparidze. In addition to modal axiom schemes expressing Löb's theorem for the two kinds of provability, the logics treated here contain a scheme expressing that if a statement is consistent, then the statement that it is consistent is provable by the ω-rule.

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)

In this paper individual proofs are integrated into provability logic. Systems of axioms for a logic with operators “A is provable” and “p is a proof of A” are introduced, provided with Kripke semantics and decision procedure. Completeness theorems with respect to the arithmetical interpretation are proved.

The logic of single-conclusion proofs () is introduced. It combines the verification property of proofs with the single valuedness of proof predicate and describes the operations on proofs induced by modus ponens rule and proof checking. It is proved that is decidable, sound and complete with respect to arithmetical proof interpretations based on single-valued proof predicates. The application to arithmetical inference rules specification and -admissibility testing is considered. We show that the provability in gives the complete admissibility test for the (...) rules which can be specified by schemes in -language. The test is supplied with the ground proof extraction algorithm which eliminates the admissible rules from a -proof by utilizing the information from the corresponding -proofs. (shrink)

Let PLω be the provability logic of IΔ0 + ω1. We prove some containments of the form L ⊆ PLω < Th(C) where L is the provability logic of PA and Th(C) is a suitable class of Kripke frames.

The modal logic of Gödel sentences, termed as GS, is introduced to analyze the logical properties of 'true but unprovable' sentences in formal arithmetic. The logic GS is, in a sense, dual to Grzegorczyk's Logic, where modality can be interpreted as 'true and provable'. As we show, GS and Grzegorczyk's Logic are, in fact, mutually embeddable. We prove Kripke completeness and arithmetical completeness for GS. GS is also an extended system of the logic of 'Essence and Accident' proposed by Marcos (...) (Bull Sect Log 34(1):43-56, 2005). We also clarify the relationships between GS and the provability logic GL and between GS and Intuitionistic Propositional Logic. (shrink)

This paper propounds a systematic examination of the link between the Knower Paradox and provability interpretations of modal logic. The aim of the paper is threefold: to give a streamlined presentation of the Knower Paradox and related results; to clarify the notion of a syntactical treatment of modalities; finally, to discuss the kind of solution that modal provability logic provides to the Paradox. I discuss the respective strength of different versions of the Knower Paradox, both in the framework of first-order (...) arithmetic and in that of modal logic with fixed point operators. It is shown that the notion of a syntactical treatment of modalities is ambiguous between a self-referential treatment and a metalinguistic treatment of modalities, and that these two notions are independent. I survey and compare the provability interpretations of modality respectively given by Skyrms, B. (1978, The Journal of Philosophy 75: 368–387) Anderson, C.A. (1983, The Journal of Philosophy 80: 338–355) and Solovay, R. (1976, Israel Journal of Mathematics 25: 287–304). I examine how these interpretations enable us to bypass the limitations imposed by the Knower Paradox while preserving the laws of classical logic, each time by appeal to a distinct form of hierarchy. (shrink)

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. (shrink)

In this paper we study local induction w.r.t. Σ1‐formulas over the weak arithmetic. The local induction scheme, which was introduced in, says roughly this: for any virtual class that is progressive, i.e., is closed under zero and successor, and for any non‐empty virtual class that is definable by a Σ1‐formula without parameters, the intersection of and is non‐empty. In other words, we have, for all Σ1‐sentences S, that S implies, whenever is progressive. Since, in the weak context, we have (at (...) least) two definitions of Σ1, we obtain two minimal theories of local induction w.r.t. Σ1‐formulas, which we call Peano Corto and Peano Basso.In the paper we give careful definitions of Peano Corto and Peano Basso. We establish their naturalness both by giving a model theoretic characterization and by providing an equivalent formulation in terms of a sentential reflection scheme.The theories Peano Corto and Peano Basso occupy a salient place among the sequential theories on the boundary between weak and strong theories. They bring together a powerful collection of principles that is locally interpretable in. Moreover, they have an important role as examples of various phenomena in the metamathematics of arithmetical (and, more generally, sequential) theories. We illustrate this by studying their behavior w.r.t. interpretability, model interpretability and local interpretability. In many ways the theories are more like Peano arithmetic or Zermelo Fraenkel set theory, than like finitely axiomatized theories as Elementary Arithmetic, and. On the one hand, Peano Corto and Peano Basso are very weak: they are locally cut‐interpretable in. On the other hand, they behave as if they were strong: they are not contained in any consistent finitely axiomatized arithmetical theory, however strong. Moreover, they extend, the theory of parameter‐free Π1‐induction. (shrink)

In the paper the joint Logic of Proofs and Provability is presented that incorporates both the modality □ for provability 287–304) and the proof operator tF representing the proof predicate “t is a proof of F” . The obtained system naturally includes both the modal logic of provability GL and Artemov's Logic of Proofs . The presence of the modality □ requires two new operations on proofs that together with operations of allow to realize all the invariant operations on proofs (...) admitting description in the modal propositional language. Logic is proved to be decidable and complete with the intended provability semantics. (shrink)

We study here extensions of the Artemov's logic of proofs in the language with quantifiers on proof variables. Since the provability operator □ A could be expressed in this language by the formula u[u]A, the corresponding logic naturally extends the well-known modal provability logic GL. Besides, the presence of quantifiers on proofs allows us to study some properties of provability not covered by the propositional logics.In this paper we study the arithmetical complexity of the provability logic with quantifiers on proofs (...) for a given arithmetical theory T and a class of proof predicates.In the last section we define Kripke style semantics for the logics corresponding to the standard Gödel proof predicate and its multiple conclusion version. (shrink)

A new modal logic is introduced. It describes properties of provability by interpreting modality as a deductive closure operator on sets of formulas. Logic is proven to be decidable and complete with respect to this semantics.

Quine has argued that modal logic began with the sin of confusing use and mention. Anderson and Belnap, on the other hand, have offered us a way out through a strategy of nominahzation. This paper reviews the history of Lewis's early work in modal logic, and then proves some results about the system in which "A is necessary" is intepreted as "A is a classical tautology.".

In this paper we study 1. the frame-theory of certain bimodal provability logics involving the reflection principle and we study2. certain specific bimodal logics with a provability predicate for a subtheory of Peano arithmetic axiomatized by a non-standardly finite number of axioms.

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)

We present some results on algebraic and modal analysis of polynomial distortions of the standard provability predicate in Peano Arithmetic PA, and investigate three provability-like modal systems related to the Gödel–Löb modal system GL. We also present a short review of relational and topological semantics for these systems, and describe the dual category of algebraic models of our main modal system.

In the pioneering article and two papers, written jointly with McKinsey, Tarski developed the so-called algebraic and topological frameworks for the Intuitionistic Logic and the Lewis modal system. In this paper, we present an outline of modern systems with a topological tinge. We consider topological interpretation of basic systems GL and G of the provability logic in terms of the Cantor derivative and the Hausdorff residue.

A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.

Interpretability logic is an extension of provability logic. Veltman models and generalized Veltman models are two semantics for interpretability logic. We consider a connection between Veltman semantics and generalized Veltman semantics. We prove that for a complete image-finite generalized Veltman modelW there is a Veltman model W ′ that is bisimular to W.

We establish the bi-modal forgetful projection of the Logic of Proofs and Formal Provability GLA. That is to say, we present a normal bi-modal provability logic with modalities □ and whose theorems are precisely those formulas for which the implicit provability assertions represented by the modality can be realized by explicit proof terms.

Formulas of the propositional modal language with the unary modal operators □, Σ1, 1, Σ2, 2,… are considered as schemata of sentences of arithmetic , where □A is interpreted as “A is PA-provable”, ΣnA as “A is PA-equivalent to a Σn-sentence” and nA as “A is PA-equivalent to a Boolean combination of Σn-sentences”. We give an axiomatization and show decidability of the sets of the modal formulas which are schemata of: PA-provable, true arithmetical sentences.