Principle of Explosion¶
A logic-relative consequence rule under which a proposition and its negation together entail any formula whatsoever.
Core Idea¶
The principle of explosion says that, under a specified logical consequence relation, contradictory premises permit any conclusion. In schematic notation, for arbitrary formulas A and B, {A, ¬A} entails B. Classical and intuitionistic consequence validate this rule; a paraconsistent consequence relation is designed so the unrestricted inference fails. Whether explosion holds therefore depends on the host logic, not on the bare presence of the words “contradiction” or “falsehood.”[1][2]
If a theory proves A and ¬A and is closed under an explosive consequence relation, every formula belongs to its deductive closure. This is formal trivialization: the theory cannot discriminate any proposed conclusion by derivability alone. It does not imply that a human who holds conflicting beliefs consciously endorses every claim or that software will physically print every query result. Those are separate claims about reasoning practices and implementations.[1][3]
Structural Signature¶
Sig role-phrases: specified consequence relation → same-scope A and ¬A → arbitrary formula B → unrestricted entailment → possible trivialized closure.
- Host logic and consequence relation: define what counts as derivable or entailed. Without them, neither validity nor failure of explosion is well-typed.[1][2]
- Contradictory premises: A and its negation ¬A are available together in the same premise set or theory. One false proposition or two claims in different contexts do not supply this antecedent.[1]
- Arbitrary target: B ranges over every formula of the language, including one wholly unrelated to A. Deriving only a special related B is weaker than explosion.[1][3]
- Unrestricted consequence step: the host relation validates {A, ¬A} ⊢ B for each choice of A and B. One counterexample B in a paraconsistent semantics defeats that universal schema.[3]
- Closure effect: if a theory actually derives such a pair and applies this consequence rule, its set of derivable formulas becomes universal. The rule itself can be studied even when a particular theory contains no contradiction.[1]
Disjunction introduction and disjunctive syllogism supply a familiar proof route in suitable calculi; they are not constituent roles required in that precise form by every explosive logic.[3][2]
What It Is Not¶
Explosion is not the same as contradiction. A contradictory pair supplies the antecedent; explosion says what follows from it under a particular consequence relation. Nor is it the same as trivialism, the thesis that every proposition is true. A classical theory with contradictory axioms has every formula derivable, but the metalogical description of its derivability is not a commitment that every proposition is true in reality.[1][3]
It is not a property of every logic containing negation. A paraconsistent logic can recognize a pair A, ¬A while withholding an unrelated B. It is also not merely a permission to infer a false statement from a false premise; the consequent is unrestricted, not selected by topical or causal relevance. Finally, formal entailment is not a psychological instruction to believe everything entailed by one's possibly inconsistent beliefs.[1][3]
Scope of Application¶
In classical propositional reasoning, one can derive A∨B from A and then infer B from A∨B and ¬A by disjunctive syllogism. That route makes the rule explicit, but proof systems can encode explosion differently. Valencia Vizcaíno studies ex falso as a principle separable from excluded middle and double-negation elimination over a minimal-logic base; one should not smuggle those other principles into the identity.[3][2]
In classical description-logic knowledge bases, an inconsistent assertion set may have no classical model. Since classical model-theoretic entailment asks whether every model of the premises satisfies a query, the empty model set gives no countermodel to any query. Zhang and colleagues contrast this collapse with a quasi-classical paraconsistent entailment under which p and ¬p can coexist without entailing an unrelated q.[3]
These are distinct implementations of a formal consequence issue. A database error flag, belief-revision procedure, or a selective query engine is not automatically an explosive theory; its actual inference relation must be specified.
Clarity¶
The schema exposes the decisive quantifier: any B. In a classical derivation from P and ¬P, choosing Q = “the server is healthy” works even when Q shares no terms with P. If one only derives P, ¬P or an immediate restatement, one has not demonstrated explosion. Testing an unrelated target prevents the rule from being mistaken for ordinary inference within an inconsistent topic.[1][3]
It also separates a logic from a theory inside the logic. Classical consequence validates the explosion schema even when a well-formed theory is consistent and never activates it. A contradictory theory under a paraconsistent relation may contain the pair yet avoid trivial closure. Both the host relation and the premise set are needed to predict what happens.[1][3]
Manages Complexity¶
Rather than inspect every proposed conclusion of an inconsistent theory, the schema tells us that one contradictory pair suffices for unrestricted deductive closure—if the logic is explosive. Conversely, one paraconsistent countermodel with p and ¬p true or designated while q is not entailed shows that the universal rule fails in that semantics. This lets a curator distinguish an inference-policy problem from the original inconsistency.[3]
The compression can mislead if the entailment relation is left implicit. Practical reasoners may reject input, flag unsatisfiability, repair axioms, use nonclassical semantics, or answer only a restricted query fragment. The formal result alone does not identify which behavior occurs; it identifies the collapse of unrestricted classical consequence from inconsistent premises.[3]
Abstract Reasoning¶
Let a calculus validate disjunction introduction and disjunctive syllogism with transitive consequence. From P derive P∨Q. From P∨Q and ¬P derive Q. Because Q was chosen arbitrarily, the same route applies to any target formula. The local pair P, ¬P thereby erases a distinction the theory would otherwise use to reject unrelated conclusions. Zhang and colleagues spell out this route for their classical comparison before presenting a nonexplosive alternative.[3]
Now change only the consequence relation. If there is an admissible interpretation satisfying p and ¬p but not q, then p, ¬p do not entail q under that relation. The contradiction remains; the arbitrary-conclusion step fails. This is a counterexample to explosion, not evidence that p and ¬p have become classically consistent.[3]
Knowledge Transfer¶
Classical propositional proofs and classical ontology reasoning literally share the same structure: host consequence, same-scope conflicting premises, arbitrary target and absence of an escape from entailment. Their proof presentations differ—rule derivation in one setting, empty classical model set in another—but the schema tested is the same.[1][3]
The phrase “an inconsistency contaminates everything” may be useful in organizational or software discussions, but it is only an analogy unless an actual consequence relation licenses every downstream conclusion. A defect that has a large but bounded blast radius is not logical explosion. This entry therefore remains domain-specific despite the portability of its warning.
Examples¶
Classical propositional proof. Mapped back: host = classical consequence; contradictory pair = P and ¬P in one premise set; arbitrary target = unrelated Q; entailment = P gives P∨Q, then ¬P and disjunctive syllogism give Q; closure = every Q is derivable from a theory that closes over the pair. Q need not describe the same subject as P.[3]
Classical description-logic knowledge base. Mapped back: host = classical model-theoretic entailment; contradictory pair = C(a) and ¬C(a) asserted together; arbitrary target = unrelated D(a); entailment = the knowledge base has no classical model, hence none that refutes D(a); closure = every query formula is formally entailed. This is a statement about the entailment relation, not a claim about a particular product's user interface.[3]
Nonexplosive contrast. Zhang and colleagues' quasi-classical account supplies p and ¬p with an interpretation that does not support unrelated q. The antecedent is present but the universal consequence condition fails, placing this case outside explosion rather than outside inconsistency.[3]
Structural Tensions¶
Familiar classical rules versus tolerance of inconsistent information. Keeping ordinary introduction and elimination rules preserves many standard derivations, but their combination can allow the arbitrary Q step. A paraconsistent alternative blocks unrestricted collapse, at the cost of changing which inferences remain valid. Diagnostic: Which exact rules or semantics support or block the target Q in this calculus?[3][2]
Sharp formal theorem versus human reasoning norm. Classical closure makes the consequence relation precise; a real agent need not infer or endorse every consequence of inconsistent beliefs. Treating formal closure as a psychological prediction gives explosion more reach than its proof establishes. Diagnostic: Is the claim about theoremhood, justified belief, an actual inference, or system output?[1]
Repair premises versus change consequence. One response removes or revises the contradiction; another keeps inconsistent information but changes the logic so unrelated conclusions do not follow. The former preserves classical inference after repair, while the latter retains more raw information but must specify a different consequence relation. Diagnostic: Is the research objective consistency of the premise set or useful nontrivial reasoning despite inconsistency?[3]
Structural–Framed Character¶
Evaluative weight. “Explosion” and “trivialization” sound undesirable, but schema validity is a formal matter; its desirability depends on one's logic and application. Human-practice dependence. Researchers choose a consequence relation and may assign normative significance to it, yet the derivation is fixed once rules and premises are fixed. Institutional origin. Logical traditions supply the terminology and calculi; no individual institution determines the rule's truth across all logics.[1][2]
Vocabulary travel. “Explosive” travels metaphorically into many domains, while the exact arbitrary-formula quantifier remains specialized. Import versus recognition. A new formalism literally instantiates the rule only after its premise language, negation, consequence relation and arbitrary-B test are specified. A cascading operational failure by itself does not pass that test.
Its character: formally structural within logic, but domain-specific as an Encyclopedia identity. Its value-laden interpretation and applied reasoning policy are separate from the consequence schema.
Structural Core vs. Domain Accent¶
Portable skeleton. A small local incompatibility can collapse global discrimination under a permissive propagation rule. That suggests a higher-order failure pattern, but this draft does not equate it with the named principle of explosion outside formal inference.
Domain accent. The inputs are formulas A and ¬A; the operator is a typed consequence relation; the target B ranges over every formula; and validity is assessed proof-theoretically or semantically. Paraconsistent countermodels test the exact boundary.[1][3]
Why not prime. The two demonstrated settings—formal proof and ontology reasoning—both use logical entailment. They show depth within logic, not literal independent transfer to nonlogical substrates. The screened prime-like intuition about unbounded spread is not enough to override that evidence.
Instantiates / Related Primes¶
Live Contradiction identifies a conflicting commitment condition; explosion is a rule about its possible inferential effect. The rule is not a subtype of that condition, nor does merely defining it require an actual contradictory theory. Live Paraconsistent Logic is the domain-specific contrast in which the unrestricted schema fails; Trivialism is a different global thesis about truth. No strict DAG edge is staged, and no canonical graph change was made.
Neighborhood in Abstraction Space¶
Principle of Explosion sits in a moderately populated region (49th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.
Family — Formal Models & Logical Foundations (33 abstractions)
Nearest neighbors
- Propositional logic — 0.86
- Modus ponens — 0.86
- Logical Consequence — 0.86
- Formal Theory — 0.86
- Logical or — 0.85
Computed from structural-signature embeddings · 2026-10-08
Not to Be Confused With¶
Bottom elimination, sometimes called ex falso quodlibet, is a rule from a falsum constant; its equivalence to the contradictory-pair schema depends on a calculus's treatment of negation and bottom, so it is not retained as an exact alias here. Disjunctive syllogism is one rule in one standard derivation, not itself the full arbitrary-conclusion schema. Paraconsistency is the failure of explosion, not the denial that contradictions can be expressed. A cascading software error can have large effects without entailing every proposition in a formal language.[2][3]
References¶
[1] Daniele Sgaravatti, “Explosion and Reasoning”, Episteme (2025), DOI 10.1017/epi.2025.6, especially pp. 1–2. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n
[2] Pedro Francisco Valencia Vizcaíno, “Relations between ex falso, tertium non datur, and double negation elimination” (2013), §§1–2 and Theorem 1. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g
[3] Xiaowang Zhang, Guohui Xiao, Zuoquan Lin and Jan Van den Bussche, “Inconsistency-Tolerant Reasoning with OWL DL”, International Journal of Approximate Reasoning 55, no. 2 (2014), 557–584, author-version PDF §§2.1–2.2. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k ↩l ↩m ↩n ↩o ↩p ↩q ↩r ↩s ↩t ↩u ↩v