54 found
Order:
  1.  13
    Gödel on Deduction.Kosta Došen & Miloš Adžić - forthcoming - Studia Logica:1-21.
    This is an examination, a commentary, of links between some philosophical views ascribed to Gödel and general proof theory. In these views deduction is of central concern not only in predicate logic, but in set theory too, understood from an infinitistic ideal perspective. It is inquired whether this centrality of deduction could also be kept in the intensional logic of concepts whose building Gödel seems to have taken as the main task of logic for the future.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  2. Identity of Proofs Based on Normalization and Generality.Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (4):477-503.
    Some thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal form in natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the same generality if after generalizing maximally (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  3.  10
    Gödel’s Natural Deduction.Kosta Došen & Miloš Adžić - 2018 - Studia Logica 106 (2):397-415.
    This is a companion to a paper by the authors entitled “Gödel on deduction”, which examined the links between some philosophical views ascribed to Gödel and general proof theory. When writing that other paper, the authors were not acquainted with a system of natural deduction that Gödel presented with the help of Gentzen’s sequents, which amounts to Jaśkowski’s natural deduction system of 1934, and which may be found in Gödel’s unpublished notes for the elementary logic course he gave in 1939 (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  4.  46
    Logical Constants as Punctuation Marks.Kosta Došen - 1989 - Notre Dame Journal of Formal Logic 30 (3):362-381.
  5.  15
    Gödel’s Notre Dame Course.Miloš Adžić & Kosta Došen - 2016 - Bulletin of Symbolic Logic 22 (4):469-481.
    This is a companion to a paper by the authors entitled “Gödel’s natural deduction,” which presented and made comments about the natural deduction system in Gödel’s unpublished notes for the elementary logic course he gave at the University of Notre Dame in 1939. In that earlier paper, which was itself a companion to a paper that examined the links between some philosophical views ascribed to Gödel and general proof theory, one can find a brief summary of Gödel’s notes for the (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6.  26
    Sequent-Systems and Groupoid Models. I.Kosta Došen - 1988 - Studia Logica 47 (4):353 - 385.
    The purpose of this paper is to connect the proof theory and the model theory of a family of propositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related toBCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the structural (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   19 citations  
  7.  56
    Models for Normal Intuitionistic Modal Logics.Milan Božić & Kosta Došen - 1984 - Studia Logica 43 (3):217 - 245.
    Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given for analogues of the modal systemK based on Heyting's prepositional logic. It is shown that these two relations can combine with each other in various ways. Soundness and completeness are proved for systems with only the necessity operator, or only the possibility operator, or both. Embeddings in modal systems with several modal operators, based on classical propositional logic, are also considered. This paper lays the ground for (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  8. Uniqueness, Definability and Interpolation.Kosta Došen & Peter Schroeder-Heister - 1988 - Journal of Symbolic Logic 53 (2):554-570.
  9.  90
    Models of Deduction.Kosta Dosen - 2006 - Synthese 148 (3):639-657.
    In standard model theory, deductions are not the things one models. But in general proof theory, in particular in categorial proof theory, one finds models of deductions, and the purpose here is to motivate a simple example of such models. This will be a model of deductions performed within an abstract context, where we do not have any particular logical constant, but something underlying all logical constants. In this context, deductions are represented by arrows in categories involved in a general (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  10.  10
    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 types of (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  11.  37
    The First Axiomatization of Relevant Logic.Kosta Došen - 1992 - Journal of Philosophical Logic 21 (4):339 - 356.
    This is a review, with historical and critical comments, of a paper by I. E. Orlov from 1928, which gives the oldest known axiomatization of the implication-negation fragment of the relevant logic R. Orlov's paper also foreshadows the modal translation of systems with an intuitionistic negation into S4-type extensions of systems with a classical, involutive, negation. Orlov introduces the modal postulates of S4 before Becker, Lewis and Gödel. Orlov's work, which seems to be nearly completely ignored, is related to the (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  12.  35
    Models for Stronger Normal Intuitionistic Modal Logics.Kosta Došen - 1985 - Studia Logica 44 (1):39 - 70.
    This paper, a sequel to Models for normal intuitionistic modal logics by M. Boi and the author, which dealt with intuitionistic analogues of the modal system K, deals similarly with intuitionistic analogues of systems stronger than K, and, in particular, analogues of S4 and S5. For these prepositional logics Kripke-style models with two accessibility relations, one intuitionistic and the other modal, are given, and soundness and completeness are proved with respect to these models. It is shown how the holding of (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  13.  29
    Sequent-Systems for Modal Logic.Kosta Došen - 1985 - Journal of Symbolic Logic 50 (1):149-168.
    The purpose of this work is to present Gentzen-style formulations of S5 and S4 based on sequents of higher levels. Sequents of level 1 are like ordinary sequents, sequents of level 1 have collections of sequents of level 1 on the left and right of the turnstile, etc. Rules for modal constants involve sequents of level 2, whereas rules for customary logical constants of first-order logic with identity involve only sequents of level 1. A restriction on Thinning on the right (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  14. Substructural Logics.Peter Joseph Schroeder-Heister, Kosta Dosen & Seminar Für Natürlich-Sprachliche Systeme - 1993
  15.  54
    Modal Translations in Substructural Logics.Kosta Došen - 1992 - Journal of Philosophical Logic 21 (3):283 - 336.
    Substructural logics are logics obtained from a sequent formulation of intuitionistic or classical logic by rejecting some structural rules. The substructural logics considered here are linear logic, relevant logic and BCK logic. It is proved that first-order variants of these logics with an intuitionistic negation can be embedded by modal translations into S4-type extensions of these logics with a classical, involutive, negation. Related embeddings via translations like the double-negation translation are also considered. Embeddings into analogues of S4 are obtained with (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  16.  8
    Sequent-Systems and Groupoid Models. II.Kosta Došen - 1989 - Studia Logica 48 (1):41 - 65.
    The purpose of this paper is to connect the proof theory and the model theory of a family of prepositional logics weaker than Heyting's. This family includes systems analogous to the Lambek calculus of syntactic categories, systems of relevant logic, systems related to BCK algebras, and, finally, Johansson's and Heyting's logic. First, sequent-systems are given for these logics, and cut-elimination results are proved. In these sequent-systems the rules for the logical operations are never changed: all changes are made in the (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  17.  9
    Bicartesian Coherence.Kosta Došen & Zoran Petrić - 2002 - Studia Logica 71 (3):331-353.
    Coherence is demonstrated for categories with binary products and sums, but without the terminal and the initial object, and without distribution. This coherence amounts to the existence of a faithful functor from a free category with binary products and sums to the category of relations on finite ordinals. This result is obtained with the help of proof-theoretic normalizing techniques. When the terminal object is present, coherence may still be proved if of binary sums we keep just their bifunctorial properties. It (...)
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  18.  18
    A Brief Survey of Frames for the Lambek Calculus.Kosta Došen - 1992 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 38 (1):179-187.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  19.  12
    A Completeness Theorem for the Lambek Calculus of Syntactic Categories.Kosta Došen - 1985 - Mathematical Logic Quarterly 31 (14‐18):235-241.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  20.  33
    Deductive Completeness.Kosta Došen - 1996 - Bulletin of Symbolic Logic 2 (3):243-283.
    This is an exposition of Lambek's strengthening and generalization of the deduction theorem in categories related to intuitionistic propositional logic. Essential notions of category theory are introduced so as to yield a simple reformulation of Lambek's Functional Completeness Theorem, from which its main consequences can be readily drawn. The connections of the theorem with combinatory logic, and with modal and substructural logics, are briefly considered at the end.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  21.  53
    Modal Logic as Metalogic.Kosta Došen - 1992 - Journal of Logic, Language and Information 1 (3):173-201.
    The goal of this paper is to show how modal logic may be conceived as recording the derived rules of a logical system in the system itself. This conception of modal logic was propounded by Dana Scott in the early seventies. Here, similar ideas are pursued in a context less classical than Scott's.First a family of propositional logical systems is considered, which is obtained by gradually adding structural rules to a variant of the nonassociative Lambek calculus. In this family one (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  22.  15
    Coherence in Linear Predicate Logic.Kosta Došen & Zoran Petrić - 2009 - Annals of Pure and Applied Logic 158 (1-2):125-153.
    Coherence with respect to Kelly–Mac Lane graphs is proved for categories that correspond to the multiplicative fragment without constant propositions of classical linear first-order predicate logic without or with mix. To obtain this result, coherence is first established for categories that correspond to the multiplicative conjunction–disjunction fragment with first-order quantifiers of classical linear logic, a fragment lacking negation. These results extend results of [K. Došen, Z. Petrić, Proof-Theoretical Coherence, KCL Publications , London, 2004 ; K. Došen, Z. Petrić, Proof-Net Categories, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  23.  12
    Coherence for Star-Autonomous Categories.Kosta Došen & Zoran Petrić - 2006 - Annals of Pure and Applied Logic 141 (1):225-242.
    This paper presents a coherence theorem for star-autonomous categories exactly analogous to Kelly and Mac Lane’s coherence theorem for symmetric monoidal closed categories. The proof of this theorem is based on a categorial cut-elimination result, which is presented in some detail.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  24.  16
    Associativity as Commutativity.Kosta Došen & Zoran Petrć - 2006 - Journal of Symbolic Logic 71 (1):217 - 226.
    It is shown that coherence conditions for monoidal categories concerning associativity are analogous to coherence conditions for symmetric strictly monoidal categories, where associativity arrows are identities. Mac Lane's pentagonal coherence condition for associativity is decomposed into conditions concerning commutativity, among which we have a condition analogous to naturality and a degenerate case of Mac Lane's hexagonal condition for commutativity. This decomposition is analogous to the derivation of the Yang-Baxter equation from Mac Lane's hexagon and the naturality of commutativity. The pentagon (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  25. Proof-Net Categories.Kosta Dosen, Zoran Petric & Lutz Strassburger - 2008 - Bulletin of Symbolic Logic 14 (2):268-271.
     
    Export citation  
     
    Bookmark   1 citation  
  26.  38
    A Reduction of Classical Propositional Logic to the Conjunction-Negation Fragment of an Intuitionistic Relevant Logic.Kosta Došen - 1981 - Journal of Philosophical Logic 10 (4):399 - 408.
  27.  20
    Duality Between Modal Algebras and Neighbourhood Frames.Kosta Došen - 1989 - Studia Logica 48 (2):219 - 234.
    This paper presents duality results between categories of neighbourhood frames for modal logic and categories of modal algebras (i.e. Boolean algebras with an additional unary operation). These results extend results of Goldblatt and Thomason about categories of relational frames for modal logic.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  28.  25
    Bicartesian Coherence.Kosta Došen & Zoran Petrić - 2002 - Studia Logica 71 (3):331 - 353.
    Coherence is demonstrated for categories with binary products and sums, but without the terminal and the initial object, and without distribution. This coherence amounts to the existence of a faithful functor from a free category with binary products and sums to the category of relations on finite ordinals. This result is obtained with the help of proof-theoretic normalizing techniques. When the terminal object is present, coherence may still be proved if of binary sums we keep just their bifunctorial properties. It (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  29.  17
    A Completeness Theorem for the Lambek Calculus of Syntactic Categories.Kosta Došen - 1985 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 31 (14-18):235-241.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  30.  18
    A Note on Gentzen's Decision Procedure for Intuitionistic Propositional Logic.Kosta Došen - 1987 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 33 (5):453-456.
  31.  4
    Representing Conjunctive Deductions by Disjunctive Deductions.Kosta Došen & Zoran Petrić - 2017 - Review of Symbolic Logic 10 (1):145-157.
    Direct download  
     
    Export citation  
     
    Bookmark  
  32.  21
    Cartesian Isomorphisms Are Symmetric Monoidal: A Justification of Linear Logic.Kosta Došen & Zoran Petrić - 1999 - Journal of Symbolic Logic 64 (1):227-242.
    It is proved that all the isomorphisms in the cartesian category freely generated by a set of objects (i.e., a graph without arrows) can be written in terms of arrows from the symmetric monoidal category freely generated by the same set of objects. This proof yields an algorithm for deciding whether an arrow in this free cartesian category is an isomorphism.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  33.  9
    An Intuitionistic Sheffer Function.Kosta Došen - 1985 - Notre Dame Journal of Formal Logic 26 (4):479-482.
  34.  13
    Ancestral Kripke Models and Nonhereditary Kripke Models for the Heyting Propositional Calculus.Kosta Došen - 1991 - Notre Dame Journal of Formal Logic 32 (4):580-597.
  35. Normal Modal Logics In Which The Heyting Propositional Calculus Can Be Embedded.Kosta Dosen - 1988 - Bulletin of the Section of Logic 17 (1):23-30.
     
    Export citation  
     
    Bookmark   2 citations  
  36.  13
    Axiomatizations of Intuitionistic Double Negation.Milan Bozic & Kosta Došen - 1983 - Bulletin of the Section of Logic 12 (2):99-102.
    We investigate intuitionistic propositional modal logics in which a modal operator is equivalent to intuitionistic double negation. Whereas ¬¬ is divisible into two negations, is a single indivisible operator. We shall first consider an axiomatization of the Heyting propositional calculus H, with the connectives →,∧,∨ and ¬, extended with . This system will be called Hdn . Next, we shall consider an axiomatization of the fragment of H without ¬ extended with . This system will be called Hdn + . (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  37. Higher-Order Sequent-System for Intuitionistic Modal Logic.Kosta Dosen - 1985 - Bulletin of the Section of Logic 14 (4):140-142.
    In [2] we have presented sequent formulations of the modal logics S5 and S4 based on sequents of higher levels: sequents of level 1 are like ordinary sequents, sequents of level 2 have collections of sequents of level 1 on the left and right of the turnstile, etc. The rules we gave for modal constants involved sequents of level 2, whereas rules for other customary logical constants of first–order logic involved only sequents of level 1. Here we show starting from (...)
     
    Export citation  
     
    Bookmark  
  38.  2
    Modal Functional Completeness.Kosta Dosen & Zoran Petric - 1996 - In H. Wansing (ed.), Proof Theory of Modal Logic. Kluwer Academic Publishers.
  39.  13
    Review: Greg Restall, An Introduction to Substructural Logics. [REVIEW]Kosta Dosen - 2001 - Bulletin of Symbolic Logic 7 (4):527-530.
  40.  11
    Cut Elimination in Adjuncion.Kosta Došen - 1999 - Bulletin of the Section of Logic 28 (2):61-73.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  41.  11
    Restall Greg. An Introduction to Substructural Logics. Routledge, London and New York 2000, Xiv+ 381 Pp. [REVIEW]Kosta Došen - 2001 - Bulletin of Symbolic Logic 7 (4):527-530.
    Direct download  
     
    Export citation  
     
    Bookmark  
  42.  12
    Equality of Proofs for Linear Equality.Kosta Došen & Zoran Petrić - 2008 - Archive for Mathematical Logic 47 (6):549-565.
    This paper is about equality of proofs in which a binary predicate formalizing properties of equality occurs, besides conjunction and the constant true proposition. The properties of equality in question are those of a preordering relation, those of an equivalence relation, and other properties appropriate for an equality relation in linear logic. The guiding idea is that equality of proofs is induced by coherence, understood as the existence of a faithful functor from a syntactical category into a category whose arrows (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  43.  5
    On Sets of Premises.Kosta Došen - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. De Gruyter. pp. 151-162.
    Direct download  
     
    Export citation  
     
    Bookmark  
  44.  6
    2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium'02.Lev D. Beklemishev, Stephen Cook, Olivier Lessmann, Simon Thomas, Jeremy Avigad, Arnold Beckmann, Tim Carlson, Robert L. Constable & Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (1):71.
  45.  6
    Syntax for Split Preorders.Kosta Došen & Zoran Petrić - 2013 - Annals of Pure and Applied Logic 164 (4):443-481.
    A split preorder is a preordering relation on the disjoint union of two sets, which function as source and target when one composes split preorders. The paper presents by generators and equations the category SplPre, whose arrows are the split preorders on the disjoint union of two finite ordinals. The same is done for the subcategory Gen of SplPre, whose arrows are equivalence relations, and for the category Rel, whose arrows are the binary relations between finite ordinals, and which has (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  46.  4
    An Introduction to Substructural Logics.Kosta Došen - 2001 - Bulletin of Symbolic Logic 7 (4):527-530.
  47.  7
    Addenda and Corrigenda to "Sequent-Systems and Groupoid Models".Kosta Došen - 1990 - Studia Logica 49 (4):614 -.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  48.  6
    Isomorphic Formulae in Classical Propositional Logic.Kosta Došen & Zoran Petrić - 2012 - Mathematical Logic Quarterly 58 (1):5-17.
    Isomorphism between formulae is defined with respect to categories formalizing equality of deductions in classical propositional logic and in the multiplicative fragment of classical linear propositional logic caught by proof nets. This equality is motivated by generality of deductions. Characterizations are given for pairs of isomorphic formulae, which lead to decision procedures for this isomorphism.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  49.  6
    Rudimentary Kripke Models for the Intuitionistic Propositional Calculus.Kosta Došen - 1993 - Annals of Pure and Applied Logic 62 (1):21-49.
    It is shown that the intuitionistic propositional calculus is sound and complete with respect to Kripke-style models that are not quasi-ordered. These models, called rudimentary Kripke models, differ from the ordinary intuitionistic Kripke models by making fewer assumptions about the underlying frames, but have the same conditions for valuations. However, since accessibility between points in the frames need not be reflexive, we have to assume, besides the usual intuitionistic heredity, the converse of heredity, which says that if a formula holds (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  50.  7
    A Note on the Law of Identity and the Converse Parry Property.Kosta Došen - 1978 - Notre Dame Journal of Formal Logic 19 (1):174-176.
1 — 50 / 54