Intuitionistic modal logics are extensions of intuitionistic propositional logic with modal axioms. We treat with two modal languages ${\mathscr{L}}_\Diamond $ and $\mathscr{L}_{\Diamond,\Box }$ which extend the intuitionistic propositional language with $\Diamond $ and $\Diamond,\Box $, respectively. Gentzen sequent calculi are established for several intuitionistic modal logics. In particular, we introduce a Gentzen sequent calculus for the well-known intuitionistic modal logic $\textsf{MIPC}$. These sequent calculi admit cut elimination and subformula property. They are decidable.

Throughout this paper, we are trying to show how and why our Mathematical frame-work seems inappropriate to solve problems in Theory of Computation. More exactly, the concept of turning back in time in paradoxes causes inconsistency in modeling of the concept of Time in some semantic situations. As we see in the first chapter, by introducing a version of “Unexpected Hanging Paradox”,first we attempt to open a new explanation for some paradoxes. In the second step, by applying this paradox, it (...) is demonstrated that any formalized system for the Theory of Computation based on Classical Logic and Turing Model of Computation leads us to a contradiction. We conclude that our mathematical frame work is inappropriate for Theory of Computation. Furthermore, the result provides us a reason that many problems in Complexity Theory resist to be solved.(This work is completed in 2017 -5- 2, it is in vixra in 2017-5-14, presented in Unilog 2018, Vichy). (shrink)

The relationship between Lexical-Functional Grammar (LFG) functional structures (f-structures) for sentences and their semanticinterpretations can be formalized in linear logic in a way thatcorrectly explains the observed interactions between quantifier scopeambiguity, bound anaphora and intensionality.Our linear-logic formalization of the compositional properties ofquantifying expressions in natural language obviates the need forspecial mechanisms, such as Cooper storage, in representing thescoping possibilities of quantifying expressions. Instead, thesemantic contribution of a quantifier is recorded as a linear-logicformula whose use in a proof will establish the (...) scope of thequantifier. Different proofs can lead to different scopes. In eachcomplete proof, the properties of linear logic ensure thatquantifiers are properly scoped. (shrink)

The article presents a calculus of syntactic types which differs from the calculi L and NL of J. Lambek in that, in its Gentzen-like form, sequent antecedents are neither strings nor phrase structures but functor-argument structures. The product-free part of the calculus is shown to be equivalent to the system AB due to Ajdukiewicz and Bar-Hillel. However, if the empty sequent antecedent is admitted, the resulting product-free calculus is not finitely cut-rule axiomatizable.

We give a proof-theoretic and algorithmic complexity analysis for systems introduced by Morrill to serve as the core of the CatLog categorial grammar parser. We consider two recent versions of Morrill’s calculi, and focus on their fragments including multiplicative (Lambek) connectives, additive conjunction and disjunction, brackets and bracket modalities, and the! subexponential modality. For both systems, we resolve issues connected with the cut rule and provide necessary modifications, after which we prove admissibility of cut (cut elimination theorem). We also prove (...) algorithmic undecidability for both calculi, and show that categorial grammars based on them can generate arbitrary recursively enumerable languages. (shrink)

This papers gives a survey of recent results about simulations of one class of modal logics by another class and of the transfer of properties of modal logics under extensions of the underlying modal language. We discuss: the transfer from normal polymodal logics to their fusions, the transfer from normal modal logics to their extensions by adding the universal modality, and the transfer from normal monomodal logics to minimal tense extensions. Likewise, we discuss simulations of normal polymodal logics by normal (...) monomodal logics, of nominals and the difference operator by normal operators, of monotonic monomodal logics by normal bimodal logics, of polyadic normal modal logics by polymodal normal modal logics, and of intuitionistic modal logics by normal bimodal logics. (shrink)

A cut-free Gentzen sequent calculus for Ewald’s intuitionistic tense logic \ is established. By the proof-theoretic method, we prove that, for every set of strictly positive implications S, the classical tense logic \ is embedded into its intuitionistic analogue \ via Kolmogorov, Gödel–Genzten and Kuroda translations respectively. A sufficient and necessary condition for Glivenko type theorem in tense logics is established.

Involutive Nonassociative Lambek Calculus is a nonassociative version of Noncommutative Multiplicative Linear Logic, but the multiplicative constants are not admitted. InNL adds two linear negations to Nonassociative Lambek Calculus ; it is a strongly conservative extension of NL Logical aspects of computational linguistics. LNCS, vol 10054. Springer, Berlin, pp 68–84, 2016). Here we also add unary modalities satisfying the residuation law and De Morgan laws. For the resulting logic InNLm, we define and study phase spaces. We use them to prove (...) the cut elimination theorem for a one-sided sequent system for InNLm, introduced here. Phase spaces are also employed in studying auxiliary systems InNLm, assuming the k-cyclic law for negation. The latter behave similarly as Classical Nonassociative Lambek Calculus, studied in de Groote and Lamarche :355–388, 2002) and Buszkowski. We reduce the provability in InNLm to that in InNLm. This yields the equivalence of type grammars based on InNLm with -free) context-free grammars and the PTIME complexity of InNLm. (shrink)

