Lambda the Ultimate

Inconsistency robustness is “information system performance in the face of continually pervasive inconsistencies.” Inconsistency robustness is both an observed phenomenon and a desired feature:
• It is an observed phenomenon because large information systems are required to operate in an environment of pervasive inconsistency. How are they doing?
• It is a desired feature because we need to improve the performance of large information systems

This paper explores the role of Inconsistency Robustness in the history and theory of Logic Programs. Inconsistency Robustness has been a continually recurring issue in Logic Programs from the beginning including Church's system developed in the early 1930s based on partial functions (defined in the lambda calculus) that he thought would allow development of a general logic without the kind of paradoxes that had plagued earlier efforts by Frege, Russell, etc. Unfortunately, Church's system was quickly shown to be inconsistent because:
• His system allowed the kind of self-referential propositions introduced by Gödel using fixed points on a (implicit) overly loose grammar of mathematical sentences.
• Church thought that a general system must be able to computationally enumerate its theorems
In the face of the contradictions, Church abandoned the quest for a general foundation and subsequently used the lambda calculus solely for the purpose of computation.

[Kowalski 1988] advocated a bold thesis: “Looking back on our early discoveries, I value most the discovery that computation could be subsumed by deduction.” However, mathematical logic cannot always infer computational steps because computational systems make use of arbitration for determining which message is processed next by a recipient that is sent multiple messages concurrently. Since reception orders are in general indeterminate, they cannot be inferred from prior information by mathematical logic alone. Therefore mathematical logic alone cannot in general implement computation. Logic Programs (like Functional Programs) are useful idioms even though they are not universal. For example Logic Programs can provide useful principles and methods for systems which are quasi-commutative and quasi-monotonic even though the systems themselves cannot be implemented using Logic Programs.

According to [Feferman 2008]:"So far as I know, it has not been determined whether such [inconsistency robust] logics account for 'sustained ordinary reasoning', not only in everyday discourse but also in mathematics and the sciences." Direct Logic is put forward as an improvement over classical logic with respect to Feferman’s desideratum above using
• Inconsistency Robust Direct Logic for pervasively inconsistent theories of practice, e.g., theories for climate modeling and for modeling the human brain
• Classical Direct Logic (augmentation of Inconsistency Robust Direct Logic with the rule of Proof by Contradiction) for theories thought to be consistent by an overwhelming consensus of working professional mathematicians
The claim is made that Inconsistency Robust Direct Logic is an improvement over classical logic with respect to Feferman’s desideratum above for today's information systems that are perpetually, pervasively inconsistent. Information technology needs an all-embracing system of inconsistency-robust reasoning to support practical information integration. Having such a system is important in computer science because computers must be able to carry out all inferences (including inferences about their own inference processes) without relying on humans.

Independent developments by different research groups in the fall of 1972 gave rise to a controversy over Logic Programs that persists to this day in the form of following alternatives:
1. Logic Programs using procedural interpretation of program-clause syntax (Logic Programs are Y⇐F₁, ..., F_n where Y and each of the F_i is a literal proposition or its negation (i.e., either P[t₁, ..., tn] or ¬P[t₁, ..., t_n] for some atomic predicate P and terms t_i.)
2. Logic Programs in which each computational step (e.g. using the Actor Model of computation) is logically inferred (e.g. using Direct Logic)
This article argues for the second alternative based on the following considerations:
• Programs in program-clause syntax are a special case of the second alternative because each computational step of a program in program-clause syntax is logically inferred.
• Reducing propositions to program-clause syntax can obscure their natural structure.
•Procedural interpretation of program-clause syntax does can obscure the natural structure of proofs (e.g. Natural Deduction using Direct Logic).

Consequently, Direct Logic is proposed as a foundation for Logic Programs.

Going beyond the limitations of program-clause syntax, a core subset of Logic Program constructs is presented in this article (using explicit assertions and goals to invoke pattern-directed procedures) that are applicable to both mathematical theories and theories of practice.

The above examples are intended to be case studies in Inconsistency Robustness in which information is formalized, contradictions are derived using Inconsistency Robust reasoning, and arguments are formalized for and against contradictory propositions. A challenge for the future is to automate the reasoning involved in these case studies.

Above abstract is from  the full article