19 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   17 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   10 citations  
  3.  59
    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   9 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 (9 more)  
     
    Export citation  
     
    My bibliography   11 citations  
  5.  9
    Analyticity, Balance and Non-Admissibility of Cut in Stoic Logic.Susanne Bobzien & Roy Dyckhoff - 2018 - Studia Logica:1-23.
    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 (2 more)  
     
    Export citation  
     
    My bibliography  
  6.  8
    Analyticity, Balance and Non-Admissibility of Cut in Stoic Logic.Susanne Bobzien & Roy Dyckhoff - forthcoming - Studia Logica:1-23.
    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 (2 more)  
     
    Export citation  
     
    My bibliography  
  7.  24
    Contraction-Free Sequent Calculi for Intuitionistic Logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.
  8.  10
    Geometrisation of First-Order Logic.Roy Dyckhoff & Sara Negri - 2015 - Bulletin of Symbolic Logic 21 (2):123-163.
  9.  47
    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  
  10.  47
    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  
  11.  62
    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  
  12.  8
    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.  31
    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  
  14.  4
    Review: A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory. [REVIEW]Roy Dyckhoff - 1998 - Journal of Symbolic Logic 63 (4):1605-1606.
  15.  2
    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  
  16. Basic Proof Theory.Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280.
  17. 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  
  18. 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  
  19. REVIEWS-Basic Proof Theory.A. Troelstra, H. Schwichtenberg & Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280.
     
    Export citation  
     
    My bibliography