We present an axiomatization for Basic Propositional Calculus BPC and give a completeness theorem for the class of transitive Kripke structures. We present several refinements, including a completeness theorem for irreflexive trees. The class of intermediate logics includes two maximal nodes, one being Classical Propositional Calculus CPC, the other being E1, a theory axiomatized by T → ⊥. The intersection CPC ∩ E1 is axiomatizable by the Principle of the Excluded Middle A V ∨ ⌝A. If B is a formula (...) such that → B is not derivable, then the lattice of formulas built from one propositional variable p using only the binary connectives, is isomorphically preserved if B is substituted for p. A formula → B is derivable exactly when B is provably equivalent to a formula of the form → A) →. (shrink)

We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.

This paper studies a propositional logic which is obtained by interpreting implication as formal provability. It is also the logic of finite irreflexive Kripke Models.A Kripke Model completeness theorem is given and several completeness theorems for interpretations into Provability Logic and Peano Arithmetic.

This paper is a comparative study of the propositional intuitionistic (non-modal) and classical modal languages interpreted in the standard way on transitive frames. It shows that, when talking about these frames rather than conventional quasi-orders, the intuitionistic language displays some unusual features: its expressive power becomes weaker than that of the modal language, the induced consequence relation does not have a deduction theorem and is not protoalgebraic. Nevertheless, the paper develops a manageable model theory for this consequence and its extensions (...) which also reveals some unexpected phenomena. The balance between the intuitionistic and modal languages is restored by adding to the former one more implication. (shrink)

We characterize the first-order formulas with one free variable that are preserved under bisimulation and persistence or strong persistence over the class of Kripke models with transitive frames and unary persistent predicates.

Masini, A., 2-Sequent calculus: a proof theory of modalities, Annals of Pure and Applied Logic 58 229–246. In this work we propose an extension of the Getzen sequent calculus in order to deal with modalities. We extend the notion of a sequent obtaining what we call a 2-sequent. For the obtained calculus we prove a cut elimination theorem.

We introduce a dual-context style sequent calculus which is complete with respectto Kripke semantics where implication is interpreted as strict implication in the modal logic K. The cut-elimination theorem for this calculus is proved by a variant of Gentzen's method.

This paper introduces sequent systems for Visser's two propositional logics: Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL). It is shown through semantical completeness that the cut rule is admissible in each system. The relationships with Hilbert-style axiomatizations and with other sequent formulations are discussed. The cut-elimination theorems are also demonstrated by syntactical methods.

We present a single sequent calculus common to classical, intuitionistic and linear logics. The main novelty is that classical, intuitionistic and linear logics appear as fragments, i.e. as particular classes of formulas and sequents. For instance, a proof of an intuitionistic formula A may use classical or linear lemmas without any restriction: but after cut-elimination the proof of A is wholly intuitionistic, what is superficially achieved by the subformula property and more deeply by a very careful treatment of structural rules. (...) This approach is radically different from the one that consists in “changing the rule of the game” when we want to change logic, e.g. pass from one style of sequent to another: here, there is only one logic, which—depending on its use—may appear classical, intuitionistic or linear. (shrink)

Visser's propositional logic was first considered in Visser [5] as the propositional logic embedded into the modal logic {\bf K4} by G\"odel's translation. He gave a natural deduction system $\vdash_V$ for the consequence relation of {\bf VPL}. An essential difference from the consequence relation $\vdash_I$ of intuitionistic propositional logic is $\{a,a\supset b\}\not \vdash_Vb$ while $\{ a,a\supset b\}\vdash_Ib$. In other words, in $\vdash_V$, modus ponens does not hold in general. So, we may well say that systems for the consequence relation of (...) {\bf VPL} are obtained from the systems for $\vdash_I$ by replacing the inference rule, which corresponds to modus ponens, by other inference rules. For instance, Visser's system $ \vdash_V$ was obtained from Gentzen's natural deduction system $\vdash_{ NJ}$ by replacing implication elimination rule by three other inference rules. Ardeshir [1] and [2] gave sequent style systems for $\vdash_V$ by replacing the inference rule in Gentzen's sequent system {\bf LJ} by other inference rules. However, it seems difficult to give a finite Hilbert style system for the consequence relation of {\bf VPL} because modus pones in Hilbert style system for $\vdash_I$ has the role of translating axioms into inference rules, and so, we have to find another inference rule having the same role in $\vdash_V$. This problem was raised in Suzuki, Wolter and Zakharyaschev [4]. Here we introduce a restricted modus ponens, which mostly has the same role as modus ponens in Hilbert style system for $\vdash_I$ has. Using the restricted modus ponens and adjunction, we give a formalization for $ \vdash_V$, and at the same time we show that $\vdash_V$ can not be formalized by any systems with a restricted modus ponens as only one inference rule. (shrink)

In this paper we prove a bounded translation of intuitionistic propositional logic into basic propositional logic. Our new theorem, compared with the translation theorem in [1], has the advantage that it gives an effective bound on the translation, depending on the complexity of formulas.