How Robust Can Inconsistency Get?
John Woods[*]
“Inconsistency robustness is information system performance in the face of continually pervasive inconsistencies – a shift from the previously dominant paradigms of inconsistency denial and inconsistency elimination attempting to sweep them under the rug . Inconsistency robustness is both an observed dominant phenomenon and a desired feature: It is an observed phenomenon because large information systems are required to operate in an environment of pervasive inconsistency. It is a desired feature because we need to improve the performance of large information systems.”
Carl Hewitt
“We are all agreed that your theory is crazy. The question that divides us is whether it is crazy enough to have a chance of being correct.”
Neils Bohr to Wolfgang Pauli
I TECHNICAL CONSIDERATIONS
1. Inconsistency robustness logic
Inconsistency Robust Logic (IRL) is an adaptation of Carl Hewitt’s Direct Logic (DL).[1] DL is a logic that enables computers to carry out all inferences – including inferences about their own inferential processes – without the necessity of human intervention.[2] IRL is a logic built to accommodate the inconsistency robustness claims as set out in the epigraph just above. For my purposes here it will suffice to confine myself to some remarks about IRL’s DL component. In the case of inconsistency-pervasive[3] practical[4] theories, DL banishes proof by contradiction, as well as excluded middle and naïve -introduction.[5] The Hewitt quotation makes two related assertions. One I’ll call “the observability thesis” and the other “the desirability thesis.” The observability thesis says that the pervasiveness and persistence of inconsistency are empirically discernible in the performance behaviour of large practical systems. The desirability thesis asserts that this inconsistency is a necessary and advantageous feature, made so by the fact that “[c]urrent systems do not perform adequately in the face of inconsistency, and must be improved.”[6] Hewitt asserts that large inconsistent systems work better with the inconsistencies left in that is to say, robustly managed than they do with the inconsistencies swept under the rug – or denied entry in the first place.[7] When these two conditions are met, there is an allowable extension of the term in which it is the information system itself that is inconsistency robust.[8]
Of particular interest here is Hewitt’s proof of the self-proved consistency of mathematics, informally set out as follows.
- Suppose for contradiction that mathematics is inconsistent.
- So there is some proposition Φ of mathematics such that ⊦Φ and ⊦~Φ.
- From this we have an immediate contradiction: ⌐Φ ~Φ¬is a theorem of mathematics.
- So by reductio mathematics is consistent.[9]
If the proof stands up, it would now seem that we have an easy way to prove not the relative consistency of mathematics but its absolute consistency as well:
- Either mathematics is consistent or inconsistent.
- If consistent, well and good.
- If inconsistent, then consistent.
- So mathematics is consistent.
The trouble is that line (a) calls upon excluded middle, which Hewitt excludes from DL and IRL.
There is an even more threatening generalization of it to consider. Let be an arbitrarily selected theory and let ⊦ denote the relation ⌐Φ holds in ¬. Then
1. Suppose for contradiction that is inconsistent.
2. So there is some proposition Φ such that ⊦ Φ and ⊦ ~Φ.
3. From this we have an immediate contradiction: ⊦ (Φ ~Φ).
4. So by reductio is consistent.
But again,
a. Either is consistent or inconsistent.
b. If consistent, well and good.
c. If inconsistent, then consistent.
d. So is consistent.
Since is arbitrary, we have it then that
e. Every theory is consistent.
This is rather striking. For anyone at ease with excluded middle, Hewitt’s generalized proof does for consistency the sort of thing the Curry-proof did for truth.[10] That is, it proves that there is massively too much of it. This we might call “the paradox of consistency.”
I don’t want to overpress the Curry-proof resemblance. It hinges on my version of Hewitt’s own informal presentation of his proof. It does not hinge on the formal presentation of Hewitt’s proof as set out in DL. Hewitt’s informal proof is set out in non-technical English. My generalization of it is too. My Hewitt’s proof invokes rules and assumptions that fail in Hewitt’s own DL and IRL. Given their respective purposes, in DL and IRL, Hewitt may be right in making them fail there. But this is a long way from meaning that they should also fail for non-technical English. This qualifies the resemblance my proof of omni-consistency and Curry’s proof of omni-truth. But it does not obliterate it. When all is said and done, Curry’s is a proof about the English predicate “true”, and mine is a proof about the English predicate “consistent”. But if the crudity of saying so might be forgiven, the guts of my generalization of Hewitt’s informal proof are the guts of that proof too.
A second difficulty with the proof is that even if valid it does not appear to establish that it is mathematics itself that proves its own self-consistency. If so, it is hard to see how,as Hewitt himself avers,[11]it engages with, much less contradicts, the Gödel second incompleteness theorem. Of course the present formulation of the proof is a loosely informal one. The actual proof lies deep in the coils of DL.[12] The language of DL is purpose-built to pronounce upon its own doings, in ways that enable DL to prove theorems about itself. Assume now an extension of the language of DL – call it FADL which gives formal expression to the axioms of first-order arithmetic in a way that provides that if ⊦Φ and ⊦ψ, then ⊦(Φ ψ). Then as presented there, Hewitt’s proof must look something like this: If FADL is inconsistent, ⌐FADL is consistent¬ is provable in FADL. Supposing that all goes well, it still isn’t clear that Hewitt’s formal proof conflicts with Gödel’s. Gödel established that if FA is consistent, it is not provably so in FA. Of course, if excluded middle were allowed[13] the desired incompatibility would be solidly established, but only at the expense of a Curry-like result for consistency.
The Curry-like result also carries consequences for Hewitt’s more immediate concerns. If proof by contradiction were an allowable rule for arbitrary [14], there would be no such thing as inconsistency robustness. If anything’s robust here, it is consistency and in so saying conferences on inconsistency are now denied a coherent motivation. Hewitt is right to say that if inconsistency robustness is to be saved, it is essential that IRL suppress proof by contradiction. But robustness aside, if we merely wanted to give the plain old predicate “is inconsistent” a non-null extension, we would also have to disable proof by contradiction.[15] Thus the reach of Hewitt’s proof considerably outruns his preoccupation with inconsistency robustness.
We might think that a proof causing this much trouble is too delicious to be true.That certainly is Hewitt’s own view of the matter. Hewitt does not think that his proof causes trouble on any scale that would remotely approach the trouble caused by a Curry-like result for consistency. The reason for this is that he thinks that his proof doesn’t generalize in the way that I’ve suggested. What he does think is that the proof succeeds in showing that “it is only in practical pervasively inconsistent theories that” proofs by contradiction fail.[16] However, as Hewitt insists, it is the practical inconsistency-pervasive theories that are important for large systems.
My generalized version of Hewitt’s informal proof gives a result of sufficient excessiveness to justify the efforts to disarm it. One possibility is that the refusal of proof by contradiction rule, notwithstanding its dominant and necessary employment in the existing consistency proofs in standard mathematics. Another is the repudiation of adjunction. Since I myself am not much inclined to give up on adjunction, it would appear that proof by contradiction will have to go, in spite of Hewitt’s insistence that the proof by contradiction rule fails only for robustly inconsistent systems. So perhaps the present option requires further consideration.
Whether or not Hewitt is right in saying that my generalization of Hewitt’s informal proof is not a generalization of Hewitt’s Hewitt’s informal proof, I daresay that some readers will think that my proof is a validly serious discouragement of proof by contradiction beyond the confines of inconsistency robust theories. It certainly matters whether my Hewitt’s proof stands or falls. If it stands, inconsistency robustness doesn’t bear thinking bout. If it doesn’t fall, we’ll have to get clearer about how Hewitt’s Hewitt’s proof attains its exclusive attachment to IR contexts. That is not evident in Hewitt’s informal exposition of his proof. To get to the bottom of things, we would have to study the formal intricacies of IRL. But that is not my mission here.
Still, I don’t mean to make light of this matter. If perchance my generalized version of the proof were right, we would have to proceed with care. We would have to take pains to honour a distinction between a proof by contradiction and a reductio ad absurdum proof. Here is why. The case against proof by contradiction afforded by my generalization of Hewitt’s proof is itself advanced as a reductio argument, summarizable as follows:
1. Proof by contradiction is a valid rule.
2. Provided proof by contradiction is a valid procedure, it can be demonstrated
that everything whatever is consistent.
3. But this seems absurd.
4. So proof by contradiction is not a valid rule.[17]
All this is very interesting and important. But since my concern here – like Hewitt’s own – is with inconsistency robustness, I’ll turn to that now, leaving the intricacies of reductio reasoning and related matters for another time.
2. Is there a DL tie to paraconsistency?
A system is negation-inconsistent just in case for some sentence , both ⊦ and ⊦~. It is generally agreed that the defining feature of paraconsistent systems is their rejection of the ex falso quodlibet theorem, by which negation-inconsistency and absolute consistency are strictly equivalent properties; in particular, by which everything whatever can be proved from a negation-inconsistency. In other words, ex falso-compliant systems detonate on the presence of any contradictory pair of theorems; which is the very thing that paraconsistentists want to avoid. This raises the question of how a paraconsistent system should manage its negation-inconsistencies. A dominant answer bids us to find (or define) one or more premiss-conclusion relations for which ex falso fails but which is property-preserving with respect to some desirable property or properties other than truth. In some approaches this property to be preserved is “bad, but not too bad”. Its preservation requires that in its management of the logic things are not made worse. If ex falso held true, this would be a forlorn hope. Negation-inconsistency is bad, but not too bad if it is carefully treated. But in ex falso logics, the system is handled in ways that make everything inconsistent. That’s bad too, but shockingly worse.[18]
Paraconsistent logics divide fairly neatly into two camps. In the one, ex falso is blocked by imposition of relevance constraints on entailment and deducibility. In the other, ex falso is blocked in some other way, for example, by suppressing the rule of adjunction, without the need to impose a relevance condition. See, in this regard, Nicholas Rescher and Robert Brandom, The Logic of Inconsistency.[19] At the time of its publication, most of the paraconsistent work done by American logicians was of this first type. Indeed some of the leading relevant logicians were Rescher’s colleagues at the University of Pittsburgh. But Rescher himself, and Brandom too, are in this second camp, in the slipstream of paraconsistent developments in Poland and Brazil. The paraconsistent terrain in Australia tended to subdivide into dialethic logic and relevant logic, with some concomitant overlap. The paraconsistent turn in Canada is substantially influenced by preservationist adaptations of Rescher and Brandom, got by weakening some of the latter’s inferential constraints.[20] Also important are Belgium’s contributions to adaptive logic. The Rescher and Brandom essay is a response to two different impulses. One is the impulse to free set theory from the Russell contradiction, and to do so with least possible disturbance of the theory’s original intuitions. The other is to have a logic that is duly sensitive to the particularities of assertion. Accordingly we might propose that
Ex falso questionable for assertion: A relation that preserves theoremhood woud seem to be more ex falso-friendly than a relation that preserves assertion.
Although these are clearly inequivalent objectives, they embedded a common strategy. It entailed, in the manner of Jáskowski, the suppression of the adjunction rule, the rule that permits unrestricted premiss-aggregation. This disables the classical equivalence of {A, B, C, } ⊦ X and ⌐A B C¬⊦ X.[21]
Towards the end of The Logic of Inconsistency, we find the idea of an “intelligible” formal system. Clearly a technical term, a formal system is intelligible just in case it meets the following three conditions. (1) Its theorems include all the logical truths. (2) No self-contradiction is a theorem. (3) Any classical consequence of a theorem is a theorem. However condition (3) doesn’t apply to sets of theorems. An intelligible formal system not only isn’t closed under conjunction, it may also prove contradictory pairs of theorems (but not their conjunctions).
These days, there is a hefty multiplicity of paraconsistent logics, mainly inequivalent and often one another’s rivals. Comparing DL with paraconsistent logic as such is too much to hope for. So far, there is only one of it, and too many of them. Still some things are clear. As we saw, DL proves the self-consistency of formal arithmetic. Again, the proof informally rendered is this.
- Suppose for reductio that FA is inconsistent.
- For some , ⊦FA and ⊦FA ~ from 1, by def. of inconsistency
- ⊦FA ( ~)from 2, by adjunction
- FA is consistentfrom 3, by proof by contradiction
and double negation.
One of Hewitt’s tasks is to disable this proof. It is interesting to take note of theremedies he doesn’t apply here. Unlike all non-adjunctive paraconsistent systems,Hewitt doesn’t suppress adjunction. Unlike most breeds of paraconsistentism, hedoesn’t press the objection that if and ⌐~¬ were allowed to stand as theorems ofFA, FA would be up to its eyeballs with endlessly more contradictory theorem-pairs.Nor, unlike relevant paraconsistents, is there any overt concern with ex falso. ForHewitt, the overriding fact is that FA proves an outright contradiction which is in immediate and direct contradiction of the law of noncontradictionLNC. This is a point of pivotal importance, dispossessing all other concerns of a place at the table. If FA proves and ⌐~¬ it violates LNC, and that fact alone is wholly decisive; it constitutes the entire case against it. Whereupon it is immediate that FA is not inconsistent.
Later on I will have something to say about Aristotle’s version of his own noncontradiction law. All we need say about it now is that there is no traceof Aristotle’s interest in the equivalence or otherwise of contradictory pairs of propositions and contradictory conjunctions of them. Such textual support as we have indicates that the closest Aristotle comes to the modern LNC is in a contradictory- pairs formulation of it.
Hewitt’s remedy is to retain the contradictory conjunction reading while
concurrently disabling the proof by contradiction rule. It is a risky move, as no one knows better than he. The proof by contradiction rule is indispensable for mainstream mathematics. Hewitt will need to do two things at once. He will need to keep the proof rule in general circulation while clipping its wings here. The desired accommodation will be provided in IRL, which is a purpose-built adaptation of DL. IRL has a number of interesting properties. One is its suppression of self-reference. Another is the welcome it extends to pervasive and wholly entrenched inconsistencies in very largeinformation systems. In the first instance, IRL takes a quite orthodox approach toinconsistency-producing self-reference. It banishes self-reference. In the second, it is in a league by itself.
3. Thought-to-be consistency
Hewitt is strongly of the view that the proof by contradiction rule is both allowed by and is indispensable for "thought-to-be consistent" mathematical theories. Suppose, however, a given thought-to-be-consistent theory in fact were inconsistent. Hewitt is adamant that "you can't prove everything." But this is precisely what you can do if ex falso is true. Everything could be proved if the system has -elimination, -introduction, and double negation. DL disallows -introduction but admits the others. Would that make DL a paraconsistent logic?
Perhaps not. Might we not get ex falso in other ways, and more directly, from the definition of ⊧: Φ ⊦ ψ iff ~◊ (Φ ~ψ). If the system is sound and complete, the same holds for ⊦: Φ⊦ ψ iff ~⊦ (Φ ~ψ). Putting ⌐A ~A¬for Φ and ~B for ψ, we now have it that A ~A ⊧~ ~B, for any B. Since double negation holds in DL, this gives it that A ~A ⊧ B. Wouldn't this make DL a non-paraconsistent detonating logic? If so, wouldn't this also imperil Hewitt’s thought-to-be-consistent rescue of proof by contradiction for all systems, except for those very particular ones in which it is excluded as a matter of policy?
A related issue concerns IR systems. IR systems are not only inconsistent but are discernibly so. They wear their inconsistencies on their sleeves. If, as suggested, DL allowedex falso, here too IR systems would detonate, and everything would be provable there, never mind whether proof by contradiction is also allowed. Hewitt says that DL must allow proof by contradiction for all systems thought-to-be consistent. That way the business of mathematics can be transacted comme d'habitude.
In fact, however, DL avoids these difficulties, on a technicality we might say. DL isn’t a model theoretic logic and has no capacity (or wish) to express or regulate “◊” and “⊧”. Why would we say that this problem is avoided “only on a technicality”? I say it because the modal definition of ⊧ might be true and the derivation of ex falso might follow from it validly. If these things actually were so, their not being so in DL would cause them no discouragement, but is it not fairly called into question whether DL is the logic we should want for mathematics?
What does it take to fulfill the "thought-to-be" condition? If it means "is, for the sake of mathematics, taken to be “or"is, for the sake of mathematics, stipulated to be", then why wouldn't we apply this face-saving measure even to systems that are discernibly inconsistent? Hewitt’s answer is that this not what the thought-to-consistent qualification comes to. “By a ‘thought-to-be consistent mathematical theory’, I mean one that is thought to be consistent by the overwhelming consensus of working professional mathematicians.”[22] Examples include the second order axiomatizations of the integers and reals, Hilbert spaces, and group theory. So it is clear that the final occurrence of “thought” in the quoted sentence means “widely believed by the experts.”