Search results for 'Elimination' (try it on Scholar)

1000+ found
Order:
  1.  5
    Christoph Benzmüller (forthcoming). Cut-Elimination for Quantified Conditional Logic. Journal of Philosophical Logic:1-21.
    A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  2.  9
    Bryan Renne (2012). Multi-Agent Justification Logic: Communication and Evidence Elimination. [REVIEW] Synthese 185 (S1):43-82.
    This paper presents a logic combining Dynamic Epistemic Logic, a framework for reasoning about multi-agent communication, with a new multi-agent version of Justification Logic, a framework for reasoning about evidence and justification. This novel combination incorporates a new kind of multi-agent evidence elimination that cleanly meshes with the multi-agent communications from Dynamic Epistemic Logic, resulting in a system for reasoning about multi-agent communication and evidence elimination for groups of interacting rational agents.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  3.  11
    Enrico Marchioni (2012). Amalgamation Through Quantifier Elimination for Varieties of Commutative Residuated Lattices. Archive for Mathematical Logic 51 (1-2):15-34.
    This work presents a model-theoretic approach to the study of the amalgamation property for varieties of semilinear commutative residuated lattices. It is well-known that if a first-order theory T enjoys quantifier elimination in some language L, the class of models of the set of its universal consequences ${\rm T_\forall}$ has the amalgamation property. Let ${{\rm Th}(\mathbb{K})}$ be the theory of an elementary subclass ${\mathbb{K}}$ of the linearly ordered members of a variety ${\mathbb{V}}$ of semilinear commutative residuated lattices. We show (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  4.  2
    Philipp Gerhardy (2005). The Role of Quantifier Alternations in Cut Elimination. Notre Dame Journal of Formal Logic 46 (2):165-171.
    Extending previous results from work on the complexity of cut elimination for the sequent calculus LK, we discuss the role of quantifier alternations and develop a measure to describe the complexity of cut elimination in terms of quantifier alternations in cut formulas and contractions on such formulas.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  5.  17
    Pierluigi Minari (2007). Analytic Proof Systems for Λ-Calculus: The Elimination of Transitivity, and Why It Matters. [REVIEW] Archive for Mathematical Logic 46 (5-6):385-424.
    We introduce new proof systems G[β] and G ext[β], which are equivalent to the standard equational calculi of λβ- and λβη- conversion, and which may be qualified as ‘analytic’ because it is possible to establish, by purely proof-theoretical methods, that in both of them the transitivity rule admits effective elimination. This key feature, besides its intrinsic conceptual significance, turns out to provide a common logical background to new and comparatively simple demonstrations—rooted in nice proof-theoretical properties of transitivity-free derivations—of a (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  6.  12
    Yalin Firat Çelikler (2007). Quantifier Elimination for the Theory of Algebraically Closed Valued Fields with Analytic Structure. Mathematical Logic Quarterly 53 (3):237-246.
    The theory of algebraically closed non-Archimedean valued fields is proved to eliminate quantifiers in an analytic language similar to the one used by Cluckers, Lipshitz, and Robinson. The proof makes use of a uniform parameterized normalization theorem which is also proved in this paper. This theorem also has other consequences in the geometry of definable sets. The method of proving quantifier elimination in this paper for an analytic language does not require the algebraic quantifier elimination theorem of Weispfenning, (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  7.  56
    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)  
     
    Export citation  
     
    My bibliography   1 citation  
  8.  8
    Tommaso Cortonesi, Enrico Marchioni & Franco Montagna (2010). Quantifier Elimination and Other Model-Theoretic Properties of BL-Algebras. Notre Dame Journal of Formal Logic 52 (4):339-379.
    This work presents a model-theoretic approach to the study of first-order theories of classes of BL-chains. Among other facts, we present several classes of BL-algebras, generating the whole variety of BL-algebras, whose first-order theory has quantifier elimination. Model-completeness and decision problems are also investigated. Then we investigate classes of BL-algebras having (or not having) the amalgamation property or the joint embedding property and we relate the above properties to the existence of ultrahomogeneous models.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  9.  9
    H. Jerome Keisler (1998). Quantifier Elimination for Neocompact Sets. Journal of Symbolic Logic 63 (4):1442-1472.
    We shall prove quantifier elimination theorems for neocompact formulas, which define neocompact sets and are built from atomic formulas using finite disjunctions, infinite conjunctions, existential quantifiers, and bounded universal quantifiers. The neocompact sets were first introduced to provide an easy alternative to nonstandard methods of proving existence theorems in probability theory, where they behave like compact sets. The quantifier elimination theorems in this paper can be applied in a general setting to show that the family of neocompact sets (...)
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  10.  11
    Enrique Casanovas & Rafel Farré (2004). Weak Forms of Elimination of Imaginaries. Mathematical Logic Quarterly 50 (2):126-140.
    We study the degree of elimination of imaginaries needed for the three main applications: to have canonical bases for types over models, to define strong types as types over algebraically closed sets and to have a Galois correspondence between definably closed sets B such that A ⊆ B ⊆ acl and closed subgroups of the Galois group Aut/A). We also characterize when the topology of the Galois group is the quotient topology.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  11.  8
    Jude Brighton (2016). Cut Elimination for GLS Using the Terminability of its Regress Process. Journal of Philosophical Logic 45 (2):147-153.
    The system GLS, which is a modal sequent calculus system for the provability logic GL, was introduced by G. Sambin and S. Valentini in Journal of Philosophical Logic, 11, 311–342,, and in 12, 471–476,, the second author presented a syntactic cut-elimination proof for GLS. In this paper, we will use regress trees in order to present a simpler and more intuitive syntactic cut derivability proof for GLS1, which is a variant of GLS without the cut rule.
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  12.  5
    Pierluigi Minari (2004). Analytic Combinatory Calculi and the Elimination of Transitivity. Archive for Mathematical Logic 43 (2):159-191.
    We introduce, in a general setting, an ‘‘analytic’’ version of standard equational calculi of combinatory logic. Analyticity lies on the one side in the fact that these calculi are characterized by the presence of combinatory introduction rules in place of combinatory axioms, and on the other side in that the transitivity rule proves to be eliminable. Apart from consistency, which follows immediately, we discuss other almost direct consequences of analyticity and the main transitivity elimination theorem; in particular the Church−Rosser (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  13.  10
    Steffen van Bakel (2004). Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing. Notre Dame Journal of Formal Logic 45 (1):35-63.
    This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  14.  24
    Gilles Dowek & Olivier Hermant (2012). A Simple Proof That Super-Consistency Implies Cut Elimination. Notre Dame Journal of Formal Logic 53 (4):439-456.
    We give a simple and direct proof that super-consistency implies the cut-elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut-elimination theorems in higher-order logic that involve V-complexes.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  15.  39
    Kai Brünnler (2006). Cut Elimination Inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82 (1):51 - 71.
    Deep inference is a natural generalisation of the one-sided sequent calculus where rules are allowed to apply deeply inside formulas, much like rewrite rules in term rewriting. This freedom in applying inference rules allows to express logical systems that are difficult or impossible to express in the cut-free sequent calculus and it also allows for a more fine-grained analysis of derivations than the sequent calculus. However, the same freedom also makes it harder to carry out this analysis, in particular it (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography  
  16.  11
    Rafael Grimson, Bart Kuijpers & Walied Othman (2012). Quantifier Elimination for Elementary Geometry and Elementary Affine Geometry. Mathematical Logic Quarterly 58 (6):399-416.
    We introduce new first-order languages for the elementary n-dimensional geometry and elementary n-dimensional affine geometry , based on extending equation image and equation image, respectively, with new function symbols. Here, β stands for the betweenness relation and ≡ for the congruence relation. We show that the associated theories admit effective quantifier elimination.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography  
  17.  10
    M. Prunescu (2001). Non-Effective Quantifier Elimination. Mathematical Logic Quarterly 47 (4):557-562.
    Genera connections between quantifier elimination and decidability for first order theories are studied and exemplified.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  18.  4
    Andrey A. Kuzichev (1992). Elimination of Quantifiers Over Vectors in Some Theories of Vector Spaces. Mathematical Logic Quarterly 38 (1):575-577.
    We consider two-sorted theories of vector spaces and prove a criterion for the assertion that such a theory allows elimination of quantifiers over vector variables.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   1 citation  
  19.  10
    Michael Gabbay (2011). A Proof-Theoretic Treatment of Λ-Reduction with Cut-Elimination: Λ-Calculus as a Logic Programming Language. Journal of Symbolic Logic 76 (2):673 - 699.
    We build on an existing a term-sequent logic for the λ-calculus. We formulate a general sequent system that fully integrates αβη-reductions between untyped λ-terms into first order logic. We prove a cut-elimination result and then offer an application of cut-elimination by giving a notion of uniform proof for λ-terms. We suggest how this allows us to view the calculus of untyped αβ-reductions as a logic programming language (as well as a functional programming language, as it is traditionally seen).
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  20.  20
    Pierre Poirier (2006). Finding a Place for Elimination in Inter-Level Reductionist Activities: Reply to Wimsatt. Synthese 151 (3):477 - 483.
    According to Wimsatt, a proper treatment of reduction must distinguish between two types of reductionist activities scientists engage in. One of the benefits of better understanding the nature of reduction, he believes, is that it shows that eliminativism, that is, the elimination of concepts and theories from science, is a rather circumscribed and limited affair, especially in the case of inter-level reductionist activities. While I agree with Wimsatt that it is important to distinguish the two types of reductionisms, I (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  21.  3
    Yunfu Shen (1999). Elimination of Algorithmic Quantifiers for Ordered Differential Algebra. Archive for Mathematical Logic 38 (3):139-144.
    In [2], Singer proved that the theory of ordered differential fields has a model completion, i.e, the theory of closed ordered differential fields, CODF. As a result, CODF admits elimination of quantifiers. In this paper we give an algorithm to eliminate the quantifiers of CODF-formulas.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  22.  6
    M. Baaz & A. Leitsch (2014). Cut-Elimination: Syntax and Semantics. Studia Logica 102 (6):1217-1244.
    In this paper we first give a survey of reductive cut-elimination methods in classical logic. In particular we describe the methods of Gentzen and Schütte-Tait from the abstract point of view of proof reduction. We also present the method CERES which we classify as a semi-semantic method. In a further section we describe the so-called semantic methods. In the second part of the paper we carry the proof analysis further by generalizing the CERES method to CERESD . In the (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography  
  23.  16
    William Craig (2008). Elimination Problems in Logic: A Brief History. Synthese 164 (3):321 - 332.
    A common aim of elimination problems for languages of logic is to express the entire content of a set of formulas of the language, or a certain part of it, in a way that is more elementary or more informative. We want to bring out that as the languages for logic grew in expressive power and, at the same time, our knowledge of their expressive limitations also grew, elimination problems in logic underwent some change. For languages other than (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  24.  10
    Grigori Mints (2012). Effective Cut-Elimination for a Fragment of Modal Mu-Calculus. Studia Logica 100 (1-2):279-287.
    A non-effective cut-elimination proof for modal mu-calculus has been given by G. Jäger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M 1 with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M 1 without restriction to positive sequents.
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography  
  25.  3
    Stefano Baratella & Siu‐Ah Ng (2003). Consequences of Neocompact Quantifier Elimination. Mathematical Logic Quarterly 49 (2):150-162.
    We provide some consequences of a Quantifier Elimination Property and related properties previously introduced in the setting of Banach space structures. We further consider some applications of quantifierfree definability, such as strict convexity via the definability of certain mapping and the continuity of definable functions.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  26.  3
    Ben Ellison, Jonathan Fleischmann, Dan McGinn & Wim Ruitenburg (2008). Quantifier Elimination for a Class of Intuitionistic Theories. Notre Dame Journal of Formal Logic 49 (3):281-293.
    From classical, Fraïissé-homogeneous, ($\leq \omega$)-categorical theories over finite relational languages, we construct intuitionistic theories that are complete, prove negations of classical tautologies, and admit quantifier elimination. We also determine the intuitionistic universal fragments of these theories.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  27.  3
    Rajeev Goré & Revantha Ramanayake (2014). Cut-Elimination for Weak Grzegorczyk Logic Go. Studia Logica 102 (1):1-27.
    We present a syntactic proof of cut-elimination for weak Grzegorczyk logic Go. The logic has a syntactically similar axiomatisation to Gödel–Löb logic GL (provability logic) and Grzegorczyk’s logic Grz. Semantically, GL can be viewed as the irreflexive counterpart of Go, and Grz can be viewed as the reflexive counterpart of Go. Although proofs of syntactic cut-elimination for GL and Grz have appeared in the literature, this is the first proof of syntactic cut-elimination for Go. The proof is (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  28.  1
    Ryo Kashima & Tatsuya Shimura (1994). Cut‐Elimination Theorem for the Logic of Constant Domains. Mathematical Logic Quarterly 40 (2):153-172.
    The logic CD is an intermediate logic which exactly corresponds to the Kripke models with constant domains. It is known that the logic CD has a Gentzen-type formulation called LD and rules are replaced by the corresponding intuitionistic rules) and that the cut-elimination theorem does not hold for LD. In this paper we present a modification of LD and prove the cut-elimination theorem for it. Moreover we prove a “weak” version of cut-elimination theorem for LD, saying that (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  29.  1
    Y. Tanaka (2001). Cut-Elimination Theorems of Some Infinitary Modal Logics. Mathematical Logic Quarterly 47 (3):327-340.
    In this article, a cut-free system TLMω1 for infinitary propositional modal logic is proposed which is complete with respect to the class of all Kripke frames.The system TLMω1 is a kind of Gentzen style sequent calculus, but a sequent of TLMω1 is defined as a finite tree of sequents in a standard sense. We prove the cut-elimination theorem for TLMω1 via its Kripke completeness.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  30. Peter Carruthers (1998). Conscious Thinking: Language or Elimination? Mind and Language 13 (4):457-476.
    Do we conduct our conscious propositional thinking in natural language? Or is such language only peripherally related to human conscious thought-processes? In this paper I shall present a partial defence of the former view, by arguing that the only real alternative is eliminativism about conscious propositional thinking. Following some introductory remarks, I shall state the argument for this conclusion, and show how that conclusion can be true. Thereafter I shall defend each of the three main premises in turn.
    Direct download (15 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  31.  10
    Kaja Bednarska & Andrzej Indrzejczak (2015). Hypersequent Calculi for S5: The Methods of Cut Elimination. Logic and Logical Philosophy 24 (3):277–311.
  32.  3
    Robert A. Bull (1992). Cut Elimination for Propositional Dynamic Logic Without. Mathematical Logic Quarterly 38 (1):85-100.
  33.  27
    J. Schwartz (1991). Reduction, Elimination, and the Mental. Philosophy of Science 58 (June):203-20.
    The antireductionist arguments of many philosophers (e.g., Baker, Fodor and Davidson) are motivated by a worry that successful reduction would eliminate rather than conserve the mental. This worry derives from a misunderstanding of the empiricist account of reduction, which, although it does not underwrite "cognitive suicide", should be rejected for its positivist baggage. Philosophy of psychology needs more detailed attention to issues in natural science which serve as analogies for reduction of the mental. I consider a range of central cases, (...)
    Direct download (9 more)  
     
    Export citation  
     
    My bibliography  
  34.  4
    J. A. McGeoch & H. N. Peters (1933). An All-or-None Characteristic in the Elimination of Errors During the Learning of a Stylus Maze. Journal of Experimental Psychology 16 (4):504.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  35.  4
    Marylin C. Smith & Susan Ramunas (1971). Elimination of Visual Field Effects by Use of a Single Report Technique: Evidence for Order-of-Report Artifact. Journal of Experimental Psychology 87 (1):23.
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  36.  2
    H. N. Peters & J. A. McGeoch (1935). The Relationship Between Time Spent in the Culs-de-Sac of a Stylus Maze and Speed of Elimination. Journal of Experimental Psychology 18 (4):414.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  37.  1
    C. J. Warden (1923). Some Factors Determining the Order of Elimination of Culs-de-Sac in the Maze. Journal of Experimental Psychology 6 (3):192.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  38.  17
    Clemens Grabmayer, Joop Leo, Vincent van Oostrom & Albert Visser (2011). On the Termination of Russell's Description Elimination Algorithm. Review of Symbolic Logic 4 (3):367-393.
    In this paper we study the termination behavior of Russell’s description elimination rewrite system. We discuss certain claims made by Kripke (2005) in his paper concerning the possible nontermination of elimination of descriptions.
    No categories
    Direct download (6 more)  
     
    Export citation  
     
    My bibliography   17 citations  
  39. Anna Zamansky & Arnon Avron (2006). Cut-Elimination and Quantification in Canonical Systems. Studia Logica 82 (1):157 - 176.
    Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to rules with (...)
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography  
  40. Stephen Read (2010). General-Elimination Harmony and the Meaning of the Logical Constants. Journal of Philosophical Logic 39 (5):557-76.
    Inferentialism claims that expressions are meaningful by virtue of rules governing their use. In particular, logical expressions are autonomous if given meaning by their introduction-rules, rules specifying the grounds for assertion of propositions containing them. If the elimination-rules do no more, and no less, than is justified by the introduction-rules, the rules satisfy what Prawitz, following Lorenzen, called an inversion principle. This connection between rules leads to a general form of elimination-rule, and when the rules have this form, (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   8 citations  
  41.  90
    Andrew M. Bailey (2014). The Elimination Argument. Philosophical Studies 168 (2):475-482.
    Animalism is the view that we are animals: living, breathing, wholly material beings. Despite its considerable appeal, animalism has come under fire. Other philosophers have had much to say about objections to animalism that stem from reflection on personal identity over time. But one promising objection (the `Elimination Argument') has been overlooked. In this paper, I remedy this situation and examine the Elimination Argument in some detail. I contend that the Elimination Argument is both unsound and unmotivated.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  42.  7
    Jan von Plato (2001). Natural Deduction with General Elimination Rules. Archive for Mathematical Logic 40 (7):541-567.
    The structure of derivations in natural deduction is analyzed through isomorphism with a suitable sequent calculus, with twelve hidden convertibilities revealed in usual natural deduction. A general formulation of conjunction and implication elimination rules is given, analogous to disjunction elimination. Normalization through permutative conversions now applies in all cases. Derivations in normal form have all major premisses of elimination rules as assumptions. Conversion in any order terminates.Through the condition that in a cut-free derivation of the sequent Γ⇒C, (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   19 citations  
  43.  20
    David Ludwig (2014). Hysteria, Race, and Phlogiston. A Model of Ontological Elimination in the Human Sciences. Studies in History and Philosophy of Science Part C: Studies in History and Philosophy of Biological and Biomedical Sciences 45:68-77.
    Elimination controversies are ubiquitous in philosophy and the human sciences. For example, it has been suggested that human races, hysteria, intelligence, mental disorder, propositional attitudes such as beliefs and desires, the self, and the super-ego should be eliminated from the list of respectable entities in the human sciences. I argue that eliminativist proposals are often presented in the framework of an oversimplified “phlogiston model” and suggest an alternative account that describes ontological elimination on a gradual scale between criticism (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography  
  44.  16
    Francesco Belardinelli, Peter Jipsen & Hiroakira Ono (2004). Algebraic Aspects of Cut Elimination. Studia Logica 77 (2):209 - 240.
    We will give here a purely algebraic proof of the cut elimination theorem for various sequent systems. Our basic idea is to introduce mathematical structures, called Gentzen structures, for a given sequent system without cut, and then to show the completeness of the sequent system without cut with respect to the class of algebras for the sequent system with cut, by using the quasi-completion of these Gentzen structures. It is shown that the quasi-completion is a generalization of the MacNeille (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   12 citations  
  45.  28
    Rajeev Gore & Revantha Ramanayake (2012). Valentini's Cut-Elimination for Provability Logic Resolved. Review of Symbolic Logic 5 (2):212-238.
    In 1983, Valentini presented a syntactic proof of cut elimination for a sequent calculus GLSV for the provability logic GL where we have added the subscript V for “Valentini”. The sequents in GLSV were built from sets, as opposed to multisets, thus avoiding an explicit contraction rule. From a syntactic point of view, it is more satisfying and formal to explicitly identify the applications of the contraction rule that are ‘hidden’ in these set based proofs of cut elimination. (...)
    Direct download (8 more)  
     
    Export citation  
     
    My bibliography   3 citations  
  46.  3
    Kai Brünnler & Thomas Studer (2009). Syntactic Cut-Elimination for Common Knowledge. Annals of Pure and Applied Logic 160 (1):82-95.
    We first look at an existing infinitary sequent system for common knowledge for which there is no known syntactic cut-elimination procedure and also no known non-trivial bound on the proof-depth. We then present another infinitary sequent system based on nested sequents that are essentially trees and with inference rules that apply deeply inside these trees. Thus we call this system “deep” while we call the former system “shallow”. In contrast to the shallow system, the deep system allows one to (...)
    Direct download (2 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  47.  4
    Nikolaos Galatos & Hiroakira Ono (2010). Cut Elimination and Strong Separation for Substructural Logics: An Algebraic Approach. Annals of Pure and Applied Logic 161 (9):1097-1133.
    We develop a general algebraic and proof-theoretic study of substructural logics that may lack associativity, along with other structural rules. Our study extends existing work on substructural logics over the full Lambek Calculus [34], Galatos and Ono [18], Galatos et al. [17]). We present a Gentzen-style sequent system that lacks the structural rules of contraction, weakening, exchange and associativity, and can be considered a non-associative formulation of . Moreover, we introduce an equivalent Hilbert-style system and show that the logic associated (...)
    Direct download (3 more)  
     
    Export citation  
     
    My bibliography   4 citations  
  48.  13
    Angela J. Schneider & Robert R. Butcher (1993). Why Olympic Athletes Should Avoid the Use and Seek the Elimination of Performance-Enhancing Substances and Practices From the Olympic Games. Journal of the Philosophy of Sport 20 (1):64-81.
    (1993). Why Olympic Athletes Should Avoid the Use and Seek the Elimination of Performance-Enhancing Substances and Practices From the Olympic Games. Journal of the Philosophy of Sport: Vol. 20, No. 1, pp. 64-81. doi: 10.1080/00948705.1993.9714504.
    Direct download (4 more)  
     
    Export citation  
     
    My bibliography   14 citations  
  49.  12
    Kazushige Terui (2007). Which Structural Rules Admit Cut Elimination? An Algebraic Criterion. Journal of Symbolic Logic 72 (3):738 - 754.
    Consider a general class of structural inference rules such as exchange, weakening, contraction and their generalizations. Among them, some are harmless but others do harm to cut elimination. Hence it is natural to ask under which condition cut elimination is preserved when a set of structural rules is added to a structure-free logic. The aim of this work is to give such a condition by using algebraic semantics. We consider full Lambek calculus (FL), i.e., intuitionistic logic without any (...)
    Direct download (5 more)  
     
    Export citation  
     
    My bibliography   5 citations  
  50.  62
    Chantal Berline (1981). Rings Which Admit Elimination of Quantifiers. Journal of Symbolic Logic 46 (1):56-58.
    The aim of this paper is to provide an addendum to a paper by Rose with the same title which has appeared in an earlier issue of this Journal [2]. Our new result is: Theorem. A ring of characteristic zero which admits elimination of quantifiers in the language {0, 1, +, ·} is an algebraically closed field.
    Direct download (7 more)  
     
    Export citation  
     
    My bibliography   1 citation  
1 — 50 / 1000