This contributed volume includes both theoretical research on philosophical logic and its applications in artificial intelligence, mostly employing the concepts and techniques of modal logic. It collects selected papers presented at the Second Asia Workshop on Philosophical Logic, held in Guangzhou, China in 2014, as well as a number of invited papers by specialists in related fields. The contributions represent pioneering philosophical logic research in Asia.

We provide a complete binary implicational axiomatization of the positive fragment of propositional dynamic logic. The intended application of this result are completeness proofs for non-classical extensions of positive PDL. Two examples are discussed in this article, namely, a paraconsistent extension with modal De Morgan negation and a substructural extension with the residuated operators of the non-associative Lambek calculus. Informal interpretations of these two extensions are outlined.

Every language recognized by the Lambek calculus with brackets is context-free. This is shown by combining an observation by Jäger with an entirely straightforward adaptation of the method Pentus used for the original Lambek calculus. The case of the variant of the calculus allowing sequents with empty antecedents is slightly more complicated, requiring a restricted use of the multiplicative unit.

The article presents proofs of the context freeness of a family of typelogical grammars, namely all grammars that are based on a uni- ormultimodal logic of pure residuation, possibly enriched with thestructural rules of Permutation and Expansion for binary modes.

\ is a 7000 line Prolog parser/theorem-prover for logical categorial grammar. In such logical categorial grammar syntax is universal and grammar is reduced to logic: an expression is grammatical if and only if an associated logical statement is a theorem of a fixed calculus. Since the syntactic component is invariant, being the logic of the calculus, logical categorial grammar is purely lexicalist and a particular language model is defined by just a lexical dictionary. The foundational logic of continuity was established (...) by Lambek while a corresponding extension including also logic of discontinuity was established by Morrill and Valentín :167–192, 2010). \ implements a logic including as primitive connectives the continuous and discontinuous connectives of the displacement calculus, additives, 1st order quantifiers, normal modalities, bracket modalities, and universal and existential subexponentials. In this paper we review the rules of inference for these primitive connectives and their linguistic applications, and we survey the principles of Andreoli’s focusing, and of a generalisation of van Benthem’s count-invariance, on the basis of which \ is implemented. (shrink)

The Lambek-Grishin calculus is a symmetric version of categorial grammar obtained by augmenting the standard inventory of type-forming operations (product and residual left and right division) with a dual family: coproduct, left and right difference. Interaction between these two families is provided by distributivity laws. These distributivity laws have pleasant invariance properties: stability of interpretations for the Curry-Howard derivational semantics, and structure-preservation at the syntactic end. The move to symmetry thus offers novel ways of reconciling the demands of natural language (...) form and meaning. (shrink)

This paper describes a prototype implementation of a Labelled Deduction System for natural language interpretation, where interpretation is taken to be the process of understanding a natural language utterance. The implementation models the process of understanding wh-gap dependencies in questions and relative clauses for a fragment of English. The paper is divided in three main sections. In Section 1, we introduce the basic architecture of the system. Section 2 outlines a prototype implementation of wh-binding and indicates its potential for explanation (...) of linguistic phenomena, and in Section 3 we briefly set the model within a large theoretical perspective, comparing it to other type-logical approaches to natural language analysis. (shrink)

The Distributional Compositional Categorical model is a mathematical framework that provides compositional semantics for meanings of natural language sentences. It consists of a computational procedure for constructing meanings of sentences, given their grammatical structure in terms of compositional type-logic, and given the empirically derived meanings of their words. For the particular case that the meaning of words is modelled within a distributional vector space model, its experimental predictions, derived from real large scale data, have outperformed other empirically validated methods that (...) could build vectors for a full sentence. This success can be attributed to a conceptually motivated mathematical underpinning, something which the other methods lack, by integrating qualitative compositional type-logic and quantitative modelling of meaning within a category-theoretic mathematical framework. The type-logic used in the DisCoCat model is Lambekʼs pregroup grammar. Pregroup types form a posetal compact closed category, which can be passed, in a functorial manner, on to the compact closed structure of vector spaces, linear maps and tensor product. The diagrammatic versions of the equational reasoning in compact closed categories can be interpreted as the flow of word meanings within sentences. Pregroups simplify Lambekʼs previous type-logic, the Lambek calculus. The latter and its extensions have been extensively used to formalise and reason about various linguistic phenomena. Hence, the apparent reliance of the DisCoCat on pregroups has been seen as a shortcoming. This paper addresses this concern, by pointing out that one may as well realise a functorial passage from the original type-logic of Lambek, a monoidal bi-closed category, to vector spaces, or to any other model of meaning organised within a monoidal bi-closed category. The corresponding string diagram calculus, due to Baez and Stay, now depicts the flow of word meanings, and also reflects the structure of the parse trees of the Lambek calculus. (shrink)