Decidability of the Admissibility Problem for Inference Rules in Some <Emphasis Type="Italic">S</Emphasis>5<Subscript>t</Subscript>-Logics

We examine some many-modal logics extending S5_t, t ∈ N, for decidability w.r.t. admissibility of inference rules, and for the logics in question, we prove an algorithmic criterion determining whether the inference rules in them are admissible.__________Translated from Algebra i Logika, Vol. 44, No. 4, pp. 438–458, July–August, 2005.     

A focused approach to combining logics

We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut-elimination holds in such fragments. From cut-elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical-linear hybrid logics.     

Hypersequent calculi for intuitionistic logic with classical atoms

We discuss a propositional logic which combines classical reasoning with constructive reasoning, i.e., intuitionistic logic augmented with a class of propositional variables for which we postulate the decidability property. We call it intuitionistic logic with classical atoms. We introduce two hypersequent calculi for this logic. Our main results presented here are cut-elimination with the subformula property for the calculi. As corollaries, we show decidability, an extended form of the disjunction property, the existence of embedding into an intuitionistic modal logic and a partial form of interpolation.     

An intuitionistic formula hierarchy based on high‐school identities

We revisit the notion of intuitionistic equivalence and formal proof representations by adopting the view of formulas as exponential polynomials. After observing that most of the invertible proof rules of intuitionistic (minimal) propositional sequent calculi are formula (i.e., sequent) isomorphisms corresponding to the high‐school identities, we show that one can obtain a more compact variant of a proof system, consisting of non‐invertible proof rules only, and where the invertible proof rules have been replaced by a formula normalization procedure. Moreover, for certain proof systems such as the G4ip sequent calculus of Vorob'ev, Hudelmaier, and Dyckhoff, it is even possible to see all of the non‐invertible proof rules as strict inequalities between exponential polynomials; a careful combinatorial treatment is given in order to establish this fact. Finally, we extend the exponential polynomial analogy to the first‐order quantifiers, showing that it gives rise to an intuitionistic hierarchy of formulas, resembling the classical arithmetical hierarchy, and the first one that classifies formulas while preserving isomorphism.     

A proof-search procedure for intuitionistic propositional logic

A sequent root-first proof-search procedure for intuitionistic propositional logic is presented. The procedure is obtained from modified intuitionistic multi-succedent and classical sequent calculi, making use of Glivenko’s Theorem. We prove that a sequent is derivable in a standard intuitionistic multi-succedent calculus if and only if the corresponding prefixed-sequent is derivable in the procedure.     

New operations in intuitionistic calculus

The question is studied of the possibility of extending the intuitionistic propositional calculus by adding single-valued one-place operations which are not expressible in terms of conjunction, disjunction, implication, or negation. There is constructed a system of correct calculi with new single-valued operations which is isomorphic to the family of proper extensions of the intuitionistic propositional calculus.Translated from Matematicheskie Zametki, Vol. 22, No. 1, pp. 23–28, July, 1977.The author wishes to thank L. L. Maksimova for his help with this paper.     

Path calculus in the modal logic S4

We describe the tableau and inverse calculi for the propositional modal logic S4. The formulas are treated as sets of paths. We obtain the upper bound for the number of applications of rules in the deduction tree.__________Translated from Lietuvos Matematikos Rinkinys, Vol. 45, No. 1, pp. 117–126, January–March, 2005.Translated by R. Lapinskas     

On intuitionistic modal and tense logics and their classical companion logics: Topological semantics and bisimulations

We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order (or partial-order) with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that their topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics.     

Intuitionistic ϵ- and τ-calculi

There are several open problems in the study of the calculi which result from adding either of Hilbert's ?- or τ-operators to the first order intuitionistic predicate calculus. This paper provides answers to several of them. In particular, the first complete and sound semantics for these calculi are presented, in both a “quasi-extensional” version which uses choice functions in a straightforward way to interpret the ?- or τ-terms, and in a form which does not require extensionality assumptions. Unlike the classical case, the addition of either operator to intuitionistic logic is non-conservative. Several interesting consequences of the addition of each operator are proved. Finally, the independence of several other schemes in either calculus are also proved, making use of the semantics supplied earlier in the paper.     

A Basis in Semi‐Reduced Form for the Admissible Rules of the Intuitionistic Logic IPC

We study the problem of finding a basis for all rules admissible in the intuitionistic propositional logic IPC. The main result is Theorem 3.1 which gives a basis consisting of all rules in semi‐reduced form satisfying certain specific additional requirements. Using developed technique we also find a basis for rules admissible in the logic of excluded middle law KC.     

Upper bound on the lengthening of proofs by cut elimination

