21 found
Order:
  1. A Note on Harmony.Nissim Francez & Roy Dyckhoff - 2012 - Journal of Philosophical Logic 41 (3):613-628.
    In the proof-theoretic semantics approach to meaning, harmony , requiring a balance between introduction-rules (I-rules) and elimination rules (E-rules) within a meaning conferring natural-deduction proof-system, is a central notion. In this paper, we consider two notions of harmony that were proposed in the literature: 1. GE-harmony , requiring a certain form of the E-rules, given the form of the I-rules. 2. Local intrinsic harmony : imposes the existence of certain transformations of derivations, known as reduction and expansion . We propose (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   33 citations  
  2.  30
    A. S. Troelstra and H. Schwichtenberg. Basic proof theory. Second edition of jsl lxiii 1605. Cambridge tracts in theoretical computer science, no. 43. cambridge university press, cambridge, new York, etc., 2000, XII + 417 pp.Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280-280.
  3. Proof-Theoretic Semantics for Subsentential Phrases.Nissim Francez, Roy Dyckhoff & Gilad Ben-Avi - 2010 - Studia Logica 94 (3):381-401.
    The paper briefly surveys the sentential proof-theoretic semantics for fragment of English. Then, appealing to a version of Frege’s context-principle (specified to fit type-logical grammar), a method is presented for deriving proof-theoretic meanings for sub-sentential phrases, down to lexical units (words). The sentential meaning is decomposed according to the function-argument structure as determined by the type-logical grammar. In doing so, the paper presents a novel proof-theoretic interpretation of simple type, replacing Montague’s model-theoretic type interpretation (in arbitrary Henkin models). The domains (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   24 citations  
  4. Proof-theoretic semantics for a natural language fragment.Nissim Francez & Roy Dyckhoff - 2010 - Linguistics and Philosophy 33 (6):447-477.
    The paper presents a proof-theoretic semantics (PTS) for a fragment of natural language, providing an alternative to the traditional model-theoretic (Montagovian) semantics (MTS), whereby meanings are truth-condition (in arbitrary models). Instead, meanings are taken as derivability-conditions in a dedicated natural-deduction (ND) proof-system. This semantics is effective (algorithmically decidable), adhering to the meaning as use paradigm, not suffering from several of the criticisms formulated by philosophers of language against MTS as a theory of meaning. In particular, Dummett’s manifestation argument does not (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   35 citations  
  5. Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
    Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   29 citations  
  6.  62
    Geometrisation of first-order logic.Roy Dyckhoff & Sara Negri - 2015 - Bulletin of Symbolic Logic 21 (2):123-163.
    That every first-order theory has a coherent conservative extension is regarded by some as obvious, even trivial, and by others as not at all obvious, but instead remarkable and valuable; the result is in any case neither sufficiently well-known nor easily found in the literature. Various approaches to the result are presented and discussed in detail, including one inspired by a problem in the proof theory of intermediate logics that led us to the proof of the present paper. It can (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  7.  90
    Contraction-free sequent calculi for intuitionistic logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.
  8. Some Remarks on Proof-Theoretic Semantics.Roy Dyckhoff - 2016 - In Peter Schroeder-Heister & Thomas Piecha (eds.), Advances in Proof-Theoretic Semantics. Springer Verlag.
     
    Export citation  
     
    Bookmark   7 citations  
  9.  23
    Indirect Proof and Inversions of Syllogisms.Roy Dyckhoff - 2019 - Bulletin of Symbolic Logic 25 (2):196-207.
    By considering the new notion of theinversesof syllogisms such asBarbaraandCelarent, we show how the rule ofIndirect Proof, in the form (no multiple or vacuous discharges) used by Aristotle, may be dispensed with, in a system comprising four basic rules of subalternation or conversion and six basic syllogisms.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  10. Analyticity, Balance and Non-admissibility of Cut in Stoic Logic.Susanne Bobzien & Roy Dyckhoff - 2019 - Studia Logica 107 (2):375-397.
    This paper shows that, for the Hertz–Gentzen Systems of 1933, extended by a classical rule T1 and using certain axioms, all derivations are analytic: every cut formula occurs as a subformula in the cut’s conclusion. Since the Stoic cut rules are instances of Gentzen’s Cut rule of 1933, from this we infer the decidability of the propositional logic of the Stoics. We infer the correctness for this logic of a “relevance criterion” and of two “balance criteria”, and hence that a (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11. Decision methods for linearly ordered Heyting algebras.Sara Negri & Roy Dyckhoff - 2006 - Archive for Mathematical Logic 45 (4):411-422.
    The decision problem for positively quantified formulae in the theory of linearly ordered Heyting algebras is known, as a special case of work of Kreisel, to be solvable; a simple solution is here presented, inspired by related ideas in Gödel-Dummett logic.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  12. Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
    We describe a sequent calculus, based on work of Herbelin, of which the cut-free derivations are in 1-1 correspondence with the normal natural deduction proofs of intuitionistic logic. We present a simple proof of Herbelin's strong cut-elimination theorem for the calculus, using the recursive path ordering theorem of Dershowitz.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  13.  74
    Admissibility of structural rules for contraction-free systems of intuitionistic logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
    We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14. Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic.Roy Dyckhoff & Sara Negri - 2000 - Journal of Symbolic Logic 65 (4):1499-1518.
    We give a direct proof of admissibility of cut and contraction for the contraction-free sequent calculus G4ip for intuitionistic propositional logic and for a corresponding multi-succedent calculus: this proof extends easily in the presence of quantifiers, in contrast to other, indirect, proofs. i.e., those which use induction on sequent weight or appeal to admissibility of rules in other calculi.
     
    Export citation  
     
    Bookmark  
  15.  20
    Contraction-free sequent calculi for intuitionistic logic: A correction.Roy Dyckhoff - 2018 - Journal of Symbolic Logic 83 (4):1680-1682.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  16. REVIEWS-Basic proof theory.A. Troelstra, H. Schwichtenberg & Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280.
  17.  22
    A. S. Troelstra and H. Schwichtenberg. Basic proof theory. Second edition of jsl lxiii 1605. Cambridge tracts in theoretical computer science, no. 43. cambridge university press, cambridge, new York, etc., 2000, XII + 417 pp. [REVIEW]Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280-280.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  18.  4
    Extensions of Logic Programming: 4th International Workshop, Elp '93, St Andrews, U.K., March 29-April 1, 1993 : Proceedings.Roy Dyckhoff - 1994 - Springer.
    "The papers in this volume are extended versions of presentations at the fourth International Workshop on Extensions of Logic Programming, held at the University of St Andrews, March/April 1993. Among the topics covered in the volume are: defintional reflection and completion, modules in lambda-Prolog, representation of logics as partial inductive definitions, non-procedural logic programming, knowledge representation, contradiction avoidance, disjunctive databases, strong negation, linear logic programming, proof theory and regular search spaces, finite sets and constraint logic programming, search-space pruning and universal (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  19.  7
    Extensions of Logic Programming: 5th International Workshop, Elp '96, Leipzig, Germany, March 28 - 30, 1996. Proceedings.Roy Dyckhoff, Heinrich Herre & Peter Schroeder-Heister - 1996 - Springer Verlag.
    A major strategy to reduce transport congestion and other social costs of transport is to ensure that travellers make the best decisions, based on real time information. A wide range of technological systems have been developed to provide this information, but little is known about how travellers actually respond to it. This book offers an overview of various transport telematics options and provides an appropriate methodological framework, followed by a presentation of results from actual applications of these telematics systems from (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  20.  20
    Review: A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory. [REVIEW]Roy Dyckhoff - 1998 - Journal of Symbolic Logic 63 (4):1605-1606.
  21.  29
    A. S. Troelstra and H. Schwichtenberg. Basic proof theory. Cambridge tracts in theoretical computer science, no. 43. Cambridge University Press, Cambridge, New York, and Oakleigh, Victoria, 1996, xi + 343 pp. [REVIEW]Roy Dyckhoff - 1998 - Journal of Symbolic Logic 63 (4):1605-1606.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark