17 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 (7 more)  
     
    Export citation  
     
    My bibliography   16 citations  
  2. 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 (7 more)  
     
    Export citation  
     
    My bibliography  
  3. 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 (9 more)  
     
    Export citation  
     
    My bibliography   10 citations  
  4.  27
    Proof Analysis in Intermediate Logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1-2):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  
     
    My bibliography   6 citations  
  5.  23
    Contraction-Free Sequent Calculi for Intuitionistic Logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.
  6.  38
    Positive Logic with Adjoint Modalities: Proof Theory, Semantics, and Reasoning About Information.Mehrnoosh Sadrzadeh & Roy Dyckhoff - 2010 - Review of Symbolic Logic 3 (3):351-373.
    We consider a simple modal logic whose nonmodal part has conjunction and disjunction as connectives and whose modalities come in adjoint pairs, but are not in general closure operators. Despite absence of negation and implication, and of axioms corresponding to the characteristic axioms of T , S4 , and S5 , such logics are useful, as shown in previous work by Baltag, Coecke, and the first author, for encoding and reasoning about information and misinformation in multiagent systems. For the propositional-only (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  7.  15
    Decision Methods for Linearly Ordered Heyting Algebras.Sara Negri & Roy Dyckhoff - 2005 - 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 (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  8.  60
    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 (8 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  9.  3
    Geometrisation of First-Order Logic.Roy Dyckhoff & Sara Negri - 2015 - Bulletin of Symbolic Logic 21 (2):123-163.
  10.  22
    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 (7 more)  
     
    Export citation  
     
    My bibliography  
  11.  4
    Review: A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory. [REVIEW]Roy Dyckhoff - 1998 - Journal of Symbolic Logic 63 (4):1605-1606.
  12. 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  
     
    Export citation  
     
    My bibliography  
  13. Basic Proof Theory.Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280.
  14. Extensions of Logic Programming 4th International Workshop, Elp '93, St Andrews, U.K., March 29-April 1, 1993 : Proceedings'. [REVIEW]Roy Dyckhoff & Elp '93 - 1994
     
    Export citation  
     
    My bibliography  
  15. Extensions of Logic Programming 5th International Workshop, Elp '96, Leipzig, Germany, March 28-30, 1996 : Proceedings'.Roy Dyckhoff, Heinrich Herre & Peter Joseph Schroeder-Heister - 1996
     
    Export citation  
     
    My bibliography  
  16. Troelstra A. S. And Schwichtenberg H.. 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 (2 more)  
     
    Export citation  
     
    My bibliography  
  17. REVIEWS-Basic Proof Theory.A. Troelstra, H. Schwichtenberg & Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280.
     
    Export citation  
     
    My bibliography