## Results for 'Calculus' (try it on Scholar)

1000+ found
Order:
1. 1. Intuitionistic Sentential Calculus with Iden-Tity.Intuitionistic Sentential Calculus - 1990 - Bulletin of the Section of Logic 19 (3):92-99.

Export citation

My bibliography
2. The revised edition contains a new chapter which provides an elegant description of the semantics. The various classes of lambda calculus models are described in a uniform manner. Some didactical improvements have been made to this edition. An example of a simple model is given and then the general theory (of categorical models) is developed. Indications are given of those parts of the book which can be used to form a coherent course.

Export citation

My bibliography   50 citations
3. Differential Calculus Based on the Double Contradiction.Kazuhiko Kotani - 2016 - Open Journal of Philosophy 6 (4):420-427.
The derivative is a basic concept of differential calculus. However, if we calculate the derivative as change in distance over change in time, the result at any instant is 0/0, which seems meaningless. Hence, Newton and Leibniz used the limit to determine the derivative. Their method is valid in practice, but it is not easy to intuitively accept. Thus, this article describes the novel method of differential calculus based on the double contradiction, which is easier to accept intuitively. (...)

Export citation

My bibliography
4. Building on the work of Peter Hinst and Geo Siegwart, we develop a pragmatised natural deduction calculus, i.e. a natural deduction calculus that incorporates illocutionary operators at the formal level, and prove its adequacy. In contrast to other linear calculi of natural deduction, derivations in this calculus are sequences of object-language sentences which do not require graphical or other means of commentary in order to keep track of assumptions or to indicate subproofs. (Translation of our German paper (...)

Export citation

My bibliography
5. Introduction to Combinators and [Lambda]-Calculus.J. Roger Hindley - 1986 - Cambridge University Press.
Combinatory logic and lambda-conversion were originally devised in the 1920s for investigating the foundations of mathematics using the basic concept of 'operation' instead of 'set'. They have now developed into linguistic tools, useful in several branches of logic and computer science, especially in the study of programming languages. These notes form a simple introduction to the two topics, suitable for a reader who has no previous knowledge of combinatory logic, but has taken an undergraduate course in predicate calculus and (...)

Export citation

My bibliography   11 citations
6. Is Leibnizian Calculus Embeddable in First Order Logic?Piotr BLaszczyk, Vladimir Kanovei, Karin U. Katz, Mikhail G. Katz, Taras Kudryk, Thomas Mormann & David Sherry - 2016 - Foundations of Science 22.
To explore the extent of embeddability of Leibnizian infinitesimal calculus in first-order logic (FOL) and modern frameworks, we propose to set aside ontological issues and focus on pro- cedural questions. This would enable an account of Leibnizian procedures in a framework limited to FOL with a small number of additional ingredients such as the relation of infinite proximity. If, as we argue here, first order logic is indeed suitable for developing modern proxies for the inferential moves found in Leibnizian (...)

Export citation

My bibliography
7. The Displacement Calculus.Glyn Morrill, Oriol Valentín & Mario Fadda - 2011 - Journal of Logic, Language and Information 20 (1):1-48.
If all dependent expressions were adjacent some variety of immediate constituent analysis would suffice for grammar, but syntactic and semantic mismatches are characteristic of natural language; indeed this is a, or the, central problem in grammar. Logical categorial grammar reduces grammar to logic: an expression is well-formed if and only if an associated sequent is a theorem of a categorial logic. The paradigmatic categorial logic is the Lambek calculus, but being a logic of concatenation the Lambek calculus can (...)

Export citation

My bibliography   3 citations
8. Polynomial Ring Calculus for Modal Logics: A New Semantics and Proof Method for Modalities.Juan C. Agudelo & Walter Carnielli - 2011 - Review of Symbolic Logic 4 (1):150-170.
A new (sound and complete) proof style adequate for modal logics is defined from the polynomial ring calculus (PRC). The new semantics not only expresses truth conditions of modal formulas by means of polynomials, but also permits to perform deductions through polynomial handling. This paper also investigates relationships among the PRC here defined, the algebraic semantics for modal logics, equational logics, the Dijkstra–Scholten equational-proof style, and rewriting systems. The method proposed is throughly exemplified for S5, and can be easily (...)

Export citation

My bibliography   2 citations
9. A Brief Survey of Frames for the Lambek Calculus.Kosta Došen - 1992 - Mathematical Logic Quarterly 38 (1):179-187.
Models for the Lambek calculus of syntactic categories surveyed here are based on frames that are in principle of the same type as Kripke frames for intuitionistic logic. These models are extracted from the literature on models for relevant logics, in particular the ternary relationed models introduced in the early seventies. The purpose of this brief survey is to locate some open completeness problems for variants of the Lambek calculus in the context of completeness results based on various (...)

Export citation

My bibliography   10 citations
10. Hegel and Deleuze on the Metaphysical Interpretation of the Calculus.Henry Somers-Hall - 2010 - Continental Philosophy Review 42 (4):555-572.
The aim of this paper is to explore the uses made of the calculus by Gilles Deleuze and G. W. F. Hegel. I show how both Deleuze and Hegel see the calculus as providing a way of thinking outside of finite representation. For Hegel, this involves attempting to show that the foundations of the calculus cannot be thought by the finite understanding, and necessitate a move to the standpoint of infinite reason. I analyse Hegel’s justification for this (...)

Export citation

My bibliography   1 citation
11. Relational Semantics of the Lambek Calculus Extended with Classical Propositional Logic.Michael Kaminski & Nissim Francez - 2014 - Studia Logica 102 (3):479-497.
We show that the relational semantics of the Lambek calculus, both nonassociative and associative, is also sound and complete for its extension with classical propositional logic. Then, using filtrations, we obtain the finite model property for the nonassociative Lambek calculus extended with classical propositional logic.

Export citation

My bibliography   1 citation
12. Lambek Calculus and its Relational Semantics: Completeness and Incompleteness. [REVIEW]Hajnal Andréka & Szabolcs Mikulás - 1994 - Journal of Logic, Language and Information 3 (1):1-37.
The problem of whether Lambek Calculus is complete with respect to (w.r.t.) relational semantics, has been raised several times, cf. van Benthem (1989a) and van Benthem (1991). In this paper, we show that the answer is in the affirmative. More precisely, we will prove that that version of the Lambek Calculus which does not use the empty sequence is strongly complete w.r.t. those relational Kripke-models where the set of possible worlds,W, is a transitive binary relation, while that version (...)

Export citation

My bibliography   7 citations
13. On Nonlinear Quantum Mechanics, Noncommutative Phase Spaces, Fractal-Scale Calculus and Vacuum Energy.Carlos Castro - 2010 - Foundations of Physics 40 (11):1712-1730.
A (to our knowledge) novel Generalized Nonlinear Schrödinger equation based on the modifications of Nottale-Cresson’s fractal-scale calculus and resulting from the noncommutativity of the phase space coordinates is explicitly derived. The modifications to the ground state energy of a harmonic oscillator yields the observed value of the vacuum energy density. In the concluding remarks we discuss how nonlinear and nonlocal QM wave equations arise naturally from this fractal-scale calculus formalism which may have a key role in the final (...)

Export citation

My bibliography
14. The Lambek Calculus Enriched with Additional Connectives.Makoto Kanazawa - 1992 - Journal of Logic, Language and Information 1 (2):141-171.
Some formal properties of enriched systems of Lambek calculus with analogues of conjunction and disjunction are investigated. In particular, it is proved that the class of languages recognizable by the Lambek calculus with added intersective conjunction properly includes the class of finite intersections of context-free languages.

Export citation

My bibliography   7 citations
15. Translations From Natural Deduction to Sequent Calculus.J. Von Plato - 2003 - Mathematical Logic Quarterly 49 (5):435.
Gentzen's “Untersuchungen” [1] gave a translation from natural deduction to sequent calculus with the property that normal derivations may translate into derivations with cuts. Prawitz in [8] gave a translation that instead produced cut-free derivations. It is shown that by writing all elimination rules in the manner of disjunction elimination, with an arbitrary consequence, an isomorphic translation between normal derivations and cut-free derivations is achieved. The standard elimination rules do not permit a full normal form, which explains the cuts (...)

Export citation

My bibliography   3 citations
16. The Epsilon Calculus.Jeremy Avigad & Richard Zach - 2013 - In Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy. The Metaphysics Research Lab, Center for the Study of Language and Information, Stanford University.
The epsilon calculus is a logical formalism developed by David Hilbert in the service of his program in the foundations of mathematics. The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. Specifically, in the calculus, a term εx A denotes some x satisfying A(x), if there is one. In Hilbert's Program, the epsilon terms play the role of ideal elements; the aim of Hilbert's finitistic consistency proofs is to give a procedure which removes (...)

Export citation

My bibliography   1 citation
17. Implications-as-Rules Vs. Implications-as-Links: An Alternative Implication-Left Schema for the Sequent Calculus[REVIEW]Peter Schroeder-Heister - 2011 - Journal of Philosophical Logic 40 (1):95 - 101.
The interpretation of implications as rules motivates a different left-introduction schema for implication in the sequent calculus, which is conceptually more basic than the implication-left schema proposed by Gentzen. Corresponding to results obtained for systems with higher-level rules, it enjoys the subformula property and cut elimination in a weak form.

Export citation

My bibliography   1 citation
18. On Modal Μ -Calculus and Gödel-Löb Logic.Luca Alberucci & Alessandro Facchini - 2009 - Studia Logica 91 (2):145 - 169.
We show that the modal µ-calculus over GL collapses to the modal fragment by showing that the fixpoint formula is reached after two iterations and answer to a question posed by van Benthem in [4]. Further, we introduce the modal µ~-calculus by allowing fixpoint constructors for any formula where the fixpoint variable appears guarded but not necessarily positive and show that this calculus over GL collapses to the modal fragment, too. The latter result allows us a new (...)

Export citation

My bibliography   1 citation
19. Strong Normalization of a Symmetric Lambda Calculus for Second-Order Classical Logic.Yoriyuki Yamagata - 2002 - Archive for Mathematical Logic 41 (1):91-99.
We extend Barbanera and Berardi’s symmetric lambda calculus to second order classical propositional logic and prove its strong normalization.

Export citation

My bibliography
20. Full Lambek Calculus in Natural Deduction.Ernst Zimmermann - 2010 - Mathematical Logic Quarterly 56 (1):85-88.
A formulation of Full Lambek Calculus in the framework of natural deduction is given.

Export citation

My bibliography   1 citation
21. Light Affine Lambda Calculus and Polynomial Time Strong Normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time “weak” normalization theorem, it is natural to ask whether a “strong” form of polynomial time normalization theorem holds or not. In this paper, we (...)

Export citation

My bibliography
22. A 'Natural Logic' Inference System Using the Lambek Calculus.Anna Zamansky, Nissim Francez & Yoad Winter - 2006 - Journal of Logic, Language and Information 15 (3):273-295.
This paper develops an inference system for natural language within the ‘Natural Logic’ paradigm as advocated by van Benthem, Sánchez and others. The system that we propose is based on the Lambek calculus and works directly on the Curry-Howard counterparts for syntactic representations of natural language, with no intermediate translation to logical formulae. The Lambek -based system we propose extends the system by Fyodorov et~al., which is based on the Ajdukiewicz/Bar-Hillel calculus Bar Hillel,. This enables the system to (...)

Export citation

My bibliography   1 citation
23. Investigations Into a Left-Structural Right-Substructural Sequent Calculus.Lloyd Humberstone - 2007 - Journal of Logic, Language and Information 16 (2):141-171.
We study a multiple-succedent sequent calculus with both of the structural rules Left Weakening and Left Contraction but neither of their counterparts on the right, for possible application to the treatment of multiplicative disjunction against the background of intuitionistic logic. We find that, as Hirokawa dramatically showed in a 1996 paper with respect to the rules for implication, the rules for this connective render derivable some new structural rules, even though, unlike the rules for implication, these rules are what (...)

Export citation

My bibliography   1 citation
24. Itô's Lemma with Quantum Calculus (Q-Calculus): Some Implications. [REVIEW]Emmanuel Haven - 2011 - Foundations of Physics 41 (3):529-537.
q-derivatives are part of so called quantum calculus. In this paper we investigate how such derivatives can possibly be used in Itô’s lemma. This leads us to consider how such derivatives can be used in a social science setting. We conclude that in a Itô Lemma setting we cannot use a macroscopic version of the Heisenberg uncertainty principle with q-derivatives.

Export citation

My bibliography
25. Powerset Residuated Algebras and Generalized Lambek Calculus.Miroslawa Kolowska‐Gawiejnowicz - 1997 - Mathematical Logic Quarterly 43 (1):60-72.
We prove a representation theorem for residuated algebras: each residuated algebra is isomorphically embeddable into a powerset residuated algebra. As a consequence, we obtain a completeness theorem for the Generalized Lambek Calculus. We use a Labelled Deductive System which generalizes the one used by Buszkowski [4] and Pankrat'ev [17] in completeness theorems for the Lambek Calculus.

Export citation

My bibliography   2 citations
26. A Finite Hilbert‐Style Axiomatization of the Implication‐Less Fragment of the Intuitionistic Propositional Calculus.Jordi Rebagliato & Ventura Verdú - 1994 - Mathematical Logic Quarterly 40 (1):61-68.
In this paper we obtain a finite Hilbert-style axiomatization of the implicationless fragment of the intuitionistic propositional calculus. As a consequence we obtain finite axiomatizations of all structural closure operators on the algebra of {–}-formulas containing this fragment.

Export citation

My bibliography   2 citations
27. Normal Form of Derivations in the Nonassociative and Commutative Lambek Calculus with Product.Maciej Kandulski - 1993 - Mathematical Logic Quarterly 39 (1):103-114.
We show that derivations in the nonassociative and commutative Lambek calculus with product can be transformed to a normal form as it is the case with derivations in noncommutative calculi. As an application we obtain that the class of languages generated by categorial grammars based on the nonassociative and commutative Lambek calculus with product is included in the class of CF-languages. MSC: 68Q50, 03D15, 03B65.

Export citation

My bibliography   2 citations
28. The Situation Calculus: A Case for Modal Logic. [REVIEW]Gerhard Lakemeyer - 2010 - Journal of Logic, Language and Information 19 (4):431-450.
The situation calculus is one of the most established formalisms for reasoning about action and change. In this paper we will review the basics of Reiter’s version of the situation calculus, show how knowledge and time have been addressed in this framework, and point to some of the weaknesses of the situation calculus with respect to time. We then present a modal version of the situation calculus where these problems can be overcome with relative ease and (...)

Export citation

My bibliography
29. A Complete Graphical Calculus for Spekkens’ Toy Bit Theory.Miriam Backens & Ali Nabi Duman - 2016 - Foundations of Physics 46 (1):70-103.
While quantum theory cannot be described by a local hidden variable model, it is nevertheless possible to construct such models that exhibit features commonly associated with quantum mechanics. These models are also used to explore the question of \-ontic versus \-epistemic theories for quantum mechanics. Spekkens’ toy theory is one such model. It arises from classical probabilistic mechanics via a limit on the knowledge an observer may have about the state of a system. The toy theory for the simplest possible (...)

Export citation

My bibliography
30. The Lambek Calculus Extended with Intuitionistic Propositional Logic.Michael Kaminski & Nissim Francez - 2016 - Studia Logica 104 (5):1051-1082.
We present sound and complete semantics and a sequent calculus for the Lambek calculus extended with intuitionistic propositional logic.

Export citation

My bibliography
31. Gentzen-Style Sequent Calculus for Semi-Intuitionistic Logic.Diego Castaño & Juan Manuel Cornejo - 2016 - Studia Logica 104 (6):1245-1265.
The variety \ of semi-Heyting algebras was introduced by H. P. Sankappanavar [13] as an abstraction of the variety of Heyting algebras. Semi-Heyting algebras are the algebraic models for a logic HsH, known as semi-intuitionistic logic, which is equivalent to the one defined by a Hilbert style calculus in Cornejo :9–25, 2011) [6]. In this article we introduce a Gentzen style sequent calculus GsH for the semi-intuitionistic logic whose associated logic GsH is the same as HsH. The advantage (...)

Export citation

My bibliography
32. Dual-Context Sequent Calculus and Strict Implication.Kentaro Kikuchi - 2002 - Mathematical Logic Quarterly 48 (1):87-92.
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.

Export citation

My bibliography
33. Berkeleys Kritik Am Leibniz´Schen Calculus.Horst Struve, Eva Müller-Hill & Ingo Witzke - 2015 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 46 (1):63-82.
One of the most famous critiques of the Leibnitian calculus is contained in the essay “The Analyst” written by George Berkeley in 1734. His key argument is those on compensating errors. In this article, we reconstruct Berkeley's argument from a systematical point of view showing that the argument is neither circular nor trivial, as some modern historians think. In spite of this well-founded argument, the critique of Berkeley is with respect to the calculus not a fundamental one. Nevertheless, (...)

Export citation

My bibliography
34. Is Leibnizian Calculus Embeddable in First Order Logic?Piotr Błaszczyk, Vladimir Kanovei, Karin U. Katz, Mikhail G. Katz, Taras Kudryk, Thomas Mormann & David Sherry - forthcoming - Foundations of Science:1-15.
To explore the extent of embeddability of Leibnizian infinitesimal calculus in first-order logic and modern frameworks, we propose to set aside ontological issues and focus on procedural questions. This would enable an account of Leibnizian procedures in a framework limited to FOL with a small number of additional ingredients such as the relation of infinite proximity. If, as we argue here, first order logic is indeed suitable for developing modern proxies for the inferential moves found in Leibnizian infinitesimal (...), then modern infinitesimal frameworks are more appropriate to interpreting Leibnizian infinitesimal calculus than modern Weierstrassian ones. (shrink)

