13 found
Sort by:
  1. Roy Dyckhoff & Sara Negri (2012). Proof Analysis in Intermediate Logics. 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 (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. Nissim Francez & Roy Dyckhoff (2012). A Note on Harmony. 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 (8 more)  
     
    My bibliography  
     
    Export citation  
  3. Roy Dyckhoff (2010). Positive Logic with Adjoint Modalities: Proof Theory, Semantics, and Reasoning About Information. 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 (e.g.) 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 fragment of (...)
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  4. Nissim Francez & Roy Dyckhoff (2010). Proof-Theoretic Semantics for a Natural Language Fragment. 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)  
     
    My bibliography  
     
    Export citation  
  5. Nissim Francez, Roy Dyckhoff & Gilad Ben-Avi (2010). Proof-Theoretic Semantics for Subsentential Phrases. 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 (8 more)  
     
    My bibliography  
     
    Export citation  
  6. Mehrnoosh Sadrzadeh & Roy Dyckhoff (2010). Positive Logic with Adjoint Modalities: Proof Theory, Semantics, and Reasoning About Information. Review of Symbolic Logic 3 (3):351-373.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  7. Sara Negri & Roy Dyckhoff (2006). Decision Methods for Linearly Ordered Heyting Algebras. 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.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  8. Roy Dyckhoff & Heinrich Wansing (2001). Editorial. Studia Logica 69 (1).
    Direct download  
     
    My bibliography  
     
    Export citation  
  9. A. Troelstra, H. Schwichtenberg & Roy Dyckhoff (2001). REVIEWS-Basic Proof Theory. Bulletin of Symbolic Logic 7 (2):280.
     
    My bibliography  
     
    Export citation  
  10. Roy Dyckhoff & Sara Negri (2000). Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic. 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 (6 more)  
     
    My bibliography  
     
    Export citation  
  11. Roy Dyckhoff (1998). Review: A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory. [REVIEW] Journal of Symbolic Logic 63 (4):1605-1606.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  12. Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. 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)  
     
    My bibliography  
     
    Export citation  
  13. Roy Dyckhoff (1992). Contraction-Free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic 57 (3):795-807.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation