David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Studia Logica 63 (1):85-119 (1999)
For each regular cardinal , we set up three systems of infinitary type logic, in which the length of the types and the length of the typed syntactical constructs are . For a fixed , these three versions are, in the order of increasing strength: the local system (), the global system g() (the difference concerns the conditions on eigenvariables) and the -system () (which has anti-selection terms or Hilbertian -terms, and no conditions on eigenvariables). A full cut elimination theorem is proved for the local systems, and about the -systems we prove that they admit cut-free proofs for sequents in the -free language common to the local and global systems. These two results follow from semantic completeness proofs. Thus every sequent provable in a global system has a cut-free proof in the corresponding -systems. It is, however, an open question whether the global systems in themselves admit cut elimination.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Ryo Kashima (1994). Cut-Free Sequent Calculi for Some Tense Logics. Studia Logica 53 (1):119 - 135.
George Tourlakis (2010). On the Proof-Theory of Two Formalisations of Modal First-Order Logic. Studia Logica 96 (3):349-373.
Francesco Belardinelli, Peter Jipsen & Hiroakira Ono (2004). Algebraic Aspects of Cut Elimination. Studia Logica 77 (2):209 - 240.
Arnon Avron, Jonathan Ben-Naim & Beata Konikowska (2007). Cut-Free Ordinary Sequent Calculi for Logics Having Generalized Finite-Valued Semantics. Logica Universalis 1 (1):41-70.
Grigori Mints (1997). Indexed Systems of Sequents and Cut-Elimination. Journal of Philosophical Logic 26 (6):671-696.
Rajeev Goré (1994). Cut-Free Sequent and Tableau Systems for Propositional Diodorean Modal Logics. Studia Logica 53 (3):433 - 457.
Rineke Verbrugge, Gerard Renardel de Lavalette & Barteld Kooi, Hybrid Logics with Infinitary Proof Systems.
Added to index2009-01-28
Total downloads3 ( #294,094 of 1,101,544 )
Recent downloads (6 months)2 ( #178,305 of 1,101,544 )
How can I increase my downloads?