Export citation

My bibliography
35. A Phenomenological Calculus for Anisotropic Systems.A. H. Louie & I. W. Richardson - 2005 - Axiomathes 16 (1-2):215-243.
The phenomenological calculus is a relational paradigm for complex systems, closely related in substance and spirit to Robert Rosen’s own approach. Its mathematical language is multilinear algebra. The epistemological exploration continues in this paper, with the expansion of the phenomenological calculus into the realm of anisotropy.

Export citation

My bibliography
36. A Sequent Calculus for Urn Logic.Rohan French - 2015 - Journal of Logic, Language and Information 24 (2):131-147.
Approximately speaking, an urn model for first-order logic is a model where the domain of quantification changes depending on the values of variables which have been bound by quantifiers previously. In this paper we introduce a model-changing semantics for urn-models, and then give a sequent calculus for urn logic by introducing formulas which can be read as saying that “after the individuals a1,..., an have been drawn, A is the case”.

Export citation

My bibliography
37. A Proof-Theoretic Treatment of Λ-Reduction with Cut-Elimination: Λ-Calculus as a Logic Programming Language.Michael Gabbay - 2011 - Journal of Symbolic Logic 76 (2):673 - 699.
We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic. We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).

Export citation

My bibliography
38. The Taming of Recurrences in Computability Logic Through Cirquent Calculus, Part II.Giorgi Japaridze - 2013 - Archive for Mathematical Logic 52 (1-2):213-259.
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation \${{\neg}}\$ , parallel conjunction \${{\wedge}}\$ , parallel disjunction \${{\vee}}\$ , branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (the previous) Part I containing preliminaries and a soundness proof, and (the present) Part II containing a completeness proof.

Export citation

My bibliography
39. Absolute Continuity and the Uniqueness of the Constructive Functional Calculus.Douglas Bridges & Hajime Ishihara - 1994 - Mathematical Logic Quarterly 40 (4):519-527.
The constructive functional calculus for a sequence of commuting selfadjoint operators on a separable Hilbert space is shown to be independent of the orthonormal basis used in its construction. The proof requires a constructive criterion for the absolute continuity of two positive measures in terms of test functions.

Export citation

My bibliography
40. The Foundations of Quantum Mechanics and the Evolution of the Cartan-Kähler Calculus.Jose G. Vargas - 2008 - Foundations of Physics 38 (7):610-647.
In 1960–1962, E. Kähler enriched É. Cartan’s exterior calculus, making it suitable for quantum mechanics (QM) and not only classical physics. His “Kähler-Dirac” (KD) equation reproduces the fine structure of the hydrogen atom. Its positron solutions correspond to the same sign of the energy as electrons.The Cartan-Kähler view of some basic concepts of differential geometry is presented, as it explains why the components of Kähler’s tensor-valued differential forms have three series of indices. We demonstrate the power of his (...) by developing for the electron’s and positron’s large components their standard Hamiltonian beyond the Pauli approximation, but without resort to Foldy-Wouthuysen transformations or ad hoc alternatives (positrons are not identified with small components in K ähler’s work). The emergence of negative energies for positrons in the Dirac theory is interpreted from the perspective of the KD equation. Hamiltonians in closed form (i.e. exact through a finite number of terms) are obtained for both large and small components when the potential is time-independent.A new but as yet modest new interpretation of QM starts to emerge from that calculus’ peculiarities, which are present even when the input differential form in the Kähler equation is scalar-valued. Examples are the presence of an extra spin term, the greater number of components of “wave functions” and the non-association of small components with antiparticles. Contact with geometry is made through a Kähler type equation pertaining to Clifford-valued differential forms. (shrink)

