Roughly speaking, I'm wondering if it's possible to meaningfully grade different systems on how explosion-tolerant they are.
In classical sentential logic and intuitionistic sentential logic, a single contradiction P ∧ ¬P lets you conclude any well-formed formula.
Let T be the set of theorems and L be the set of the well-formed formulas. Let φ be a particular contradictory well-formed formula that is not a theorem in T.
If we take the closure of T ∪ {φ} under the inference rules in an explosive system, we get back L .
If we take a system with no inference rules at all, then the closure of T ∪ {φ} is just T ∪ {φ} . We would get no spurious theorems besides the contradiction. So the system with no inference rules is "minimally explosive".
In general, can we distinguish different non-explosive logics from each other by characterizing what the consequences are of accepting a contradictory premise / temporarily adopting a contradictory axiom? Is this a useful way of thinking about different paraconsistent logics?
As far as I can tell, an explosion-tolerant logic is one that does not admit the following the following inference rule.
P ∧ ¬P
------
Q
So then, by the contrapositive of the deduction theorem, it suffices to show that (P ∧ ¬P) → Q is not a tautology.
There's a simple three-valued logic given here defines the connectives in terms of truth tables:
neg P → Q Q P ∨ Q Q P ∧ Q Q
P ¬P 1 ? 0 1 ? 0 1 ? 0
---- +----- +----- +-----
1 0 1 |1 ? 0 1 |1 1 1 1 |1 ? 0
? ? P ? |1 ? 0 P ? |1 ? ? P ? |? ? 0
0 1 0 |1 1 1 0 |1 ? 0 0 |0 0 0
For the purposes of identifying tautologies, the two designated truth values are T/1 and ?
In order to show that (P ∧ ¬P) → Q is not a tautology, we consult the truth table and work backwards, as shown below.
1. (P ∧ ¬P) → Q falsifiable
2. Q false and P ∧ ¬P non-false
3. if P is "?", then P ∧ ¬P is non-false
4. {P="?", Q=⊥} witnesses the falsifiability of (P ∧ ¬P) → Q
This example does a good job of showing us why the asymmetry in the definition of → is there. A premise whose truth value is ? is treated just like a true premise.
It certainly seems like the set of theorems doesn't grow much in this system if a contradictory premise is assumed. I think that with the assumption of P ∧ ¬P, you only get P and ¬P through conjunction elimination, but I'm not sure how to prove that.
Also, there might be other paraconsistent logics that are less tolerant of contradictory premises than this one.
