Eliminating disjunctions by disjunction elimination
From MaRDI portal
Publication:1688959
DOI10.1016/j.indag.2017.09.011zbMath1437.03163OpenAlexW2766243828MaRDI QIDQ1688959
Davide Rinaldi, Daniel Wessel, Peter M. Schuster
Publication date: 12 January 2018
Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.indag.2017.09.011
Other constructive mathematics (03F65) Proof theory in general (including proof-theoretic semantics) (03F03) Axiom of choice and related propositions (03E25)
Related Items (16)
The Jacobson radical for an inconsistency predicate ⋮ An unexpected Boolean connective ⋮ THE JACOBSON RADICAL OF A PROPOSITIONAL THEORY ⋮ A universal algorithm for Krull's theorem ⋮ Radical theory of Scott-open filters ⋮ Unnamed Item ⋮ Dynamic evaluation of integrity and the computational content of Krull's lemma ⋮ Constructive Proofs of Negated Statements ⋮ Point-Free Spectra of Linear Spreads ⋮ Unnamed Item ⋮ Cut elimination for entailment relations ⋮ The Hahn-Banach theorem by disjunction elimination ⋮ Ordering groups constructively ⋮ Maximal ideals in countable rings, constructively ⋮ The computational significance of Hausdorff's maximal chain principle ⋮ Syntax for Semantics: Krull’s Maximal Ideal Theorem
Cites Work
- A universal Krull-Lindenbaum theorem
- The proof by cases property and its variants in structural consequence relations
- A simple proof of Parsons' theorem
- Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
- Proofs, programs, processes
- Proof-theoretical analysis of order relations
- Simple consequence relations
- Logics with disjunction and proof by cases
- Finitary formal topologies and Stone's representation theorem
- Space of valuations
- Proving open properties by induction
- Two applications of Boolean models
- Semantical investigations in Heyting's intuitionistic logic
- A globalization of the Hahn-Banach theorem
- Theory of logical calculi. Basic theory of consequence operations
- A course in constructive algebra
- Constructive rereading of Artin-Schreier theory
- Some points in formal topology.
- Untersuchungen über das logische Schliessen. I
- Untersuchungen über das logische Schliessen. II
- Valuations and Dedekind's Prague theorem
- Representations of preference orderings
- Non-deterministic inductive definitions
- Minimal from classical proofs
- Remarks on the Scott-Lindenbaum theorem
- Commutative algebra: constructive methods. Finite projective modules. Translated from the French by Tania K. Roblot
- Constructive commutative algebra. Projective modules over polynomial rings and dynamical Gröbner bases
- Quasi-transitive and Suzumura consistent relations
- Choice structures and preference relations
- Dynamical algebraic structures, pointfree topological spaces and Hilbert's program. (Structures algébriques dynamiques, espaces topologiques sans points et programme de Hilbert)
- Teilbarkeitstheorie in Bereichen
- Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen
- Induction in Algebra: a First Case Study
- SZPILRAJN, ARROW AND SUZUMURA: CONCISE PROOFS OF EXTENSION THEOREMS AND AN EXTENSION
- L.E.J. Brouwer's ‘Unreliability of the Logical Principles’: A New Translation, with an Introduction
- Induction in Algebra: A First Case Study
- On a conservative extension argument of Dana Scott
- Proofs and Computations
- Proof Analysis
- Semiorders and a Theory of Utility Discrimination
- Foundational aspects of theories of measurement
- Lindenbaum’s Lemma via Open Induction
- Geometric Hahn-Banach theorem
- A logical approach to abstract algebra
- Constructive set theory
- Continuous domains as formal spaces
- Hidden constructions in abstract algebra. Krull Dimension of distributive lattices and commutative rings
- Convergence in formal topology: a unifying notion
- Non-Deterministic Inductive Definitions and Fullness
- ELIMINATING DISJUNCTIONS BY DISJUNCTION ELIMINATION
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Every countably presented formal topology is spatial, classically
- Generalized geometric theories and set-generated classes
- Algebraische und logistische Untersuchungen über freie Verbände
- Algorithms in real algebraic geometry
- Über halbgeordnete Gruppen
- Protoalgebraic logics
- Dynamical method in algebra: Effective Nullstellensätze
- Hidden constructions in abstract algebra. I: Integral dependance.
- Refined program extraction from classical proofs
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Eliminating disjunctions by disjunction elimination