[FOM] "Hidden" contradictions
hewitt at concurrency.biz
Sun Aug 25 20:44:03 EDT 2013
On Aug 24, Steven Ericsson-Zenith wrote:
> "Mathematics and mathematical logic have
> dealt with and contained "inconsistencies" all along -
> and have provided adequate means to reason about them.
> The inadequacies of software systems will not, it seems to me,
> be aided by encouraging, or resigning ourselves to,
> a lack of rigor or disciplined effort in that field."
Unfortunately, classical mathematical logic is not up to the task
of reasoning about large software systems with pervasive inconsistences.
For example, since it is not wise to use proof by contradiction,
resolution theorem proving is not a technology that you would want to use
to infer conclusions about large software systems.
Fortunately, we don't have to buy into your conclusion that
not using classical logic means
"encouraging, or resigning ourselves to, a lack of rigor or disciplined effort."
Inconsistency Robust Logic (beginning with Stanisław Jaśkowski) has developed to the point where
there is a proposal on the table for use in software engineering (see http://arxiv.org/abs/0812.4852).
Developing such rigorous Inconsistency Robust Logic suitable for software engineering
has taken a century of disciplined effort by many excellent logicians.
Instead of disparagement, we can celebrate the scientific advance.
More information about the FOM