Export citation

My bibliography
41. The Taming of Recurrences in Computability Logic Through Cirquent Calculus, Part I.Giorgi Japaridze - 2013 - Archive for Mathematical Logic 52 (1-2):173-212.
This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation \${\neg}\$ , parallel conjunction \${\wedge}\$ , parallel disjunction \${\vee}\$ , branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (the present) Part I containing preliminaries and a soundness proof, and (the forthcoming) Part II containing a completeness proof.

Export citation

My bibliography
42. A Labelled Deductive System for Relational Semantics of the Lambek Calculus.Miroslawa Kolowska‐Gawiejnowicz - 1999 - Mathematical Logic Quarterly 45 (1):51-58.
We present a labelled version of Lambek Calculus without unit, and we use it to prove a completeness theorem for Lambek Calculus with respect to some relational semantics.

Export citation

My bibliography
43. Valuation Semantics for Intuitionic Propositional Calculus and Some of its Subcalculi.Andréa Lopari? - 2011 - Principia 14 (1):125-33.
In this paper, we present valuation semantics for the Propositional Intuitionistic Calculus (also called Heyting Calculus) and three important subcalculi: the Implicative, the Positive and the Minimal Calculus (also known as Kolmogoroff or Johansson Calculus). Algorithms based in our definitions yields decision methods for these calculi. DOI:10.5007/1808-1711.2010v14n1p125.

