Eliminating disjunctions by disjunction elimination

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

Mathematics Subject Classification ID

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