In this paper there are constructed sequential calculi KGL and IGL. The calculus KGI is a version of the classical predicate calculus, and IGL is a version of constructive calculus. KGL and IGL do not contain structural rules and there are no rules in them for which in some premise more than one lateral formula would be contained. A procedure for eliminating cuts from proofs in these calculi is described. It is shown that the height of a derivation obtained by this procedure exceeds 2 ^h, where h is the height of the original derivation, is the number of sequences in the original derivation,.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 137, pp. 87–98, 1984.     

A proof-theoretical investigation of global intuitionistic (fuzzy) logic

We perform a proof-theoretical investigation of two modal predicate logics: global intuitionistic logic GI and global intuitionistic fuzzy logic GIF. These logics were introduced by Takeuti and Titani to formulate an intuitionistic set theory and an intuitionistic fuzzy set theory together with their metatheories. Here we define analytic Gentzen style calculi for GI and GIF. Among other things, these calculi allows one to prove Herbrands theorem for suitable fragments of GI and GIF.Work Supported by C. Bühler-Habilitations-Stipendium H191-N04, from the Austrian Science Fund (FWF).     

直觉主义类型论中π和Σ规则的研究

本文研究直觉主义类型论中π和Σ规则，对于类型（πｘ∈Ａ）Ｂ（ｘ），我们给出新的消去和相等规则使新规则的式样与其他类型的规则相同，然而不使用高阶交元和常元，我们证明新规则等价于旧规则，对于类型（Σｘ∈Ａ）Ｂ（ｘ），我们利用投影运算给出新规则，而且证明它们等价于旧规则。     

Sequent calculus proof theory of intuitionistic apartness and order relations

Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity results for the theories of constructive order over the usual theories of order. Received: 4 December 1997     

The relation between intuitionistic and classical modal logics

Intuitionistic propositional logicInt and its extensions, known as intermediate or superintuitionistic logics, in many respects can be regarded as just fragments of classical modal logics containingS4. The main aim of this paper is to construct a similar correspondence between intermediate logics augmented with modal operators—we call them intuitionistic modal logics—and classical polymodal logics We study the class of intuitionistic polymodal logics in which modal operators satisfy only the congruence rules and so may be treated as various sorts of □ and ◇. Supported by the Alexander von Humboldt Foundation. Translated fromAlgebra i Logika, Vol. 36, No. 2, pp. 121–155, March–April, 1997.     

Glivenko sequent classes in the light of structural proof theory

In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the results are strengthened to height-preserving statements, and it is further shown that the constructive and minimal proofs are identical in structure to the classical proof from which they are obtained.     

Comments on some versions of intuitionistic fuzzy propositional calculus due to K. Atanassov and G. Gargov

We show that the versions of intuitionistic fuzzy propositional calculus given in Definitions 6 and 7 in Atanassov and Gargov (Fuzzy Sets and Systems 95 (1998) 39–52) do not satisfy modus ponens. Furthermore, we show that the version of intuitionistic fuzzy propositional calculus given in Definition 8 by Atanassov and Gargov is incorrect.     

Uniform interpolation and the existence of sequent calculi

This paper presents a uniform and modular method to prove uniform interpolation for several intermediate and intuitionistic modal logics. The proof-theoretic method uses sequent calculi that are extensions of the terminating sequent calculus $\mathsf{G4ip}$ for intuitionistic propositional logic. It is shown that whenever the rules in a calculus satisfy certain structural properties, the corresponding logic has uniform interpolation. It follows that the intuitionistic versions of $\mathsf{K}$ and $\mathsf{KD}$ (without the diamond operator) have uniform interpolation. It also follows that no intermediate or intuitionistic modal logic without uniform interpolation has a sequent calculus satisfying those structural properties, thereby establishing that except for the seven intermediate logics that have uniform interpolation, no intermediate logic has such a sequent calculus.     

Polarized games

We generalize the intuitionistic Hyland–Ong games (and in a second step Abramsky–Jagadeesan–Malacaria games) to a notion of polarized games allowing games with plays starting by proponent moves. The usual constructions on games are adjusted to fit this setting yielding game models for both Intuitionistic Linear Logic and Polarized Linear Logic. We prove a definability result for this polarized model and this gives complete game models for various classical systems: , λμ-calculus, … for both call-by-name and call-by-value evaluations.     

The topological models of intuitionistic anlaysis. One counterexample

In the paper we prove the falsity of the complete Brouwer principle in a topological model of intuitionistic analysis, constructed by Moschovakis. We present a counterexample showing the impossibility of extending this model and Scott's model up to a model of intuitionistic analysis with the complete Brouwer principle.Translated from Matematicheskie Zametki, Vol. 19, No. 6, pp. 859–862, June, 1976.