Export citation

My bibliography
44. Reduction Rules for Intuitionistic {{Lambda}{Rho}}-Calculus.Ken-Etsu Fujita, Ryo Kashima, Yuichi Komori & Naosuke Matsuda - 2015 - Studia Logica 103 (6):1225-1244.
The third author gave a natural deduction style proof system called the \-calculus for implicational fragment of classical logic in. In -calculus, 2015, Post-proceedings of the RIMS Workshop “Proof Theory, Computability Theory and Related Issues”, to appear), the fourth author gave a natural subsystem “intuitionistic \-calculus” of the \-calculus, and showed the system corresponds to intuitionistic logic. The proof is given with tree sequent calculus, but is complicated. In this paper, we introduce some reduction rules (...)

Export citation

My bibliography
45. Cut-Rule Axiomatization of the Syntactic Calculus L.Wojciech Zielonka - 2001 - Journal of Logic, Language and Information 10 (2):339-352.
In Zielonka (1981a, 1989), I found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It was proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek, 1958), sequent antecedents are non empty. By dropping this restriction, we obtain the variant L 0 of L. This modification, introduced in the early 1980s (see, (...)

Export citation

My bibliography
46. Effective Cut-Elimination for a Fragment of Modal Mu-Calculus.Grigori Mints - 2012 - Studia Logica 100 (1-2):279-287.
A non-effective cut-elimination proof for modal mu-calculus has been given by G. Jäger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M 1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M 1 without restriction to positive sequents.

Export citation

My bibliography
47. A Concrete Categorical Model for the Lambek Syntactic Calculus.Marcelo Da Silva Corrêa & Edward Hermann Haeusler - 1997 - Mathematical Logic Quarterly 43 (1):49-59.
We present a categorical/denotational semantics for the Lambek Syntactic Calculus , indeed for a λlD-typed version Curry-Howard isomorphic to it. The main novelty of our approach is an abstract noncommutative construction with right and left adjoints, called sequential product. It is defined through a hierarchical structure of categories reflecting the implicit permission to sequence expressions and the inductive construction of compound expressions. We claim that Lambek's noncommutative product corresponds to a noncommutative bi-endofunctor into a category, which encloses all categories (...)

Export citation

My bibliography
48. An Axiomatisation of a Pure Calculus of Names.Piotr Kulicki - 2012 - Studia Logica 100 (5):921-946.
A calculus of names is a logical theory describing relations between names. By a pure calculus of names we mean a quantifier-free formulation of such a theory, based on classical propositional calculus. An axiomatisation of a pure calculus of names is presented and its completeness is discussed. It is shown that the axiomatisation is complete in three different ways: with respect to a set theoretical model, with respect to Leśniewski's Ontology and in a sense defined with (...)

Export citation

My bibliography
49. A Cut-Free Gentzen Formulation of Basic Propositional Calculus.Kentaro Kikuchi & Katsumi Sasaki - 2003 - Journal of Logic, Language and Information 12 (2):213-225.
We introduce a Gentzen style formulation of Basic Propositional Calculus(BPC), the logic that is interpreted in Kripke models similarly tointuitionistic logic except that the accessibility relation of eachmodel is not necessarily reflexive. The formulation is presented as adual-context style system, in which the left hand side of a sequent isdivided into two parts. Giving an interpretation of the sequents inKripke models, we show the soundness and completeness of the system withrespect to the class of Kripke models. The cut-elimination theorem (...)