Carl Hewitt
on “The Logical Necessity of Inconsistency” (at Edinburgh)
Edinburgh LFCS Seminar
4pm Tuesday 11th September 2007
Room 2511, JCMB, King's Buildings
http://www.lfcs.inf.ed.ac.uk/events/theory-seminars/
The Logical Necessity of Inconsistency
MIT EECS
(emeritus)
It is well known that large
software systems are chock full of inconsistencies among their documentation,
use cases, and code. In a way, this is a good thing because if large software
systems were required to be consistent, then they would not exist. Fortunately,
the rules of classical logic can be modified in order to safely reason about such
systems. Direct Logic [Hewitt COIN@AAMAS’07] is an unstratified reflective
paraconsistent system (with mathematical induction) that is suitable for
reasoning about inconsistent theories for large software systems.
However, a paraconsistent theory T of Direct Logic necessarily has an
inconsistency for logical reasons by the following argument:
Using the Carnap fixed point
theorem it is easy to construct a sentence ParadoxT such that it is provable in T that:
(1) ParadoxT if an only if (ParadoxT is not provable in T)
It follows (by some fundamental
principles of Direct Logic) that the following are provable in T:
(2) ParadoxT is not provable in T
(3) (not ParadoxT)
is not provable in T
The combination of (2) and
(3) is called “incompleteness” because it says that T is incomplete with
respect to ParadoxT
(an idea first published by Gödel).
So far so good. However, using (1) and (2)
it follows that ParadoxT
is provable in T. Consequently, it is provable in T that
(4) ParadoxT is provable in T because if a
sentence is provable in T, then it is provable in T that the sentence is
provable in T.
But now we have an inconsistency
in T between (1) and (4). It is important to note that the proof
of inconsistency of T is paraconsistent. I.e., the proof does not assume
that T is consistent (unlike the incompleteness theorems of Gödel and Rosser).
Also, the concept of TRUTH has already been hard hit by the pervasive
inconsistencies of large software systems. Accepting the necessary logical
inconsistency discussed above would be another nail in its coffin.
But all is not lost because the following can be said about the
logically necessary inconsistency with respect to the provability in T of
ParadoxT:
* Because T is paraconsistent,
that T is inconsistent about the provability in T of ParadoxT (by itself) should not affect
other reasoning. Also the subject matter of the provability in T of ParadoxT is not of general interest in
software engineering and should not affect reasoning about current large
software systems. So do software engineers need to care that T is inconsistent
about provability in T of ParadoxT
as opposed to all the other inconsistencies of T which they care about more?
* This logically necessary
inconsistency is a nice illustration of how inconsistencies often manifest in
large software systems: “there can be good arguments on both sides for
contradictory conclusions”.
A big advantage of paraconsistent logic is that it makes fewer mistakes
than classical logic when dealing with inconsistent theories. Since software
engineers have to deal with theories chock full of inconsistencies,
paraconsistency should be attractive. However, to make it relevant we need to
provide them with tools that are cost effective.
Logical
Necessity of Inconsistency