Appendix: Examples Challenging the Paradigm
In previous sections, it has been suggested that one interesting approach to the problem of paradoxes of implication is to draw a distinction between two ways of combining assumptions, symbolised by a comma and a semicolon. Logic can be re-formulated in this way, giving a "relevant" logic, called system R in the literature on non-classical logics. It has also been noted that one way of dealing with the problem of vagueness is to re-formulate logic similarly, with a slight adjustment to the rules, giving a "fuzzy" logic which we are calling F*. The two logics R and F* share a great deal of their structure, and mostly they agree on the nature of derivation and proof. They are not the same, however: their differences are as important as their similarities. For the details, see the technical appendix in which their proof rules are specified.
F* is less well investigated than R, but it can be found in the literature under the name DBCK. Another alternative to formulating it with the rule K or exportation would be to allow vacuous discharge as in the natural deduction system for classical logic.The objects on the left side of sequents no longer represent sets of formuae, but rather bunches which are built out of their parts by applying two operations: the comma, as in classical logic, stands for set union, while the semicolon is something different, serving as a residue of the way assumptions have been used in the derivation of the conclusion. Since the two operations may be nested inside each other to any finite depth, bunches may grow to be objects of considerable complexity.
Proofs in the non-classical logics formulated here have a slightly different style from that of classical proofs, as we often need to make moves that adjust the assumption numbers as well as regular inference moves transforming the formulae. A few examples will serve to illustrate.
The first example does not require either of the special structural rules W or K, so it works in both logics.
Proof 1 (in R and F*)
SP {p IMP q, p IMP r ⊢ p IMP (q AND r)} PL {1} {1} {p IMP q} {A} PL {2} {2} {p IMP r} {A} PL {3} {3} {p} {A (for IMPI)} PL {1;3} {4} {q} {1, 3 IMPE} PL {2;3} {5} {r} {2, 3 IMPE} PL {(1;3) , (2;3)} {6} {q AND r} {4, 5 ANDI} PL {((1,2);3) , (2;3)} {7} {q AND r} {6 eK} PL {((1,2);3) , ((1,2);3)} {8} {q AND r} {7 eK} PL {(1,2);3} {9} {q AND r} {8 eW} PL {1,2} {10} {p IMP (q AND r)} {9 [3] IMPI} EPIf try it yourself, note that the proof editor helpfully cuts a few corners, for instance by allowing multiple uses of eK in one step, and by making eW implicit rather than asking you to make that move yourself—so it allows you to go from line 5 directly to line 9 in one step of eK.
The second example requires contraction (W) for semicolon, or its equivalent "import". It is a legitimate proof in relevant logic, but not in a logic suitable for vagueness:
Proof 2 (in R)
SP {p IMP q, q IMP r ⊢ p IMP r} PL {1} {1} {p IMP q} {A} PL {2} {2} {q IMP r} {A} PL {3} {3} {p} {A} PL {1;3} {4} {q} {1, 3 IMPE} PL {1;2;3} {5} {r} {2, 4 IMPE} PL {(1,2);3} {6} {r} {5 import} PL {1,2} {7} {p IMP r} {8 [3] IMPI} EPAgain note that the proof editor collapses the rules W and importation into one rule which is calls "contraction". Similarly, in a logic like F* which allows weakening for both comma and semicolon, the proof editor runs K and exportation together, calling them both "weakening". The weakening rule also absorbs eK, so that rule is not explicit in F* either. All of this is designed to shorten proofs by reducing the number of annoying low-level appeals to structural rules.
The third example is the logical theorem saying that assumptions accumulate into a conjunction: "If we had a little bread we could have bread and cheese if we had some cheese." This is provable in a logic satisfying the rule K (or "export"), but not in relevant logic.
Proof 3 (in F*)
SP {⊢ p IMP (q IMP (p AND q))} PL {1} {1} {p} {A} PL {2} {2} {q} {A} PL {1,2} {3} {p AND q} {1, 2 ANDI} PL {1;2} {4} {p AND q} {3 export} PL {1} {5} {q IMP (p AND q)} {4 [2] IMPI} PL {TEE} {6} {p IMP (q IMP (p AND q))} {5 [1] IMPI} EPFor the walkthrough of these three proofs, click here.
The common core of R and F* is quite large. Much of the logic of implication goes through in the same way as it does classically. For instance:
Proof 4 (in R and F*)
SP {p IMP (q IMP r) ⊢ (s IMP q) IMP (s IMP (p IMP r))} PL {1} {1} {p IMP (q IMP r)} {A} PL {2} {2} {s IMP q} {A} PL {3} {3} {s} {A} PL {4} {4} {p} {A} PL {1;4} {5} {q IMP r} {1, 4 IMPE} PL {2;3} {6} {q} {2, 3 IMPE} PL {1;2;3;4} {7} {r} {5, 6 IMPE} PL {1;2;3} {8} {p IMP r} {7 [4] IMPI} PL {1;2} {9} {s IMP (p IMP r)} {8 [3] IMPI} PL {1} {10} {(s IMP q) IMP (s IMP (p IMP r))} {9 [2] IMPI} EPSimilarly, the relationships between conjunction and disjunction are largely the same as they are classically. De Morgan's duality laws are all straightforwardly provable, for instance. Here is one of them:
Proof 5 (in R and F*)
SP {NOT(p AND q) ⊢ NOTp OR NOTq} PL {1} {1} {NOT(p AND q)} {A} PL {2} {2} {NOT(NOTp OR NOTq)} {A} PL {3} {3} {NOTp} {A} PL {3} {4} {NOTp OR NOTq} {3 ORI} PL {2} {5} {NOTNOTp} {2, 4 [3] RAA} PL {2} {6} {p} {5 NOTNOTE} PL {7} {7} {NOTq} {A} PL {7} {8} {NOTp OR NOTq} {8 ORI} PL {2} {9} {NOTNOTq} {2, 8 [7] RAA} PL {2} {10} {q} {9 NOTNOTE} PL {2,2} {11} {p AND q} {7, 12 ANDI} PL {2} {12} {p AND q} {13 eW} PL {1} {13} {NOTNOT(NOTp OR NOTq)} {1, 12 [2] RAA} PL {1} {14} {NOTp OR NOTq} {13 NOTNOTE} EPThe next example is one version of the disjunctive syllogism, which is not relevantly valid, of course, and indeed is unprovable in R because it requires the semicolon to satisfy weakening. It is valid in the canvassed fuzzy logic F*, as it does not require contraction:
Proof 6 (in F*)
SP {p OR q; NOTp ⊢ q} PL {1} {1} {p OR q} {A} PL {2} {2} {NOTp} {A} PL {3} {3} {p} {A} PL {4} {4} {NOTq} {A} PL {3;4} {5} {p} {3 K} PL {2;3} {6} {NOTNOTq} {2, 5 [4] RAA} PL {2;3} {7} {q} {6 NOTNOTE} PL {8} {8} {q} {A} PL {2;8} {9} {q} {8 K} PL {1;2} {10} {q} {1, 7 [3], 9 [8] ORE} EPFinally, here is the "law of the excluded middle", proved in relevant logic in much the same way as it is proved classically:
Proof 7 (in R)
SP {⊢ p OR NOTp} PL {1} {1} {NOT(p OR NOTp)} {A} PL {2} {2} {p} {A} PL {2} {3} {p OR NOTp} {2 ORI} PL {1} {4} {NOTp} {1, 3 [2] RAA} PL {1} {5} {p OR NOTp} {4 ORI} PL {TEE} {6} {NOTNOT(p OR NOTp)} {1, 5 [1] RAA} PL {TEE} {7} {p OR NOTp} {6 NOTNOTE} EPThe tricky move here is the RAA at line 6, which effectively discharges two occurrences of assumption 1. If we were to write it out laboriously, we might see something like:
SP {} PL {1;1} {6} {BAD} {1, 5 NOTE} PL {1} {7} {BAD} {6 W} PL {TEE} {8} {NOTNOT(p OR NOTp)} {7 [1] NOTI} PL {TEE} {9} {p OR NOTp} {8 NOTNOTE} EP