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

1000+ found
Sort by:
  1. Roy Dyckhoff & Luis Pinto (1998). Cut-Elimination and a Permutation-Free Sequent Calculus for Intuitionistic Logic. Studia Logica 60 (1):107-118.score: 24.0
    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  
  2. William Craig (2008). Elimination Problems in Logic: A Brief History. Synthese 164 (3):321 - 332.score: 24.0
    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 (5 more)  
     
    My bibliography  
     
    Export citation  
  3. Kai Brünnler (2006). Cut Elimination Inside a Deep Inference System for Classical Predicate Logic. Studia Logica 82 (1):51 - 71.score: 24.0
    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 (6 more)  
     
    My bibliography  
     
    Export citation  
  4. Pierre Poirier (2006). Finding a Place for Elimination in Inter-Level Reductionist Activities: Reply to Wimsatt. Synthese 151 (3):477 - 483.score: 24.0
    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 (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  5. Grigori Mints (2012). Effective Cut-Elimination for a Fragment of Modal Mu-Calculus. Studia Logica 100 (1-2):279-287.score: 24.0
    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)  
     
    My bibliography  
     
    Export citation  
  6. 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.score: 24.0
    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)  
     
    My bibliography  
     
    Export citation  
  7. M. Baaz & A. Leitsch (2014). Cut-Elimination: Syntax and Semantics. Studia Logica 102 (6):1217-1244.score: 24.0
    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)  
     
    My bibliography  
     
    Export citation  
  8. Gilles Dowek & Olivier Hermant (2012). A Simple Proof That Super-Consistency Implies Cut Elimination. Notre Dame Journal of Formal Logic 53 (4):439-456.score: 24.0
    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 (5 more)  
     
    My bibliography  
     
    Export citation  
  9. H. Jerome Keisler (1998). Quantifier Elimination for Neocompact Sets. Journal of Symbolic Logic 63 (4):1442-1472.score: 24.0
    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 (6 more)  
     
    My bibliography  
     
    Export citation  
  10. Pierluigi Minari (2004). Analytic Combinatory Calculi and the Elimination of Transitivity. Archive for Mathematical Logic 43 (2):159-191.score: 24.0
    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 (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  11. 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.score: 24.0
    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 (3 more)  
     
    My bibliography  
     
    Export citation  
  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.score: 24.0
    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, (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  13. 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.score: 24.0
    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)  
     
    My bibliography  
     
    Export citation  
  14. Rajeev Goré & Revantha Ramanayake (2014). Cut-Elimination for Weak Grzegorczyk Logic Go. Studia Logica 102 (1):1-27.score: 24.0
    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)  
     
    My bibliography  
     
    Export citation  
  15. Enrico Marchioni (2012). Amalgamation Through Quantifier Elimination for Varieties of Commutative Residuated Lattices. Archive for Mathematical Logic 51 (1-2):15-34.score: 24.0
    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 (...)
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  16. Philipp Gerhardy (2005). The Role of Quantifier Alternations in Cut Elimination. Notre Dame Journal of Formal Logic 46 (2):165-171.score: 24.0
    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 (5 more)  
     
    My bibliography  
     
    Export citation  
  17. 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.score: 24.0
    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)  
     
    My bibliography  
     
    Export citation  
  18. 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.score: 24.0
    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 (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  19. Bryan Renne (2012). Multi-Agent Justification Logic: Communication and Evidence Elimination. [REVIEW] Synthese 185 (S1):43-82.score: 24.0
    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)  
     
    My bibliography  
     
    Export citation  
  20. Yunfu Shen (1999). Elimination of Algorithmic Quantifiers for Ordered Differential Algebra. Archive for Mathematical Logic 38 (3):139-144.score: 24.0
    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.
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  21. J. Schwartz (1991). Reduction, Elimination, and the Mental. Philosophy of Science 58 (June):203-20.score: 22.0
    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 (8 more)  
     
    My bibliography  
     
    Export citation  
  22. Peter Carruthers (1998). Conscious Thinking: Language or Elimination? Mind and Language 13 (4):457-476.score: 21.0
    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)  
     
    My bibliography  
     
    Export citation  
  23. Rafael Grimson, Bart Kuijpers & Walied Othman (2012). Quantifier Elimination for Elementary Geometry and Elementary Affine Geometry. Mathematical Logic Quarterly 58 (6):399-416.score: 21.0
    No categories
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  24. M. Prunescu (2001). Non-Effective Quantifier Elimination. Mathematical Logic Quarterly 47 (4):557-562.score: 21.0
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  25. Stefano Baratella & Siu‐Ah Ng (2003). Consequences of Neocompact Quantifier Elimination. Mathematical Logic Quarterly 49 (2):150-162.score: 21.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  26. Robert A. Bull (1992). Cut Elimination for Propositional Dynamic Logic Without. Mathematical Logic Quarterly 38 (1):85-100.score: 21.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  27. Enrique Casanovas & Rafel Farré (2004). Weak Forms of Elimination of Imaginaries. Mathematical Logic Quarterly 50 (2):126-140.score: 21.0
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  28. Andrey A. Kuzichev (1992). Elimination of Quantifiers Over Vectors in Some Theories of Vector Spaces. Mathematical Logic Quarterly 38 (1):575-577.score: 21.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  29. 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.score: 21.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  30. 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.score: 21.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  31. 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.score: 21.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  32. 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.score: 21.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  33. Ryo Kashima & Tatsuya Shimura (1994). Cut‐Elimination Theorem for the Logic of Constant Domains. Mathematical Logic Quarterly 40 (2):153-172.score: 21.0
    No categories
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  34. Y. Tanaka (2001). Cut-Elimination Theorems of Some Infinitary Modal Logics. Mathematical Logic Quarterly 47 (3):327-340.score: 21.0
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  35. Stephen Read (2010). General-Elimination Harmony and the Meaning of the Logical Constants. Journal of Philosophical Logic 39 (5):557-76.score: 18.0
    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 (6 more)  
     
    My bibliography  
     
    Export citation  
  36. Radu J. Bogdan (1988). Mental Attitudes and Common Sense Psychology: The Case Against Elimination. Noûs 22 (September):369-398.score: 18.0
    Aside from brute force, there are several philosophically respectable ways of eliminating the mental. In recent years the most popular elimination strategy has been directed against our common sense or folk psychological understanding of the mental. The strategy goes by the name of eliminative materialism (or eliminativism, in short). The motivation behind this strategy seems to be the following. If common sense psychology can be construed as the principled theory of the mental, whose vocabulary and principles implicitly define what (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  37. Andrew M. Bailey (2014). The Elimination Argument. Philosophical Studies 168 (2):475-482.score: 18.0
    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)  
     
    My bibliography  
     
    Export citation  
  38. James Blachowicz (1995). Elimination, Correction and Popper's Evolutionary Epistemology. International Studies in the Philosophy of Science 9 (1):5 – 17.score: 18.0
    Abstract Evolutionary epistemologists from Popper to Campbell have appropriated the Darwinian principle to explain the apparent fit between the world and our knowledge of it. I argue that this strategy suffers from the lack of any principled distinction among various types of elimination. I offer such a distinction and show that there is a species of elimination that is really corrective, that is, which violates the Darwinian principle as Popper understands it.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  39. Greg Frost-Arnold (2005). The Large-Scale Structure of Logical Empiricism: Unity of Science and the Elimination of Metaphysics. Philosophy of Science 72 (5):826-838.score: 18.0
    Two central and well-known philosophical goals of the logical empiricists are the unification of science and the elimination of metaphysics. I argue, via textual analysis, that these two apparently distinct planks of the logical empiricist party platform are actually intimately related. From the 1920’s through 1950, one abiding criterion for judging whether an apparently declarative assertion or descriptive term is metaphysical is that that assertion or term cannot be incorporated into a language of unified science. I explore various versions (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  40. Anne Maclean (1993). The Elimination of Morality: Reflections on Utilitarianism and Bioethics. Routledge.score: 18.0
    The Elimination of Morality poses a fundamental challenge to the dominant conception of medical ethics. In this controversial and timely study, Anne Maclean addresses the question of what kind of contribution philosophers can make to the discussion of medico-moral issues and the work of health care professionals. She establishes the futility of bioethics by challenging the conception of reason in ethics which is integral to the utilitarian tradition. She argues that a philosophical training confers no special authority to make (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  41. Greg Restall, Defining Double Negation Elimination.score: 18.0
    In his paper “Generalised Ortho Negation” [2] J. Michael Dunn mentions a claim of mine to the effect that there is no condition on ‘perp frames’ equivalent to the holding of double negation elimination ∼∼A A. That claim is wrong. In this paper I correct my error and analyse the behaviour of conditions on frames for negations which verify a number of different theses.1..
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  42. Grigori Mints (2006). Cut Elimination for S4c: A Case Study. Studia Logica 82 (1):121 - 132.score: 18.0
    S4C is a logic of continuous transformations of a topological space. Cut elimination for it requires new kind of rules and new kinds of reductions.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  43. Dov M. Gabbay & Andrzej Szałas (2007). Second-Order Quantifier Elimination in Higher-Order Contexts with Applications to the Semantical Analysis of Conditionals. Studia Logica 87 (1):37 - 50.score: 18.0
    Second-order quantifier elimination in the context of classical logic emerged as a powerful technique in many applications, including the correspondence theory, relational databases, deductive and knowledge databases, knowledge representation, commonsense reasoning and approximate reasoning. In the current paper we first generalize the result of Nonnengart and Szałas [17] by allowing second-order variables to appear within higher-order contexts. Then we focus on a semantical analysis of conditionals, using the introduced technique and Gabbay’s semantics provided in [10] and substantially using a (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  44. G. Mints (1999). Cut-Elimination for Simple Type Theory with an Axiom of Choice. Journal of Symbolic Logic 64 (2):479-485.score: 18.0
    We present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  45. Colin Cheyne (1993). Reduction, Elimination, and Firewalking. Philosophy of Science 60 (2):349-357.score: 18.0
    Schwartz (1991) argues that the worry that successful reduction would eliminate rather than conserve the mental is a needless worry. He examines cases of reduction from the natural sciences and claims that if reduction of the mental is like any of those cases then it would not be a case of elimination. I discuss other cases of scientific reduction which do involve elimination. Schwartz has not shown that reduction of the mental could not be like such cases, so (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  46. Rajeev Gore, Linda Postniece & Alwen Tiu, Cut-Elimination and Proof-Search for Bi-Intuitionistic Logic Using Nested Sequents.score: 18.0
    We propose a new sequent calculus for bi intuitionistic logic which sits somewhere between display calculi and traditional sequent calculi by using nested sequents. Our calculus enjoys a simple (purely syntactic) cut elimination proof as do display calculi. But it has an easily derivable variant calculus which is amenable to automated proof search as are (some) traditional sequent calculi. We first present the initial calculus and its cut elimination proof. We then present the derived calculus, and then present (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  47. Yiwei Zheng (2001). Ockham's Connotation Theory and Ontological Elimination. Journal of Philosophical Research 26:623-634.score: 18.0
    The importance of the connotation theory in Ockham’s semantics and metaphysics can hardly be overstated---it is the main mechanism that brings forth Ockham’s famous ontological elimination. Yet none of the extant interpretations can satisfactorily accommodate three widely accepted theses: (1) there is no synonym in mental language; (2) a connotative term has a semantically equivalent nominal definition; and (3) there are simple connotative terms in Ockham’s mental language. In this paper I offer an interpretation that I argue can accommodate (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  48. Jeremy Avigad, Algebraic Proofs of Cut Elimination.score: 18.0
    Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  49. Rajeev Gore & Revantha Ramanayake (2012). Valentini's Cut-Elimination for Provability Logic Resolved. Review of Symbolic Logic 5 (2):212-238.score: 18.0
    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. (...)
    No categories
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  50. Luc Bélair & Françoise Point (2010). Quantifier Elimination in Valued Ore Modules. Journal of Symbolic Logic 75 (3):1007-1034.score: 18.0
    We consider valued fields with a distinguished isometry or contractive derivation as valued modules over the Ore ring of difference operators. Under certain assumptions on the residue field, we prove quantifier elimination first in the pure module language, then in that language augmented with a chain of additive subgroups, and finally in a two-sorted language with a valuation map. We apply quantifier elimination to prove that these structures do not have the independence property.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
1 — 50 / 1000