Carl Hewitt

Stanisław Jaśkowski

John Mccarthy

Marvin Minsky

Formalizing common sense reasoning for scalable inconsistency-robust

come     Copyright Formalizing common sense reasoning for scalable inconsistency-robust information coordination using Direct Logic™ Reasoning and the Actor Model

 [START_REF] Jaśkowski | Propositional calculus for contradictory deductive systems[END_REF]stated the following initial goal:

"To find a system [for inconsistency robust inference]  which: 1) when applied to contradictory [information] would not always entail overcompleteness [i.e. infer every proposition] 2) would be rich enough for practical inference 3) would have an intuitive justification" According to [START_REF] Feferman | Axioms for determinateness and truth[END_REF]: 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 first-order logic with respect to Feferman's desideratum above using the following:  Inconsistency Robust Direct Logic for pervasively inconsistent theories of practice i  Classical Direct Logic for use of consistent mathematical theories in inconsistency robust theories Direct Logic is an improvement over first-order logic with respect to Feferman's desideratum above for today's information systems that are perpetually, pervasively inconsistent. Information technology needs an allembracing system of inconsistency-robust reasoning to support practical information coordination. 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 Consequently, Direct Logic is proposed as a standard to replace firstorder logic as a mathematical foundation for Computer Science.

Since the global state space model of computation (first formalized by [Church 1935 followed by [START_REF] Turing | On computable numbers, with an application to the Entscheidungsproblem[END_REF]) is inadequate to the needs of modern large-scale Internet applications the Actor Model was developed to meet this need.

Hypothesis: ii All physically possible computation can be directly modeled and implemented using Actors.

i e.g., theories for climate modeling and for modeling the human brain ii This hypothesis is an update to [Church 1936] that all physically computable functions can be implemented using the lambda calculus. It is a consequence of the Actor Model that there are some computations that cannot be implemented in the lambda calculus.

Introduction

"Beneath the surface of the world are the rules of science. But beneath them there is a far deeper set of rules: a matrix of pure mathematics, which explains the nature of the rules of science and how it is that we can understand them in the first place." Malone [2007] Our lives are changing: soon we will always be online. People use their common sense interacting with large information systems. This common sense needs to be formalized. i

Large-scale Internet software systems present the following challenges:

1. Pervasive inconsistency is the norm and consequently first-order logic infers too much, i.e., anything and everything. Inconsistencies (e.g. that can be derived from implementations, documentation, and use cases) in large software systems are pervasive and despite enormous expense have not been eliminated. 2. Concurrency is the norm. Logic Programs based on the inference rules of mathematical logic are not computationally universal because the message order reception indeterminacy of concurrent computations in open systems cannot be deduced using mathematical logic from propositions about pre-existing conditions. The fact that computation is not reducible to logical inference has important practical consequences.

For example, reasoning used in information coordination cannot be implemented using logical inference [Hewitt 2008a].

This paper suggests some principles and practices formalizing common sense approaches to addressing the above issues.

Interaction creates Reality 2 "[We] cannot think of any object apart from the possibility of its connection with other things." Wittgenstein, Tractatus i Eventually, computer systems need to be able to address issues like the following:  What will be the effects of increasing greenhouse gasses?  What is the future of mass cyber surveillance?  What can done about the increasing prevalence of metabolic syndrome?

According to [Rovelli 2008]: "a pen on my table has information because it points in this or that direction. We do not need a human being, a cat, or a computer, to make use of this notion of information." i Relational physics takes the following view [Laudisa and Rovelli 2008]:

• Relational physics discards the notions of absolute state of a system and absolute properties and values of its physical quantities. • State and physical quantities refer always to the interaction, or the relation, among multiple systems. ii • Nevertheless, relational physics is a complete description of reality. iii According to this view, Interaction creates reality. 3

Information is a generalization of physical information in Relational Physics

Information, as used in this article, is a generalization of the physical information of Relational Physics. iv Information systems participate in reality and thus are both consequence and cause. Science is a large information system that investigates and theorizes about interactions. So how does Science work?

i Rovelli added: "This [concept of information] is very weak; it does not require [consideration of] information storage, thermodynamics, complex systems, meaning, or anything of the sort. In particular: i.

Information can be lost dynamically ([correlated systems can become uncorrelated]); ii.

[It does] not distinguish between correlation obtained on purpose and accidental correlation; iii.

Most important: any physical system may contain information about another physical system." He added, "Information is exchanged via physical interactions. and furthermore, It is always possible to acquire new information about a system."

ii "In place of the notion of state, which refers solely to the system, [use] the notion of the information that a system has about another system." iii Furthermore, according to [Rovelli 2008], "quantum mechanics indicates that the notion of a universal description of the state of the world, shared by all observers, is a concept which is physically untenable, on experimental grounds. In this regard, [START_REF] Feynman | Lecture 6: Probability and Uncertainty -the Quantum Mechanical view of Nature" The Character of Physical Law[END_REF]] offered the following advice: "Do not keep saying to yourself, if you can possibly avoid it, 'But how can it be like that?' because you will go 'down the drain,' into a blind alley from which nobody has yet escaped." iv Unlike physical information in Relational Physics [Rovelli 2008, page 10], this paper does not make the assumption that information is necessarily a discrete quantity or that it must be consistent.

According to [Law 2004, emphasis added]: "… scientific routinisation, produced with immense difficulty and at immense cost, that secures the general continued stability of natural (and social) scientific reality. Elements within [this routinisation] may be overturned… But overall and most of the time, … it is the expense [and other difficulties] of doing otherwise that allows [scientific routinisation] to achieve relative stability. So it is that a scientific reality is produced that holds together more or less." 4 He added that we can respond as follows: "That we refuse the distinction between the literal and the metaphorical (as various philosophers of science have noted, the literal is always 'dead' metaphor, a metaphor that is no longer seen as such). … That we work allegorically. That we imagine coherence without consistency."

[emphasis added]

The coherence envisaged by Law (above) is a dynamic interactive ongoing process among humans and other objects.

Pervasive Inconsistency is the Norm in Large Software Systems "… find bugs faster than developers can fix them and each fix leads to another bug" Cusumano & Selby, 1995, p. 40 The development of large software systems and the extreme dependence of our society on these systems have introduced new phenomena. These systems have pervasive inconsistencies among and within the following: 5  Use cases that express how systems can be used and tested in practice. 6  Documentation that expresses over-arching justification for systems and their technologies. 7  Code that expresses implementations of systems Adapting a metaphor used by Popper 8 for science, the bold structure of a large software system rises, as it were, above a swamp. It is like a building erected on piles. The piles are driven down from above into the swamp, but not down to any natural or given base; and when we cease our attempts to drive our piles into a deeper layer, it is not because we have reached bedrock. We simply pause when we are satisfied that they are firm enough to carry the structure, at least for the time being. Or perhaps we do something else more pressing. Under some piles there is no rock. Also some rock does not hold.

Different communities are responsible for constructing, evolving, justifying and maintaining documentation, use cases, and code for large, software systems. In specific cases any one consideration can trump the others.

Sometimes debates over inconsistencies among the parts can become quite heated, e.g., between vendors. In the long run, after difficult negotiations, in large software systems, use cases, documentation, and code all change to produce systems with new inconsistencies. However, no one knows what they are or where they are located! "A large software system is never done." [START_REF] Rosenberg | Dreaming in Code[END_REF]]. 9 With respect to detected contradictions in large information systems, according to [START_REF] Russo | Making Inconsistency Respectable in Software Development[END_REF]:

"The choice of an inconsistency handling strategy depends on the context and the impact it has on other aspects of the development process. Resolving the inconsistency may be as simple as adding or deleting information from a software description. However, it often relies on resolving fundamental conflicts, or taking important design decisions. In such cases, immediate resolution is not the best option, and a number of choices are available:

 Ignore -it is sometimes the case that the effort of fixing an inconsistency is too great relative to the (low) risk that the inconsistency will have any adverse consequences. In such cases, developers may choose to ignore the existence of the inconsistency in their descriptions. Good practice dictates that such decisions should be revisited as a project progresses or as a system evolves.  Defer -this may provide developers with more time to elicit further information to facilitate resolution or to render the inconsistency unimportant.

In such cases, it is important to flag the parts of the descriptions that are affected, as development will continue while the inconsistency is tolerated.  Circumvent -in some cases, what appears to be an inconsistency according to the consistency rules is not regarded as such by the software developers. This may be because the rule is wrong, or because the inconsistency represents an exception to the rule that had not been captured. In these cases, the inconsistency can be circumvented by modifying the rule, or by disabling it for a specific context.  Ameliorate -it may be more cost-effective to 'improve' a description containing inconsistencies without necessarily resolving them all. This may include adding information to the description that alleviates some adverse effects of an inconsistency and/or resolves other inconsistencies as a side effect.

In such cases, amelioration can be a useful inconsistency handling strategy in that it moves the development process in a 'desirable' direction in which inconsistencies and their adverse impact are reduced."

In this regard it is important to note that "eventual consistency" 10 is a misnomer in the sense that in a large operational IoT system updates can be continually arriving. Consequently at any given time, concurrent accesses can return inconsistent values.

Inconsistency Robustness

"You cannot be confident about applying your calculus until you know that there are no hidden contradictions in it." i Turing circa 1930. 11 "Indeed, even at this stage, I predict a time when there will be mathematical investigations of calculi containing contradictions, and people will actually be proud of having emancipated themselves from consistency." Wittgenstein circa 1930. 12 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. ii In fact, inconsistencies are pervasive throughout our information infrastructure and they affect one another. Consequently, an interdisciplinary approach is needed.

There are many examples of inconsistency robustness in practice including the following:

• Our economy relies on large software systems that have tens of thousands of known inconsistencies (often called "bugs") along with tens of thousands more that have yet to be pinned down even though their symptoms are sometimes obvious. • Physics has progressed for centuries in the face of numerous inconsistencies including the ongoing decades-long inconsistency between its two most fundamental theories (general relativity and quantum mechanics). • Decision makers commonly ask for the case against as well as the case for proposed findings and action plans in corporations, governments, and judicial systems.

Inconsistency robustness stands to become a more central theme for computation. The basic argument is that because inconsistency is continually i Turing was correct that it is unsafe to use first-order logic to reason about inconsistent information. Church later first proved that determining whether there are hidden inconsistencies in a practical mathematical theory is computationally undecidable. ii Inconsistency robustness builds on previous work on inconsistency tolerance, e.g., [Bertossi, Hunter and Schaub 2004;Gabbay andHunter 1991-1992;[START_REF] Bėziau | Handbook of Paraconsistency College Publications Kings College London[END_REF].

pervasive in large information systems, the issue of inconsistency robustness must be addressed!

Information Abstraction

Large

Small

Low High

First-Order Logic

Correlations

("deep learning" )

Big Theory

The above diagram illustrates the following:

 Big Theory is powerful enough to subsume and incorporate both correlations (including "Deep Learning") and First-Order Logic. Active research is underway to demonstrate the power of combining statistical reasoning (including "Deep Learning") with inconsistency-robust logic[Hewitt 2015d]. Big Theory information is perpetually and pervasively inconsistent [Law 2004;[START_REF] Mol | Principles and Practices of Medicine: the Coexistence of various Anaemias[END_REF]"Sun Tzu" ~500BC;von Clausewitz 1832]. Attempting to resolve ambiguities typically results in greater inconsistency because there are more ways for contradictions to occur.  First-Order Logic is limited in its ability to deal with high level abstractions because of limited expressivity. Also, First-Order Logic is limited in the amount of information that can be addressed because a First-Order theory must be known to be consistent lest it draw invalid conclusions from (hidden) inconsistencies.  Correlation (using "Deep Learning" multi-layer weighted-summing-tothreshold nets) is restricted in its abstraction capabilities because abstractions are constrained to being states of configurations of hidden nodes, which are not explicitly represented and consequently cannot be used explicitly in the construction of higher-level abstractions.

Correlation does not do well with small amounts of information because correlations are not statistically significant thereby making learning unreliable.

On the other hand for large enough datasets, there are many spurious correlations [Hewitt 2015d]. Also, large information sets from the Internet contain extraneous information that can confound whatever particular thing that a "Deep Learning" system may be attempting to discriminate.

Furthermore, in large information systems, there are typically several ways to calculate probability for higher-level abstractions. Often the result is that the probability is both close to 0% and close to 100%![Hewitt 2016d] Most published statistically significant research findings are false [Ioannidis 2005].

"Deep Learning" has some fundamental limitations including the following:

 It can't do one-time learning in which learning takes place from a singleinstance experience because there is no corpus on which to train the weights.  "Deep learning" abstractions using levels is limited because abstractions at a given level are limited to being represented as a vector of numbers.  Abstractions cannot be modularly invoked and joined with other abstractions  "Deep learning" can be slow. For example, it can require learning exponentially many parameters in in the size of an input feature set, which can require exponential time if many outputs are dependent on numerous overlapping sets of input features.

"Big data" doesn't automatically solve the problems of "Deep Learning" because of fat tail distributions with coincidences of rare exigencies.

Computer-only-driven cars present an enormous challenge for "Deep Learning" because it is likely that there is a fat-tail distribution of circumstances that can lead to fatalities including humans gestures and speech from car occupants, external pedestrians, and law enforcement officers. Although individual circumstances can be learned, coincidences of some exigencies will be extremely rare and so will not be learned. Some of these coincidences can lead to fatalities. Consequently, even hundreds of millions of miles of experience training a "Deep Learning" network for computer-only-driven cars may not be sufficient to allow their general use anytime soon because of public very low tolerance for computer-caused fatalities. Fortunately, the prospective advent of driver-computer-assisted cars will provide experience to develop new architectures that eventually can make it possible to legalize general use of computer-only-driven cars.

The "The Art of War" is a classic treatise. For example, it has maxims such as the following:

Appear weak when you are strong, and strong when you are weak.

When ⊢ (assertion)

Strong[x:Army] → ⊩ (set goal) Appear[Weak[x]] When ⊢ Weak[x:Army] → ⊩ Appear[Strong[x]]
There is no instance of a nation benefitting from prolonged warfare.

When ⊢ ProlongedWarfare[i:Instance, n:Nation] → ⊢

(assert)

NoBenefit[to ⌸ n, from ⌸ i]

Some of the maxims have potential inconsistencies such as the following:

The greatest victory is that which requires no attack.

When ⊩(goal) VictoryOver[anOpponent:Army]→ ⊩ ¬Attack[anOpponent]

Attack when the opponent is weak.

When ⊢ Weak[anOpponent:Army]→ ⊩ Attack[anOpponent]
The above can formalized in first-order logic as follows:

Opponent[RedArmy] Weak[RedArmy] VictoryOver[RedArmy] VictoryOver[x] ⇒ ¬Attack[x] Weak[x] ⇒ Attack[x]
However, first-order logic entails the following contradiction: ¬Weak[RedArmy]

First-order logic is safe only for theories for which there is strong evidence of consistency.

So what are practical uses of the "The Art of War"? Attempting to remove all potential inconsistency will leave almost nothing left.

Inconsistency robust theories can be easier to develop than first-order theories because impossibility of inconsistency is not required. In case of inconsistency, there will be some propositions that can be both proved and disproved, i.e., there will be arguments both for and against the propositions.

In the early days, an attempt was made to construct independent consistent islands of information. It did not work out well because:

• There is no practical way to determine if an island of practical information is consistent. • As an island of practical information becomes larger, it invariably develops inconsistencies. • There are pervasive ineradicable inconsistencies in attempting to relate information in different islands.

Inconsistency robustness facilitates formalization

"A little inaccuracy sometimes saves tons of explanation." Saki in "The Square Egg"

Inconsistency Robust Direct logic facilitates common sense reasoning by formalizing inconsistency robust inference. 13 For example, the "The Art of War" can be formalized as follows:

Weak[RedArmy] VictoryOver[RedArmy] VictoryOver[x] ⊢ ¬Attack[anOpponent] Weak[x] ⊢ Attack[x]
However, Direct Logic does not infer the following contradiction because the contrapositive does not hold for ⊢:

¬Weak[RedArmy]
It turns out that the following can be inferred:

Attack[RedArmy] Attack[RedArmy]
However, instead of being able to infer everything i , once the above contradiction been noticed, question answering can be improved using the "but" construct of Inconsistency Robust Direct Logic as follows:

Attack[RedArmy] but Attack[RedArmy]  Attack[RedArmy] but Attack[RedArmy]]

Contradictions can facilitate Argumentation

"contradictions are not always an entirely bad thing. I think we have all found in our googling that it is often better to find contradictory information on a search topic rather than finding no information at all. I explore some of the various reasons this may arise, which include finding that there is at least active interest in the topic, appraising the credentials of the informants, counting their relative number, assessing their arguments, trying to reproduce their experimental results, discovering their authoritative sources, etc." 14

Using Direct Logic, various arguments can be made in Art of War. For example:

VictoryOver[x]├ Argument1 𝐴𝑟𝑡𝑂𝑓𝑊𝑎𝑟 Attack[x]
i.e. "The greatest victory is that which requires no attack."

Opponent[x], Weak[x]├ Argument2 𝐴𝑟𝑡𝑂𝑓𝑊𝑎𝑟 Attack[x]
i.e. "Attack an opponent when they are weak." However, neither of the above arguments is absolute because there might be arguments against the above arguments.

The theory ArtOfWar illustrates the following points:  Inconsistency robustness facilitates theory development because a single inconsistency is not disastrous.  Even though the theory ArtOfWar is inconsistent, it is not meaningless.  Queries can be given sensible answers in the presence of inconsistent information.

Inconsistency Robustness for Statistical Information

"You can use all the quantitative data you can get, but you still have to distrust it and use your own intelligence and judgment." Alvin Toffler Medical studies can be complex. Consider a team that studying PTSD in a population. Using the same data, the team develops two methodologies for i which is the case in first-order logic from a contradiction counting those in the population with PTSD. Under one methodology, 45% of them have PTSD and under other methodology, it is 55%. The two methodologies use slightly different hypotheses, theories, interpretations, and calculation methods on the same data. The proponents of each methodology think that their preferred methodology is greatly superior to the other. Also, the difference in outcomes (55% versus 45%) is highly significant by the standard statistical criteria. The teams agree that PTSD is complex and not completely understood. Both methodologies are reasonable and involve different trade-offs. Together the two methodologies produce greater understanding their either one individually. The study report acknowledged the inconsistency, explained how it was processed, and explored the impact to users of the report.

The researchers freely admit that the results of the two methodologies are statistically significantly inconsistent, i.e., 45% versus 55%. Also, there are numerous inconsistencies internal to each methodology. i But researchers have to deal with such inconsistencies all the time and try to make sure that results are as robust as possible in spite of these inconsistencies. Hopefully, such inconsistency robustness will become more common with increased sharing of medical data. 15

IGOR ii for Probabilistic Inference

Probabilistic iii reasoning can make incorrect inferences using inconsistent information. For example, most published statistically significant research findings are false [Ioannnidis 2005a]. iv "The rate of findings that have later been found to be wrong or exaggerated has been found to be 30 percent for the top most widely cited randomized, controlled trials in the world's highest-quality medical journals. For nonrandomized trials that number rises to an astonishing five out of six." 16 i Of course, the medical science of PTSD will continue to develop. See section in this article on "Circular Information." ii Inconsistency in Garbage Out Redux.

iii Probabilities are for propositions. Sometimes these proposition are about events, past and/or future. iv "Scientific investigation is the noblest pursuit," Ioannidis writes. "I think we can improve the respect of the public for researchers by showing how difficult success is." [START_REF] Ioannidis | Why Most Published Research Findings Are False: Author's Reply to Goodman and Greenland[END_REF] Any of the following can make it more risky that a medical study is false: As illustrated below, probabilistic inference can be inconsistency non-robust in ways even beyond the inconsistency non-robustness of first-order logic.

Probability discrepancy widening. .45≲ℙ≲.55├ .05≲ℙ≲.95

i.e., If the probability of some proposition is somewhat inconsistent (which can be deeply hidden), then using probabilistic inference, the proposition is both highly probable and highly improbable. Proof: .35≲ℙ≲.65 // using 5), 3), 2) and 1) 7)

.05≲ℙ≲.95 // using 6), 5), 3), and 2)

Clearly, the laws probability are not very inconsistency robust because (as shown above) in a few of steps they can do enormous damage given that a probability is in the range 45% to 55%. Developing inconsistency robust statistical reasoning is a highly-relevant challenge for future work.

Proposition probability instability. If Inconsistent[T], then ℙ|T is unstable

i.e., If a theory is inconsistent, then using probabilistic inference, the conditional probability of every proposition given the theory is unstable.

Proof:

1) Inconsistent[T]

// hypothesis 2) ℙT ≅ 0 // using 1)

3) ℙT ≦ ℙT // using probability 4) ℙT ≅ 0 // using 3) and 2) 5) ℙ|T = ℙT ℙT // using probability 6) ℙ|T is unstable // using 5) with 4) and 2) // the ratio of two tiny numbers // that can be difficult to estimate i i Of course in the following special cases: Theory probability instability. If  is inferentially inconsistent for T, then ℙT| is unstable. i i.e., Using probabilistic inference, the conditional probability of a theory with respect to every inconsistency is unstable. Proof:

 If ├ T, then ℙ|T = 1  If ├ T , then ℙ|T = 0  If ├ T ,
1) ├ T  // hypothesis 2) ├ T  // using 1)
3) ℙT = ℙ // using 2) 4) ℙT| = ℙT ℙ // using probability 5) ℙT| ≅ 1 // using 3) and 4) 6) ├ T  // using 1) 7) ℙT = 0 // using 6) 8) ℙT| ≅ 0 // using 4) and 7) 9) ℙT| is unstable // using 5) and 8)

Theory probability based on predictions. If ├ T, then ℙT≅ℙ.

i.e., The probability of a theory is that of any proposition that it infers Proof:

1) ├ T  // hypothesis 2) ℙ|T ≅ 1 // using 1)
3) ℙT = ℙ // using 1) 4) ℙ|T = ℙT ℙT // using probability 5) ℙT ≅ ℙ // using 2) and 3)

Of course, the above issues can be multiplicative and feed into one another. i Note that ℙT| is unstable regardless of whether or not it is known that  is an inferential inconsistency of T. Typically in practice, it cannot be known if  is an inferential inconsistency of T, i.e., it cannot be known if T infers evidence against  as well as evidence in favor of .

Probabilistic inference (like first-order logic) can be safely used only for consistent information.

Limitation of Probabilistic Inference

In addition to inconsistency non-robustness, probabilistic inference is limited by the following:  Limited expressiveness (avoidance of non-numerical reasoning i )  Limited scalability  Fragile independence assumptions  Markovian ahistoricity  Bayes rule (very conservative) versus general reasoning Nevertheless, probabilities have important uses in physics, e.g. quantum dynamics.

According to [Campbell, et. al. 2016]: ii "As the use of deep neural network systems spreads into everyday life they are already used to analyze and recommend financial transactionsit raises an interesting concept for humans and their relationships with machines. The machine becomes an oracle; its pronouncements have to be believed.

When a conventional computer tells an engineer to place a rivet or a weld in a specific place on an aircraft wing, the engineerif he or she wishes -can lift the machine's lid and examine the assumptions and calculations inside. That is why the rest of us are happy to fly. Intuitive machines will need more than trust: they will demand faith."

The above opinion is deeply flawed both scientifically and ethically.

Furthermore, "faith" as described by [Campbell, et. al. 2016 Correlations derived using the above techniques can help boost information system performance provided that they are incorporated into inconsistency robust systems to limit correlational deficiencies.

Circular information

How can inconsistencies such as the ones above be understood? Assigning truth values to propositions is an attempt to characterize whether or not a proposition holds in a theory. Of course, this cannot be done consistently if the theory is inconsistent. Likewise, assigning probabilities to propositions is an attempt to characterize the likelihood that a proposition holds in a theory. Similar to assigning truth values, assigning probabilities cannot be done consistently if the theory is inconsistent.

The process of theory development can generate circularities that are an underlying source of inconsistency: "Mol shows that clinical diagnoses often depend on collective and statistically generated norms. What counts as a 'normal' haemoglobin level in blood is a function of measurements of a whole population. She is saying, then, that individual diagnoses include collective norms though they cannot be reduced to these [START_REF] Mol | Principles and Practices of Medicine: the Coexistence of various Anaemias[END_REF]. At the same time, however, the collective norms depend on a sample of clinical measurements which may be influenced by assumptions about the distribution of anaemia-though it is not, of course, reducible to any individual measurement. The lesson is that the individual is included in the collective, and the collective is included in the individual-but neither is reducible to the other." 19

First-order logic is unsafe for use with potentially inconsistent information

"Irony is about contradictions that do not resolve into larger wholes even dialectically, about the tension of holding incompatible things together because all are necessary and true." Haraway [1991] An important limitation of first-order logic 20 for inconsistent information is that it supports the principle that from an inconsistency anything and everything can be inferred, e.g. "The moon is made of green cheese."

For convenience, I have given the above principle the name IGOR 21 for Inconsistency in Garbage Out Redux. IGOR can be formalized as follows in which a contradiction about a proposition Ω infers any proposition , 22 i.e., Ω, ¬ Ω├ .

Of course, IGOR cannot be part of Inconsistency Robust Direct Logic because it allows every proposition to be inferred from a contradiction.

The IGOR principle of first-order logic may not seem very intuitive! So why is it included?

 Proof by Contradiction: (├ , ) ⇒ (├ ), on the grounds that if  infers a contradiction in a consistent theory then  must hold. In an inconsistent theory, Proof by Contradiction leads to explosion by the following derivation by a which a contradiction about P infers any proposition :

P ¬P ├ ¬ ├ P ¬P ├ () ├   Contrapositive for Inference: (├ ) ⇒ (├ )
, on the grounds that if ├ , then if  holds, then  must hold. In an inconsistent theory, Contrapositive for Inference leads to explosion by the following derivation by a which a contradiction about P (i.e.,├ PP ) infers any proposition  by the following derivation:

Since ├P├P by monotonicity. Therefore P├ by Contrapositive for Inference. Consequently PP├ .  Extraneous  Introduction: 23 Ψ├ (ΨΦ), on the ground that that if Ψ holds, then ΨΦ holds regardless of whether Φ holds. 24 In an inconsistent theory, Extraneous  introduction leads to explosion via the following derivation in which a contraction about P infers any proposition :

P¬P ├ (P)¬P ├   Excluded Middle: ├ (ΨΨ) is the principle that for every proposition  the following holds: ExcludedMiddle[] ≡ . However, Excluded Middle is not suitable for inconsistency-robust logic because it is equivalent 25 to saying that there are no inconsistencies, i.e., for every proposition , ), which means that the principle of Excluded Middle implies ΨΨΦ for all propositions Ψ and Φ. Thus the principle of Excluded Middle is not inconsistency robust because it implies every proposition Φ can be proved i given any contradiction Ψ. [START_REF] Kao | Proof by self-refutation and excluded middle lead to explosion[END_REF] i using -Elimination , i.e., ¬Φ, (ΦΨ)├ T Ψ First-Order Logic is unsafe for inference using potentially inconsistent information. 26

Noncontradiction[] ≡ () Using propositional equivalences, note that ExcludedMiddle[ΦΨ] ⇔ (ΨΨΦ)(ΦΦΨ) Consequently, ExcludedMiddle[ΦΨ]⇒(ΨΨΦ

Direct Logic

"But if the general truths of Logic are of such a nature that when presented to the mind they at once command assent, wherein consists the difficulty of constructing the Science of Logic?" [Boole, 1853 pg. 3] Direct Logic 27 is a framework: propositions have arguments for and against.

Inference rules provide arguments that let you infer more propositions. Direct Logic is just a bookkeeping system that helps you keep track. It doesn't tell you what to do when an inconsistency is derived. But it does have the great virtue that it doesn't make the mistakes of first-order logic when reasoning about inconsistent information.

The semantics of Direct Logic are based on argumentation. Arguments can be inferred for and against propositions. Furthermore, additional arguments can be inferred for and against these arguments, e.g., supporting and counter arguments. 28 Direct Logic must meet the following challenges:  Consistent to avoid security holes  Powerful so that computer systems can carry formalize all logical inferences  Principled so that it can be easily learned by software engineers  Coherent so that it hangs together without a lot of edge cases  Intuitive so that humans can follow computer system reasoning  Comprehensive to accommodate all forms of logical argumentation  Inconsistency Robust to be applicable to pervasively inconsistent theories of practice with o Inconsistency Robust Direct Logic for logical inference about inconsistent information o Classical Direct Logic for mathematics used in inconsistencyrobust theories

Inconsistency Robust Direct Logic is for reasoning about pervasivelyinconsistent large software systems with the following goals:  Provide a foundation for reasoning about the mutually inconsistent implementation, specifications, and use cases for large software systems.  Formalize a notion of "direct" inference for reasoning about inconsistent information  Support "natural" deduction [START_REF] Jaśkowski | On the Rules of Suppositions in Formal Logic[END_REF]] i inference rules ii  Support the usual propositional equivalences iii  -Elimination , i.e., ¬Φ, (ΦΨ)├ T Ψ  Reasoning by disjunctive cases, i.e., (), (├ T ), (├ T Ω)├ T Ω  Inconsistency Robust Derivation by Contradiction, i.e., (Ψ⇒ T (¬ΦΦ)) ├ T ¬Ψ  Support abstraction among code, documentation, and use cases of large software systems. (See discussion below.)  Provide increased safety in reasoning using inconsistent information. iv Consequently, Inconsistency Robust Direct Logic is well suited in practice for reasoning about large software systems. v

Adding just Classical Proof by Contradiction to Inconsistency Robust Direct Logic transforms it into a Classical Direct Logic.

The theories of Direct Logic are "open" in the sense of open-ended schematic axiomatic systems [Feferman 2007b]. The language of a theory can include any vocabulary in which its axioms may be applied, i.e., it is not restricted to a specific vocabulary fixed in advance (or at any other time). Indeed a theory can be an open system that can receive new information at any time [Hewitt 1991, Cellucci 1992].

i See discussion in [Pelletier 1999].

ii with the exception of the following:

 Classical Proof by Contradiction i.e., (Ψ├ T ¬Φ,Φ)├ T ¬Ψ  Extraneous  Introduction, i.e., Ψ├ T (ΦΨ)  Excluded Middle, i.e., ├ T (Φ¬Φ)
iii with exception of absorption, which must be restricted to avoid IGOR iv by comparison with first-order logic v In this respect, Direct Logic differs from previous inconsistency tolerant logics, which had inference rules that made them intractable for use with large software systems.

In the argumentation lies the knowledge "You don't understand anything until you learn it more than one way." [Minsky 2005] 29 Partly in reaction to Popper i , Lakatos [1967, §2]) calls the view below Euclidean: 30 "Classical epistemology has for two thousand years modeled its ideal of a theory, whether scientific or mathematical, on its conception of Euclidean geometry. The ideal theory is a deductive system with an indubitable truthinjection at the top (a finite conjunction of axioms)-so that truth, flowing down from the top through the safe truth-preserving channels of valid inferences, inundates the whole system."

Since truth is out the window for inconsistent theories, we need a reformulation in terms of argumentation.

Direct Argumentation

Inference in a theory T (├ T ) carries arguments from antecedents to consequents.

Direct Argumentation means that ├ T in a proposition actually means inference in the theory T. As stated, there is no inconsistency in either the theory Africans or the theory Portuguese. But there is an inconsistency in the join of these theories, namely, Africans+Portuguese.

In general, the theories of Inconsistency Robust Direct Logic are inconsistent and therefore propositions cannot be consistently labeled with truth values.

Information Invariance

"Become a student of change. It is the only thing that will remain constant." 32

Invariance vi is a fundamental technical goal of Direct Logic.

Invariance: Principles of Direct Logic are invariant as follows:

1. Soundness of inference: information is not increased by inference 2. Completeness of inference: all information that necessarily holds can be inferred

i ├ Africans Divine[idols] ii ├ Africans Fabricated[idols] iii ├ Portuguese (Fabricated[idols]  Divine[idols])
iv in Africans+Portuguese v in Africans vi Closely related to conservation laws in physics

Semantics of Direct Logic

The semantics of Direct Logic is the semantics of argumentation. Arguments can be made in favor of against propositions. And, in turn, arguments can be made in favor and against arguments. The notation├ A T  is used to express that A is an argument for  in T.

The semantics of Direct Logic are grounded in the principle that every proposition that holds in a theory must have argument in its favor which can be expressed as follows:

The principle Inferences have Arguments says that ├ T if and only if there is an argument A for  in T, i.e., ├ A T

 i

For example, there is a controversy in biochemistry as to whether or not it has been shown that arsenic can support life with published arguments by Redfield 33 and NASA 34 to the following effect:

├ Redfield 𝐵𝑖𝑜𝑐ℎ𝑒𝑚𝑖𝑠𝑡𝑟𝑦 (⊬ NASA 𝐵𝑖𝑜𝑐ℎ𝑒𝑚𝑖𝑠𝑡𝑟𝑦 SupportsLife[Arsenic]
) [START_REF] Rovelli | The Uselessness of Certainty[END_REF]] has commented on this general situation:

"There is a widely used notion that does plenty of damage: the notion of 'scientifically proven.' Nearly an oxymoron. The very foundation of science is to keep the door open to doubt. Precisely because we keep questioning everything, especially our own premises, we are always ready to improve our knowledge. Therefore a good scientist is never 'certain.' Lack of certainty is precisely what makes conclusions more reliable than the conclusions of those who are certain: because the good scientist will be ready to shift to a different point of view if better elements of evidence, or novel arguments emerge. Therefore certainty is not only something of no use, but is in fact damaging, if we value reliability."

i There is a computational decision deterministic procedure CheckerT running in linear time such that:

∀[a:Argument, s:Sentence]→ CheckerT [a, s]=True ⇔ ├ a T s T)
A fanciful example of argumentation comes from the famous story "What the Tortoise Said to Achilles" [Carroll 1895].

Applied to example of the Tortoise in the story, we have

Axiom1 ≡ ├ A, B Axiom2 ≡ A, B ├ Z
The above proposition fulfills the demand of the Tortoise that Whatever Logic is good enough to tell me is worth writing down.

Inference in Argumentation

"Scientist and engineers speak in the name of new allies that they have shaped and enrolled; representatives among other representatives, they add these unexpected resources to tip the balance of force in their favor." Latour [1987] Second Principle "├ Elimination" (transitivity) is a fundamental principle of inference: 36

├ Elimination: , (├ T ) ├ T  //  inferred in T from ├ T  and ├ T 
SubArguments is another fundamental principle of inference:

├ Introduction (SubArguments): (├ T Ψ ) ⇔ (├ T ) // In T,  infers  when  is inferred in TΨ
Consequently, the following theorems hold which are the basis of Gentzen/Hilbert-style deduction systems and the Curry-Howard correspondence [Curry 1934, Howard 1969]:

Please see the appendix on Direct Logic for more information.

Contraction: ├ T (├ T ) Extended Contraction: (├ T (├ T ))├ T ((├ T )├ T (├ T ))

Mathematics Self Proves that it is Open

Mathematics proves that it is open in the sense that it can prove that its proofs cannot be provably computationally enumerated: 37

Theorem ⊢Mathematics is Open, i.e., ⊢ProofsComputationalyEnumerable Proof. i Suppose to obtain a contradiction that it is possible to prove closure, i.e., ⊢ProofsComputationalyEnumerable. Then there is a provably computable total procedure ProofsEnumerator:

[ℕ]↦Proof such that it is provable that ∀[p:Proof]→ ∃[i:ℕ]→ProofsEnumerator∎[i]= p ∀[i:ℕ]→ProofsEnumerator∎[i]:Proof
A subset of the proofs are those proving that certain procedures [ℕ]↦ℕ are total. Consequently, there is a ProvedTotalsEnumerator:[ℕ]↦([ℕ]↦ℕ) that enumerates the provably total computable procedures [ℕ]↦ℕ that can be used in the implementation of the following procedure:

Diagonal∎[i:ℕ]:ℕ ≡ 1+ (ProvedTotalsEnumerator∎[i]) ∎[i] Consequently:
• Diagonal is a proved total procedure because it is implemented using computable proved total procedures. • Diagonal is not a proved total procedure because it differs from every other computable proved total procedure. The above contradiction completes the proof.

[Franzén 2004] argued that mathematics is inexhaustible because of inferential undecidability ii of mathematical theories. The above theorem that mathematics is open provides another independent argument for the inexhaustibility of mathematics.

Contributions of Direct Logic

Direct Logic aims to be a minimal fix to first-order logic to meet the needs of information coordination by making the following contributions over previous work:

• Direct Inference 38 The Actor Model differs from its predecessors and most current models of computation in that the Actor model assumes the following:  Concurrent execution in processing a message.  The following are not required by an Actor: a thread, a mailbox, a message queue, its own operating system process, etc.  Message passing has the same overhead as looping and procedure calling.

i Likewise the messages sent can contain addresses only 1. that were provided when the Actor was created 2. that have been received in messagesthat are for Actors created here ii An exclusive Actor can perform at most one activity at a time.

iii An Actor that will never update its local storage can be freely replicated and cached.

Configurations versus Global State Spaces

Computations are represented differently in Turing Machines and Actors:

• That Actors which behave like mathematical functions exactly correspond with those definable in the lambda calculus provides an intuitive justification for the rules of the lambda calculus:  Lambda identifiers: each identifier is bound to the address of an Actor.

The rules for free and bound identifiers correspond to the Actor rules for addresses.  Beta reduction: each beta reduction corresponds to an Actor receiving a message. Instead of performing substitution, an Actor receives addresses of its arguments.

The lambda calculus can be implemented in ActorScript as follows:

Actor  The definition is modular in that each lambda calculus programming language construct is an Actor.  The definition is easily extensible since it is easy to add additional programming language constructs.  The definition is easily operationalized into efficient concurrent implementations.  The definition easily fits into more general concurrent computational frameworks for many-core and distributed computation.

However, there are nondeterministic computable functions on integers that cannot be implemented using the nondeterministic lambda calculus. Furthermore, the lambda calculus can be very inefficient as illustrate by the theorem below:

Theorem: In systems of practice i , simulating an Actor system using a the parallel lambda calculus (i.e. using purely functional programming) can be exponentially slower.

i Examples include climate models and medical diagnosis and treatment systems for cancer. A software system of practice typically has tens of millions of lines of code.

The lambda calculus can express parallelism but not general concurrency (see discussion below).

Actors generalize Turing Machines

Actor systems can perform computations that are impossible by Turing Machines as illustrated by the following example:

There is a bound on the size of integer that can be computed by an always halting nondeterministic Turing Machine starting on a blank tape. 44 Plotkin [1976] gave an informal derivation as follows: 45 "Now the set of initial segments of execution sequences of a given nondeterministic program P, starting from a given state, will form a tree.

The branching points will correspond to the choice points in the program.

Since there are always only finitely many alternatives at each choice point, the branching factor of the tree is always finite. 46 That is, the tree is finitary. Now König's lemma says that if every branch of a finitary tree is finite, then so is the tree itself. In the present case this means that if every execution sequence of P terminates, then there are only finitely many execution sequences. So if an output set of P is infinite, it must contain a nonterminating computation." 47 By contrast, the following Actor system can compute an integer of unbounded size:

The above Actor system can be implemented as follows using ActorScript™: Theorem. There are nondeterministic computable functions on integers that cannot be implemented by a nondeterministic Turing Machine. Derivation. The above Actor system implements a nondeterministic function i that cannot be implemented by a nondeterministic Turing machine.

The following arguments support unbounded nondeterminism in the Actor model [Hewitt 1985[Hewitt , 2006]:  There is no bound that can be placed on how long it takes a computational circuit called an arbiter to settle. Arbiters are used in computers to deal with the circumstance that computer clocks operate asynchronously with input from outside, e.g., keyboard input, disk access, network input, etc. So it could take an unbounded time for a message sent to a computer to be received and in the meantime the computer could traverse an unbounded number of states.  Electronic mail enables unbounded nondeterminism since mail can be stored on servers indefinitely before being delivered.



Communication links to servers on the Internet can be out of service indefinitely.

Reception order indeterminacy

Hewitt and Agha [1991] and other published work argued that mathematical models of concurrency did not determine particular concurrent computations as follows: The Actor Model ii makes use of arbitration for implementing the order in which Actors process message. Since these orders are in general indeterminate, they cannot be deduced from prior information by mathematical logic alone. Therefore mathematical logic cannot implement concurrent computation in open systems.

In concrete terms for Actor systems, typically we cannot observe the details by which the order in which an Actor processes messages has been determined. Attempting to do so affects the results. Instead of observing the internals of arbitration processes of Actor computations, we await outcomes. 48 Indeterminacy in arbiters produces indeterminacy in Actors. The reason that we await outcomes is that we have no realistic alternative.

Actor Physics

The Actor model makes use of two fundamental orders on events [Baker and Hewitt 1977;Clinger 1981, Hewitt 2006]:

1. The activation order (⇝) is a fundamental order that models one event activating another (there is energy flow from an event to an event which it activates). The activation order is discrete:

∀[e1,e2Events]→ Finite[{eEvents | e1 ⇝e ⇝e2}]
There are two kinds of events involved in the activation order: reception and transmission. Reception events can activate transmission events and transmission events can activate reception events. 2. The reception order of an exclusive Actor x ( 𝐱 ⇒) models the (total) order of events in which a message is received at x. The reception order of each x is discrete:

∀[r1,r2ReceptionEventsx]→ Finite[{rReceptionEventsx | r1 𝐱 ⇒ r 𝐱 ⇒ r2}]
The combined order (denoted by ↷) is defined to be the transitive closure of the activation order and the reception orders of all Actors. So the following question arose in the early history of the Actor model: "Is the combined order discrete?" Discreteness of the combined order captures an important intuition about computation because it rules out counterintuitive computations in which an infinite number of computational events occur between two events (à la Zeno).

Hewitt conjectured that the discreteness of the activation order together with the discreteness of all reception orders implies that the combined order is discrete. Surprisingly [Clinger 1981;later generalized in Hewitt 2006] answered the question in the negative by giving a counterexample.

The counterexample is remarkable in that it violates the compactness theorem for 1 st order logic:

Any finite set of propositions is consistent (the activation order and all reception orders are discrete) and represents a potentially physically realizable situation. But there is an infinite set of propositions that is inconsistent with the discreteness of the combined order and does not represent a physically realizable situation. The counterexample is not a problem for Direct Logic because the compactness theorem does not hold.

The resolution of the problem is to take discreteness of the combined order as an axiom of the Actor model:

i ∀[e1,e2Events]→ Finite[{eEvents | e1↷e ↷e2}]
Computational Representation Theorem "a philosophical shift in which knowledge is no longer treated primarily as referential, as a set of statements about reality, but as a practice that interferes with other practices. It therefore participates in reality." Annemarie [START_REF] Mol | Principles and Practices of Medicine: the Coexistence of various Anaemias[END_REF] What does the mathematical theory of Actors have to say about the relationship between logic and computation? A closed system is defined to be one which does not communicate with the outside. Actor model theory provides the means to characterize all the possible computations of a closed system in terms of the Computational Representation Theorem [Clinger 1982;Hewitt 2006]: 50 The denotation DenoteS of a closed system S represents all the possible behaviors of S as DenoteS = limit i→∞ Progression S i where ProgressionS takes a set of partial behaviors to their next stage, i.e., ProgressionS i ⇾ ProgressionS i+1 where ⇾ means "can evolve to." In this way, S can be mathematically characterized in terms of all its possible behaviors (including those involving unbounded nondeterminism). ii The denotations form the basis of constructively checking programs against all their possible executions. iii i The above laws for Actor systems should be derivable from the laws of physics. ii There are no messages in transit in DenoteS iii a restricted form of this can be done via Model Checking in which the properties checked are limited to those that can be expressed in Linear-time Temporal Logic [Clarke, Emerson, Sifakis, etc. ACM 2007 Turing Award]

A consequence of the Computational Representation system is that there are uncountably many different Actors.

For example, CreateReal∎[ ] can produce any real number i between 0 and 1 where

CreateReal∎[ ] ≡ [(0 either 1), ⩛Postpone CreateReal∎[ ]]
where

• CreateReal∎[ ] is the result of sending the actor CreateReal the message [ ] • (0 either 1) is the nondeterministic choice of 0 or 1 ] is the sequence that begins with first and whose remainder is rest • Postpone expression delays execution of expression until the value is needed. The upshot is that concurrent systems can be represented and characterized by logical deduction but cannot be implemented.

• [first, ⩛rest

Thus, the following problem arose:

How can programming languages be rigorously defined since the proposal by [START_REF] Scott | Toward a mathematical semantics for computer languages Oxford Programming Research Group Technical Monograph[END_REF] to define them in terms lambda calculus failed because the lambda calculus cannot implement concurrency?

One solution is to develop a concurrent interpreter using eval messages in which eval[anEnvironment] is a message that can be sent to an expression to cause it be evaluated using the environment anEnvironment. Using such messages, modular meta-circular definitions can be concisely expressed in the Actor model for universal concurrent programming languages [Hewitt 2010a].

Computation is not subsumed by logical deduction

The gauntlet was officially thrown in The Challenge of Open Systems [Hewitt 1985] to which [START_REF] Kowalski | Logic-based Open Systems" Representation and Reasoning[END_REF]] replied in Logic-Based Open Systems.

[Hewitt and Agha 1988] followed up in the context of the Japanese Fifth Generation Project.

Kowalski claims that "computation could be subsumed by deduction" i His claim has been valuable in that it has motivated further research to characterize exactly which computations could be performed by Logic Programs. However, contrary to Kowalski, computation In this way, we have proved that the Procedural Embedding of Knowledge paradigm is strictly more general than the Logic Program paradigm.

Computational Undecidability

Some questions cannot be uniformly answered computationally.

The halting problem is to computationally decide whether a program halts on a given input i i.e., there is a total deterministic procedure Halt such that the following 3 properties hold for any program p and input x:

1. Halt∎[p, x] ⇾1 True ⇔ Converges[ ( p∎[x])] 2. Halt∎[p, x] ⇾1 False ⇔  Converges[( p∎[x])] 3.

Mathematics self proves its own consistency (contra Gödel et. al.)

The following rules are fundamental to mathematics:  Derivation by Contradiction, i.e. (¬Φ⇒(Θ¬Θ))├ Φ, which says that a proposition can be proved showing that its negation implies a contradiction.  A theorem can be used in a proof, i.e. (├ Φ)⇒Φ Theorem: 53 Mathematics self proves its own consistency.

Formal Derivation. By definition, if mathematics is not consistent then there is some mathematical proposition Ψ such that ├(Ψ¬Ψ). By the rule of Existential Elimination, there is some proposition Ψ0 such that ¬Consistent⇒├ (Ψ0 ¬Ψ0) which by transitivity of implication means ¬Consistent⇒(Ψ0 ¬Ψ0). Substituting for Φ and Θ, in the rule for Derivation by Contradiction, we have (¬Consistent⇒(Ψ0 ¬Ψ0))├ Consistent. Thus,├ Consistent.

i Adapted from [Church 1936]. Normal forms were discovered for the lambda calculus, which is the way that they "halt." [Church 1936] proved the halting problem computationally undecidable. Having done considerable work, Turing was disappointed to learn of Church's publication. The month after Church's article was published, [START_REF] Turing | On computable numbers, with an application to the Entscheidungsproblem[END_REF]] was hurriedly submitted for publication. ii The fact that the halting problem is computationally undecidable does not mean that proving that programs halt cannot be done in practice [Cook, Podelski, and Rybalchenko 2006]. 3)├(Ψ 0 Ψ 0 ) // rule of Existential Elimination using 2) 4) Ψ 0 Ψ 0 // rule of Soundness using 3)

Natural Deduction i Derivation of Consistency of Mathematics

Please note the following points:  The above argument formally mathematically proves that mathematics is consistent and that it is not a premise of the theorem that mathematics is consistent. 54  Mathematics was designed for consistent axioms and consequently the rules of mathematics can be used to prove consistency regardless of other axioms. 55 The above derivation means that "Mathematics is consistent" is a theorem in Classical Direct Logic. This means that the usefulness of Classical Direct Logic depends crucially on the consistency of Mathematics. Good evidence for the consistency of Mathematics comes from the way that Classical Direct Logic avoids the known paradoxes. 56 Humans have spent millennia devising paradoxes.

The above recently developed self-proof of consistency shows that the current common understanding that Gödel proved "Mathematics cannot prove its own consistency, if it is consistent" is inaccurate.

Long ago, Wittgenstein showed that contradiction in mathematics results from the proposition I'm unprovable. that Gödel used in his derivation. However, using strong typing for mathematical propositions, it can be proved that Gödel's sentence cannot be constructed because required Y fixed point is not valid. In this way, consistency of mathematics is preserved without giving up power.

Foundations with strong parameterized types

"Everyone is free to elaborate [their] own foundations. All that is required of [a] Foundation of Mathematics is that its discussion embody absolute rigor, transparency, philosophical coherence, and addresses fundamental methodological issues." 57 Direct Logic develops foundations for mathematics by deriving sets from types and categorical axioms for the natural numbers and ordinals. 58

Proof by Induction

The closed mathematical theory Nat categorically axiomatises with the induction axiom that for each order:ℕ+ and P:Propositionorder ℕ , the following holds:

(P⟦0⟧  ∀[i:ℕ]→ P⟦i⟧⇨P⟦i+1⟧) ⇨ ∀[i:ℕ]→ P⟦i⟧ Type Choice ∀[f:σ τ ]→ ∃[choice:σ τ ] → ∀[x:τ] → (∃[y:σ] → f[x]:σ) ⇨ choice[x]:σ

Completeness of inference versus inferential undecidability of closed mathematical theories

"In mathematics, there is no ignorabimus." Hilbert, 1902

A closed mathematical theory is an extension of mathematics whose proofs are computationally enumerable. For example, group theory is obtained by adding the axioms of groups to Classical Direct Logic along with the axiom that theorems of group theory are computationally enumerable.

Theorem ProofsComputationalyEnumerable Nat is true but provably unprovable in Nat . 59

Proof:

Clearly by construction, ⊨ℕ ProofsComputationalyEnumerable Nat Suppose to obtain a contradiction that

⊢ Nat ProofsComputationalyEnumerable Nat
Then there is a provable in Nat computable total procedure

ProofsEnumeratorℕ:[ℕ]↦Proof Nat such that it is provable in Nat that ∀[p:Proof Nat ]→ ∃[i:ℕ]→ ProofsEnumerator Nat ∎[i]= p ∀[i:ℕ]→ ProofsEnumerator Nat ∎[i]:Proof Nat
A subset of the proofs in Nat are those proving that certain procedures [ℕ]↦ℕ are total. Consequently, there is a procedure

ProvedTotalsEnumerator Nat :[ℕ]↦([ℕ]↦ℕ)
that enumerates the provable in Nat total computable procedures [ℕ]↦ℕ that can be used in the implementation of the following procedure:

Diagonal∎[i:ℕ]:ℕ ≡ 1+ (ProvedTotalsEnumerator Nat ∎[i]) ∎[i]
Consequently:

• Diagonal is a provable in Nat total procedure because it is implemented using computable provable in Nat total procedures. • Diagonal is not a provable in Nat total procedure because it differs from every other computable provable in Nat total procedure. The above contradiction completes the proof.

Note that the closed mathematical theory Nat is inferentially undecidable i with respect to ProofsComputationalyEnumerable Nat does not mean incompleteness with respect to the information that can be inferred about theory Nat because

 ⊢⊬ Nat ProofsComputationalyEnumerable Nat  ⊢ ⊬ Nat ProofsComputationalyEnumerable Nat i sometimes called "incomplete"
Theorem ⊢ Nat Consistent Nat Proof: Suppose to derive an inconsistency that Consistent Nat . By the definition of inconsistency for Nat, there is some Ψ:Proposition Nat such that ├ Nat (Ψ  Ψ). By Existential Elimination, there is some proposition Ψ0 such that ├ Nat (Ψ0Ψ0) which can be used to infer in Nat that Ψ0Ψ0.

The above contradiction completes the proof.

Information Invariance i is a fundamental technical goal of logic consisting of the following: 1. Soundness of inference: information is not increased by inference ii 2. Completeness of inference: all information that necessarily holds can be inferred

Information Coordination

Technology now at hand can coordinate all kinds of digital information for individuals, groups, and organizations so their information usefully links together. 60 Information coordination needs to make use of the following information system principles:  Persistence. Information is collected and indexed.

 Concurrency: Work proceeds interactively and concurrently, overlapping in time.  Quasi-commutativity: Information can be used regardless of whether it initiates new work or become relevant to ongoing work.  Sponsorship: Sponsors provide resources for computation, i.e., processing, storage, and communications.  Pluralism: Information is heterogeneous, overlapping and often inconsistent.  Provenance: The provenance of information is carefully tracked and recorded.  Lossless : Once a system has some information, then it has it thereafter.

i Closely related to conservation laws in physics ii E.g. inconsistent information does not infer nonsense.

Opposition of Some Theoreticians

"By this it appears how necessary it is for nay man that aspires to true knowledge to examine the definitions of former authors; and either to correct them, where they are negligently set down, or to make them himself. For the errors of definitions multiply themselves, according as the reckoning proceeds, and lead men into absurdities, which at last they see, but cannot avoid, without reckoning anew from the beginning; in which lies the foundation of their errors..." [Hobbes Leviathan, Chapter 4] "Faced with the choice between changing one's mind and proving that there is no need to do so, almost everyone gets busy on the proof." John Kenneth Galbraith [1971 pg. 50] A number of theoreticians have opposed the results in this paper:  Some would like to stick with just first-order logic and not consider inconsistency robustness. 61  Some would like to stick with the first-order theories and not consider direct inference. 62  Some would like to stick with just Logic Programs (e.g. nondeterministic Turing Machines, λ-calculus, etc.) and not consider concurrency.

And some would like to have nothing to do with any of the above! 63 However, the results in this paper (and the driving technological and economic forces behind them) tend to push towards inconsistency robustness, direct inference, and concurrency.

Theoreticians are now challenged as to whether they agree that  Inconsistency is the norm.  Direct inference is the norm.  Logic Programs are not computationally universal.

Scalable Information Coordination

Information coordination works by making connections including examples like the following:  A statistical connection between "being in a traffic jam" and "driving in downtown Trenton between 5PM and 6PM on a weekday."  A terminological connection between "MSR" and "Microsoft Research."  A causal connection between "joining a group" and "being a member of the group."  A syntactic connection between "a pin dropped" and "a dropped pin."  A biological connection between "a dolphin" and "a mammal".  A demographic connection between "undocumented residents of California" and "7% of the population of California."  A geographical connection between "Leeds" and "England."  A temporal connection between "turning on a computer" and "joining an on-line discussion." By making these connections, iInfo TM information coordination offers tremendous value for individuals, families, groups, and organizations in making more effective use of information technology.

In practice coordinated information is invariably inconsistent. 64 Therefore iInfo must be able to make connections even in the face of inconsistency. 65 The business of iInfo is not to make difficult decisions like deciding the ultimate truth or probability of propositions. Instead it provides means for processing information and carefully recording its provenance including arguments (including arguments about arguments) for and against propositions.

Work to be done

"The best way to predict the future is to invent it." Alan Kay There is much work to be done including the following:

Invariance

Invariance should be precisely formulated and proved. This bears on the issue of how it can be known that all the principles of Direct Logic have been discovered.

Consistency

The following conjectures for Direct Logic need to be convincingly proved:

 Constructive consistency of Classical Direct Logic i relative to the consistency of mathematics. In this regard Classical Direct Logic is consonant with Bourbaki: Absence of contradiction, in mathematics as a whole or in any given branch of it, … appears as an empirical fact, rather than as a metaphysical principle. The more a given branch has been developed, the less likely it becomes that contradictions may be met with in its farther development. ii Thus the long historical failure to find an explosion in the methods used by Direct Logic can be considered to be strong evidence of its nontriviality.  Computational decidability of Provability Direct Logic (see appendix to this article).

 Development of inconsistency-robust statistical inference analogous to

Inconsistency Robust Direct Logic

Inconsistency Robustness

Inconsistency robustness of theories of Direct Logic needs to be formally defined and proved. Church remarked as follows concerning a Foundation of Logic that he was developing: "Our present project is to develop the consequences of the foregoing set of postulates until a contradiction is obtained from them, or until the development has been carried so far consistently as to make it empirically probable that no contradiction can be obtained from them. And in this connection it is to be remembered that just such empirical evidence, although admittedly inconclusive, is the only existing evidence of the freedom from contradiction of any system of mathematical logic which has a claim to adequacy." [Church 1933] iii Direct Logic is in a similar position except that the task is to demonstrate inconsistency robustness of inconsistent theories. This means that the exact boundaries of Inconsistency Robust Direct Logic as a minimal fix to firstorder logic need to be established.

i i.e. consistency of ├ ii [André Weil 1949] speaking as a representative of Bourbaki iii The difference between the time that Church wrote the above and today is that the standards for adequacy have gone up dramatically. Direct Logic must be adequate to the needs of reasoning about large software systems.

Argumentation

Argumentation is fundamental to inconsistency robustness.  Further work is need on fundamental principles of argumentation for large-scale information coordination. See [Hewitt 2008a[Hewitt , 2008b].  Tooling for Direct Logic needs to be developed to support large software systems. See [Hewitt 2008a].

Inferential Explosion

Inconsistencies such as the one about whether Pilot flies are relatively benign in the sense that they lack significant consequences to software engineering.

Other propositions (such as ├ T 1=0 in a theory T ) are more malignant because they can be used to infer that all integers are equal to 0 using mathematical induction. To address malignant propositions, deeper investigations of argumentation using must be undertaken in which the provenance of information will play a central role. See [Hewitt 2008a].

Robustness, Soundness, and Coherence

Fundamental concepts such as robustness, soundness, and coherence need to be rigorously characterized and further developed. Inconsistency-robust reasoning beyond the inference that can be accomplished in Direct Logic needs to be developed, e.g., analogy, metaphor, discourse, debate, and collaboration.

Evolution of Mathematics

"In the relation between mathematics and computing science, the latter has been far many years at the receiving end, and I have often asked myself if, when, and how computing would ever be able to repay the debt." [START_REF] Dijkstra | A Simple Fixpoint Argument Without the Restriction of Continuity[END_REF]] "We argue that mathematics will become more like programming." [Asperti, Geuvers and Natrajan 2009] Mathematical foundations are thought to be consistent by an overwhelming consensus of working professional mathematicians, e.g., mathematical theories of real numbers, integers, etc.

In practice, mathematical theories that are thought to be consistency by an overwhelming consensus of working mathematicians play an important supporting role for inconsistency-robust theories, e.g., theories of the Liver, Diabetes, Human Behavior, etc.

Conclusion

"The problem is that today some knowledge still feels too dangerous because our times are not so different to Cantor or Boltzmann or Gödel's time. We too feel things we thought were solid being challenged; feel our certainties slipping away. And so, as then, we still desperately want to cling to a belief in certainty. It makes us feel safe. ... Are we grown up enough to live with uncertainties or will we repeat the mistakes of the twentieth century and pledge blind allegiance to another certainty?" Malone [2007] Inconsistency robustness builds on the following principles:  We know only a little, but it affects us enormously i  At any point in time, much is wrong ii with the consensus of leading scientists but it is not known how or which parts.  Science is never certain; it is continually (re-)made Software engineers for large software systems often have good arguments for some proposition P and also good arguments for its negation of P. So what do large software manufacturers do? If the problem is serious, they bring it before a committee of stakeholders to try and sort it out. In many particularly difficult cases the resulting decision has been to simply live with the problem for an indefinite period. Consequently, large software systems are shipped to customers with thousands of known inconsistencies of varying severity where  Even relatively simple subsystems can be subtly inconsistent.



There is no practical way to test for inconsistency.  Even though a system is inconsistent, it is not meaningless.

Inconsistency Robust Direct Logic is a minimal fix to First-Order Logic. A big advantage of inconsistency robust logic is that it makes it practical for computer systems to reason about theories of practice (e.g. for macroeconomics, human history, etc.) that are pervasively inconsistent. Since software engineers have to deal with theories chock full of inconsistencies, Inconsistency Robust Direct Logic should be attractive. However, to make it relevant we need to provide them with tools that are cost effective.

i for better or worse ii e.g., misleading, inconsistent, wrong-headed, ambiguous, contra best-practices, etc.

Statistical reasoning can be important in practice including the following:

• Aggregation and Correlation • Interpolation and Extrapolation • Classification and Simulation • Neural net learning

Correlations derived using the above techniques can help boost information system performance provided that they are incorporated into inconsistency robust systems to limit correlational deficiencies.

Our everyday life is becoming increasingly dependent on large software systems. And these systems are becoming increasingly permeated with inconsistency and concurrency.

As pervasively inconsistent concurrent systems become a major part of the environment in which we live, it becomes an issue of common sense to use them effectively. We will need sophisticated software systems that formalize this common sense to help people understand and apply the principles and practices suggested in this paper.

Creating this software is not a trivial undertaking!

There is much work to be done! Abstraction and parsing are becoming increasingly important in software engineering. e.g.,  The execution of code can be dynamically checked against its documentation. Also Web Services can be dynamically searched for and invoked on the basis of their documentation.  Use cases can be inferred by specialization of documentation and from code by automatic test generators and by model checking.

 Code can be generated by inference from documentation and by generalization from use cases.

Abstraction and parsing are needed for large software systems so that that documentation, use cases, and code can mutually speak about what has been said and their relationships.

For example:

In Direct Logic, a sentence is a grammar tree (analogous to the ones used by linguists). Such a grammar tree has terminals that can be constants. And there are uncountably many constants, e.g., the real numbers: ii if t then s1 else s1

Note

iii The type of (p[x]) means that the Y fixed point construction cannot be used to construct sentences in Direct Logic.

Turing versus Gödel

"You shall not cease from exploration And the end of all our journeying Will be to arrive where we started And know the place for the first time." T.S. Eliot [1942] Turing recognized that proving that inference in mathematics is computationally undecidable is quite different than proving that there is a proposition of mathematics that is inferentially undecidable. i [Turing 1936, page 259]: "It should perhaps be remarked what I shall prove is quite different from the well-known results of Gödel [1931]. Gödel has shown that there are propositions U such that neither U nor U is provable. … On the other hand, I shall show that there is no general method which tells whether a given formula U is provable." 93

Although they share some similar underlying ideas, the method of proving computational undecidability developed by Church is much more robust than the one previously developed by Gödel that relies on his proposition I'm unprovable..

The difference can be explicated as follows:

• Actors: an Actor that has an address for itself can be used to generate infinite computations. • Propositions: using the Y fixed point construction for propositions can be used to infer inconsistencies in mathematics. As Wittgenstein pointed out, Gödel's proposition leads to inconsistency in mathematics. If the inconsistency caused by the Y fixed point construction for propositions was limited to just Gödel's proposition, then it would be somewhat tolerable for an inconsistency-robust theory. However, other propositions (constructed in a similar way) can be used to prove every proposition thereby rendering inference useless. This is why Direct Logic does not support using the Y fixed point construction for propositions. ii

Contra Gödel et. al

The proof of the consistency of mathematics in this article contradicts the result [Gödel 1931] (using his proposition I'm unprovable.) that mathematics cannot prove its own consistency. The resolution is that the Y fixed points do not exist for strongly typed propositions, which is contra Gödel et. al.

How the self-proof of consistency of mathematics was overlooked and then discovered

Before the paradoxes were discovered, not much attention was paid to proving consistency. Hilbert et. al. undertook to find a convincing proof of consistency. Gentzen found a consistency proof for the first-order Peano theory but many did not find it convincing because the proof was not elementary. Then following Carnap and Gödel, philosophers blindly accepted the mathematical necessity of the Y fixed point construction for propositions. None of them seemed to understand Wittgenstein's critique. (Gödel insinuated that Wittgenstein was "crazy.") Instead, philosophers turned their attention to exploring the question of which is the weakest theory in which Gödel's results can be carried out. They were prisoners of the existing paradigm.

Computer scientists brought different concerns and a new perspective. They wanted foundations with the following characteristics:

 powerful so that arguments (derivations) are short and understandable and all logical inferences can be formalized  standard so they can join forces and develop common techniques and technology  inconsistency robust because computers deal in pervasively inconsistent information. 1941] and[Löb 1955] also led to inconsistency in mathematics. So the consistency of mathematics also had to be rescued against use of the Y fixed point construction for propositions.  Direct Logic easily proves the consistency of mathematics. So the consistency of mathematics had to be rescued against Gödel's "2 nd incompleteness theorem."

 Direct Logic easily proves Church's Paradox. So the consistency of mathematics had to be rescued against the assumption that the theorems of mathematics can be computationally enumerated.

In summary, computer science advanced to a point where it caused the development of Direct Logic.

Paraconsistency i

Inconsistency robust logic is an important conceptual advance in that requires that nothing "extra" can be inferred just from the presence of a contradiction. For example, suppose that there is a language with just two propositions, namely, P and Q. Furthermore, suppose that P and (not P ) are axioms. Then, the only propositions that can be inferred in an inconsistency robust logic are (P and (not P )), ((not P ) and (not P )), (P or (not P )), etc. In particular, (P or Q ) cannot be inferred because otherwise Q could be erroneously inferred using (not P ) by the rule of Disjunctive Syllogism.

An example of a logic (called NanoIntuitionistic) which is not inconsistency robust has just one rule of inference, namely, classical proof by contradiction.

NanoIntuitionistic is not inconsistency robust because Q,  Q , (P Q ), etc. can be erroneously inferred from the contradictory axioms P and P . Note that Q cannot be inferred in NanoIntuitionistic (because there is no rule of double negation elimination). Consequently, NanoIntuitionistic is a paraconsistent logic ii (which was conceived by Stanisław Jaśkowski [START_REF] Jaśkowski | Propositional calculus for contradictory deductive systems[END_REF]] and then developed by many logicians to deal with inconsistencies in mathematical logic [START_REF] Arruda | Aspects of the historical development of paraconsistent logic[END_REF][START_REF] Priest | The History of Paraconsistent Logic" in Paraconsistent Logic: Essays on the Inconsistent[END_REF]) where a logic is by definition paraconsistent if and only if it is not the case that every proposition can be inferred from an inconsistency.

In conclusion, a paraconsistent logic (e.g. NanoIntuitionistic) can allow erroneous inferences (e.g. Q)) from an inconsistency that are not allowed by inconsistency robustness. Of course, an inconsistency robust logic is also necessarily paraconsistent.

Natural Deduction Inference rules for Inconsistency Robust Direct Logic

End Notes

1 Inference is direct when it does not involved unnecessary circumlocutions, e.g., coding sentences as Gödel numbers. In Direct Logic, it is possible speak directly about inference relationships.

2 This section shares history with [Hewitt 2010b] 3 D'Ariano and Tosini [2010] showed how the Minkowskian space-time emerges from a topologically homogeneous causal network, presenting a simple analytical derivation of the Lorentz transformations, with metric as pure event-counting. Do events happen in space-time or is space-time that is made up of events? This question may be considered a "which came first, the chicken or the egg?" dilemma, but the answer may contain the solution of the main problem of contemporary physics: the reconciliation of quantum theory (QT) with general relativity (GR).Why? Because "events" are central to QT and "space-time" is central to GR. Therefore, the question practically means: which comes first, QT or GR? In spite of the evidence of the first position-"events happen in space-time"-the second standpoint-"space-time is made up of events"-is more concrete, if we believe à la Copenhagen that whatever is not "measured" is only in our imagination: space-time too must be measured, and measurements are always made-up of events. Thus QT comes first. How? Space-time emerges from the tapestry of events that are connected by quantum interactions, as in a huge quantum computer: this is the Wheeler's "It from bit." [START_REF] Wheeler | It from Bit[END_REF]]. 4 According to [Law 2006], a classical realism (to which he does not subscribe) is: Scientific experiments make no sense if there is no reality independent of the actions of scientists: an independent reality is one of conditions of possibility for experimentation. The job of the investigator is to experiment in order to make and test hypotheses about the mechanisms that underlie or make up reality. Since science is conducted within specific social and cultural circumstances, the models and metaphors used to generate fallible claims are, of course, socially contexted, and always revisable…Different 'paradigms' relate to (possibly different parts of) the same world. 5 Vardi [2010] has defended the traditional paradigm of proving that program meet specifications and attacked an early critical analysis as follows: "With hindsight of 30 years, it seems that De Millo, Lipton, and Perlis ' [1979] article has proven to be rather misguided." However, contrary to Vardi, limitations of the traditional paradigm of proving that program meet specifications have become much more apparent in the last 30 years-as admitted even by some who had been the most prominent proponents, e.g., [Hoare 2003[Hoare , 2009]. other aspects of the programming task. There will always be a limit at which the engineer judges that the cost of such specification is greater than the benefit that could be obtained from it; and that testing will be adequate for the purpose, and cheaper. Finally, verification [proving that programs meet specifications] cannot protect against errors in the specification itself. 8 Popper [1934] section 30. 9 The thinking in almost all scientific and engineering work has been that models (also called theories or microtheories) should be internally consistent, although they could be inconsistent with each other. Indeed some researchers have even gone so far as to construct consistency proofs for some small software systems, e.g., [Davis and Morgenstern 2005] in their system for deriving plausible conclusions using first-order logical inference for Multi-Agent Systems. In order to carry out the consistency proof of their system, Davis and Morgenstern make some simplifying assumptions:  No two agents can simultaneously make a choice (following [START_REF] Reiter | Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems[END_REF]).  No two agents can simultaneously send each other inconsistent information.  Each agent is individually serial, i.e., each agent can execute only one primitive action at a time.  There is a global clock time.  Agents use classical Speech Acts (see [Hewitt 2006b[Hewitt 2007a[Hewitt , 2007c[Hewitt , 2008c]]).  Knowledge is expressed in first-order logic. The above assumptions are not particularly good ones for modern systems (e.g., using Web Services and many-core computer architectures). [Hewitt 2007a] 13 According to [START_REF] Minsky | A Framework for Representing Knowledge[END_REF]]:

"The consistency that [first-order] logic absolutely demands is not otherwise usually availableand probably not even desirable!because consistent systems are likely to be too 'weak'." "Very large databases are a major opportunity for science and data analytics is a remarkable new field of investigation in computer science. The effectiveness of these tools is used to support a "philosophy" against the scientific method as developed throughout history. According to this view, computer-discovered correlations should replace understanding and guide prediction and action. Consequently, there will be no need to give scientific meaning to phenomena, by proposing, say, causal relations, since regularities in very large databases are enough: "with enough data, the numbers speak for themselves". The "end of science" is proclaimed.

Using classical results from ergodic theory, Ramsey theory and algorithmic information theory, we show that this "philosophy" is wrong. For example, we prove that very large databases have to contain arbitrary correlations. These correlations appear only due to the size, not the nature, of data. They can be found in "randomly" generated, large enough databases, which-as we will prove-implies that most correlations are spurious. Too much information tends to behave like very little information. The scientific method can be enriched by computer mining in immense databases, but not replaced by it." 19 In [Law 2006]. Emphases added. 20 A very similar limitation holds for intuitionistic logic. 21 In Latin, the principle is called ex falso quodlibet which means that from falsity anything follows. 22 Using the symbol ├ to mean "infers in mathematics." The symbol was first published in [Frege 1879]. 23 [Nekham 1200, pp. 288-289]; later rediscovered and published in [Lewis and Langford 1932] the following principle: Ψ, (ΨΦ├ )├  However, the above principle immediately derives extraneous  introduction when  is ΨΦ. In Direct Logic, argumentation of the above form would often be reformulated as follows to eliminate the spurious Φ middle proposition: Ψ, (Ψ├ )├  25 using propositional equivalences 26 Turing noted that first-order logic can be used to make invalid inferences using inconsistent information "without actually going through [an explicit] contradiction." [START_REF] Diamond | Wittgenstein's Lectures on the Foundations of Mathematics[END_REF]] Furthermore, [Church 1935] first proved that it is computationally undecidable whether a mathematical theory of practice is inconsistent. 27 Direct Logic is distinct from the Direct Predicate Calculus [START_REF] Ketonen | A decidable fragment of Predicate Calculus[END_REF]]. 28 The importance of (counter) examples in reasoning was emphasized in [Rissland 1984] citing mathematics, law, linguistics and computer science.

According to [Gordon 2009]: [START_REF] Toulmin | The Uses of Argument[END_REF]] was one of the first to reflect on the limitations of mathematical logic as a model of rationality in the context of everyday discourse and practical problems. By the 1950s, logic had become more or less synonymous with mathematical logic, as invented by Boole, De Morgan, Pierce, Frege, Hilbert and others, starting 45 The below derivation is quite general and applies to the Abstract State Machine (ASM) model [Blass, Gurevich, Rosenzweig, andRossman 2007a, 2007b;Glausch and Reisig 2006], which consequently are not really models of concurrency. It also applies to the parallel lambda calculus, which includes all the capabilities of the nondeterministic lambda calculus.

Researchers (before the Actor Model was invented) hypothesized that the parallel lambda calculus naturally modeled all of computation and their research programme was to reduce all computation to the parallel lambda calculus [Scott andStrachey 1971, Milne and[START_REF] Milne | A Theory of Programming Language Semantics Chapman and Hall[END_REF]. 46 This proof does not apply to extensions of Nondeterministic Turing

Machines that are provided with a new primitive instruction NoLargest which is defined to write an unbounded large number on the tape. Since executing NoLargest can write an unbounded amount of tape in a single instruction, executing it can take an unbounded time during which the machine cannot read input. Also, the NoLargest primitive is of limited practical use. Consider a Nondeterministic Turing Machine with two input-only tapes that can be read nondeterministically and one standard working tape.

It is possible for the following program to copy both of its input tapes onto its working tape:

Step 1: Either 1. copy the current input from the 1 st input tape onto the working tape and next do Step 2, or 2. copy the current input from the 2 nd input tape onto the working tape and next do Step 3.

Step 2: Next do Step 1.

Step 3: Next do Step 1.

It is also possible that the above program does not read any input from the 1 st input tape (cf. [Knabe 1993]) and the use of NoLargest is of no use in alleviating this problem. Bounded nondeterminism is a symptom of deeper underlying issues with Nondeterministic Turing Machines. 47 Consequently,  The tree has an infinite path. ⇔ The tree is infinite. ⇔ It is possible that P does not halt. If it is possible that P does not halt, then it is possible that that the set of outputs with which P halts is infinite.  The tree does not have an infinite path. ⇔ The tree is finite. ⇔ P always halts. If P always halts, then the tree is finite and the set of outputs with which P halts is finite. 48 Arbiters render meaningless the states in the Abstract State Machine (ASM) model [Blass, Gurevich, Rosenzweig, andRossman 2007a, 2007b;Glausch and Reisig 2006]. 49 The logic gates require suitable thresholds and other characteristics. 50 cf. denotational semantics of the lambda calculus [START_REF] Scott | Data Types as Lattices[END_REF] faced with a device, designed to lift stream water, but which is so badly designed that it spills most of its freight, do not set themselves to the design of a better model, but rather devote much of their energy to constructing ingenious arguments to convince themselves that the device is admirable, that they do not need or want the device to deliver more water; that there is nothing wrong with wasting water and that it may even be desirable; and that in order to "improve" the device they would have to change some features of the design, a thing which goes totally against their engineering intuitions and which they could not possibly consider doing." [Routley 2003] 62 For example:

From: Harvey Friedman Sent: Wednesday, April 20, 2016 10:53 To: Carl Hewitt Cc: Martin Davis @cs.nyu; Dana Scott @cmu; Eric Astor @uconn; Mario Carneiro @osu; Dave Mcallester @ttic; Joe Shipman Subject: Re: Parameterized types in the foundations of mathematics "And Max Planck, surveying his own career in his Scientific Autobiography [Planck 1949], sadly remarked that 'a new scientific truth does not triumph by convincing its opponents and making them see the light, but rather because its opponents eventually die, and a new generation grows up that is familiar with it.'" 64 It is not possible to guarantee the consistency of information because consistency testing is computationally undecidable even in logics much weaker than first order logic. Because of this difficulty, it is impractical to test whether information is consistent.

65 Consequently iDescriber makes use of direct inference in Direct Logic to reason more safely about inconsistent information because it omits the rules of first-order logic that enable every proposition to be inferred from a single inconsistency. 66 By the Computational Representation Theorem [Clinger 1981;Hewitt 2006], which can define all the possible executions of a procedure. 87 [Church 1956; Concoran 1973, 1980; Boulos 1975; Shapiro 2002] 88 "The world that appears to our senses is in some way defective and filled with error, but there is a more real and perfect realm, populated by entities [called "ideals" or "forms"] that are eternal, changeless, and in some sense paradigmatic for the structure and character of our world. Among the most important of these [ideals] (as they are now called, because they are not located in space or time) are Goodness, Beauty, Equality, Bigness, Likeness, Unity, Being, Sameness, Difference, Change, and Changelessness. (These terms -"Goodness", "Beauty", and so onare often capitalized by those who write about Plato, in order to call attention to their exalted status;…) The most fundamental distinction in Plato's philosophy is between the many observable objects that appear beautiful (good, just, unified, equal, big) and the one object that is what Beauty (Goodness, Justice, Unity) really is, from which those many beautiful (good, just, unified, equal, big) things receive their names and their corresponding characteristics. Nearly every major work of Plato is, in some way, devoted to or dependent on this distinction. Many of them explore the ethical and practical consequences of conceiving of reality in this bifurcated way. We are urged to transform our values by taking to heart the greater reality of the [ideals] and the defectiveness of the corporeal world." [START_REF] Kraut | Plato" Stanford Encyclopedia of Philosophy[END_REF]] 89 Structuralism takes a different view of mathematics:

The structuralist vigorously rejects any sort of ontological independence among the natural numbers. The essence of a natural number is its relations to other natural numbers. The subject matter of arithmetic is a single abstract structure, the pattern common to any infinite collection of objects that has a successor relation, a unique initial object, and satisfies the induction principle. The number 2 is no more and no less than the second position in the natural number structure; and 6 is the sixth position.

Neither of them has any independence from the structure in which they are positions, and as positions in this structure, neither number is independent of the other. [Shapiro 2000]

  Things that are equal to the same are equal to each other." B ≡ "The lengths of two sides of this Triangle are things that are equal to the same." Z ≡ "The length of two sides of this Triangle are equal to each other."

  above axiom does not compute any actual output! Instead the above axiom simply asserts the existence of unbounded outputs for Unbounded∎[ ].

1)

  Consistent // hypothesis to derive a contradiction just in this subargument ├ Consistent // rule of Proof by Contradiction using 1) and 4) 2) ∃[Ψ:Proposition]→├(ΨΨ)// definition of inconsistency using 1)

  : type theory of Classical Direct Logic is much stronger than constructive type theory with constructive logic 67 because Classical Direct Logic has all of the power of Classical Mathematics. Propositions e.g. ∀[n:ℕ]→ ∃[m:ℕ]→ m>n i.e., for every ℕ there is a larger ℕ intuitively : For every number, there is a larger number. Sentences e.g. (∀[n:ℕ]→ (∃[m:ℕ]→ (m>n))) i.e., the sentence that for every ℕ there is a larger ℕ  Sentences, i.e., a Sentence is a discrimination of the following where order:ℕ+:  (x):Sentenceorder+1 i where x:VariableSentenceorder,.  (s):Sentenceorder where s:Sentenceorder  (s1s2),(s1s2),(s1⇨s2),(s1⇔s2):Sentenceorder where s1,s2:Sentenceorder  (t � True⦂ s1⍌ False⦂ s2) ii :Sentenceorder where t:ExpressionBoolean, s1,s2:Sentenceorder  (t1=t2),(t1⊑t2),(t1t2):Sentence1 where t1:Expressionτ and t2:Expressionτ  (t1t2),(t1:t2):Sentence1 where t1:Expressionτ1 and t2:Expressionτ2 • (∀[x:τ1]→ s),(∃[x:τ1]→ s):Sentenceorder where x:Variableτ1 in s and s:Sentenceorder • (f[x]):Sentence1 where x:Expressionτ and f:ExpressionBoolean τ  • (p⟦x⟧):Sentenceorder+1 iii where x:Expressionτ and p:𝐒𝐞𝐧𝐭𝐞𝐧𝐜𝐞order 𝛕 • (s1,…,sn-1├ 𝐩 𝐓 sn):Sentenceorder where T:ExpressionTheory, s1 to n:Sentenceorder and p:ExpressionProof • s:Sentenceorder where s:StringSentenceorder i The type of (x) means that the Y fixed point construction cannot be used to construct sentences in Direct Logic.

  Not if I have anything to say about it! HarveyOn Wed, Apr 20, 2016 at 11:25 AM, Carl Hewitt wrote: > Hi Martin, > > Please post the message below to FOM [Foundations of Mathematics forumHarvey Friedman on the FOM Wiki: "I have not yet seen any seriously alternative foundational setup that tries to be better than ZFC in this [categoricity of models] and other respects that isn't far far worse than ZFC in other even more important respects." > > Of course, ZFC is a trivial consequence of parameterized types with the following definition for set of type τ: > > Setτ ≡ Boolean τ > > Also of course, classical mathematics can be naturally formalized using parameterized types. For example, see "Inconsistency Robustness in Foundations: Mathematics self proves its own Consistency and Other Matters" in HAL Archives.

  67 e.g.[Shulman 2012, nLab 2014] 68 True≠False ∀[x:Boolean]→ x=True  x=False69 The theory of the natural numbers Nat is axiomatised as follows where S is the successor function: 0ℕ:ℕ  +1:ℕ ℕ  ∀[i:ℕ]→ +1[i]≠0ℕ  ∀[i, j:ℕ]→ +1[i]= +1[j] ⇒ i=j For each order:ℕ+ and P:Propositionorder ℕ :(P⟦0ℕ⟧  ∀[i:ℕ]→ P⟦i⟧⇨P⟦+1[i]⟧) ⇨ ∀[i:ℕ]→ P⟦i⟧ 110 70The theory of the ordinals Ord can be axiomatized as follows: 0 O :O  ∀[α:O]→ α≧0 O  Ordinal types: ∀[α:O]→ α>0 O ⇒ α:TypeO  Successor ordinals o +1:O O o ∀[α:O]→ +1[α]>α o ∀[α,β:O]→ β>α ⇒ +1[α]≦β  Sum Replacement for ordinals: o ∀[α:O,f:O O ]→ ⊍αf:O o ∀[α,β<α:O,f:O O ]→ f[β]≦⊍αf o ∀[α,β:O,f:O O ]→ (∀[δ<α]→ f[δ]≦β) ⇨ ⊍αf≦β  Omega ordinals o ∀[α:O]→ ωα:O o ∀[α:O]→ α:ω0 ⇔ α:ℕ o Successor: ∀[α:O]→ ⇨ |ωα+1| ≅ |𝐁𝐨𝐨𝐥𝐞𝐚𝐧 𝛚 α | ∀[α,β:O]→ |β|≅|ωα+1| ⇨ ωα≦β where |τ1| ≅ |τ2| ⇔ ∃[f:τ 2 τ 1 ]→ OneToOneOntoτ1,τ2[f]o ∀[α:O]→ (∄[δ:O]→ α=+1[δ]) ⇨ ωα = ⊍ β<α 𝛚 β  ∀[α,β<α,δ<β:O]→ α<δ  Trichotomy: ∀[α,β:O]→ α<β ⊻ α=β ⊻ β<α  For each order:ℕ+ and P:Propositionorder O : the following ordinal induction axiom holds: (∀[α:O]→ ∀[β<α:O]→ P⟦β⟧⇨P⟦α⟧) ⇨ ∀[α:O]→ P⟦α⟧

We can stop looking for models. We can analyze the data without hypotheses about what it might show. We

	• More variables tested
	• Greater significance of the outcome
	• More flexibility in designs, definitions, and outcomes
	• Greater financial interest in the outcome
	• Lesser skepticism of alternatives
	• Greater hotness of the field of research
	• Lower variation in exploration of alternatives
	• Greater reputational investment in the outcome
	• Larger number of scientific teams racing to publish
	• Less time to conduct and analyze the study
	• Fewer number of times that the study has been independently confirmed,
	replicated, and critiqued with transparent availability of all results and
	integration of data across teams
	• Greater ideological commitment to the outcome
	The upshot is that the following (currently popular) opinion is exactly
	backwards [Anderson 2009]: 17
	"Correlation is enough. can throw the numbers into the biggest computing clusters the world has
	ever seen and let statistical algorithms find patterns where science
	cannot." (emphasis added)
	Of course, Anderson missed the whole point that causality is about affecting
	correlations through interaction. Statistical algorithms can always find
	meaningless correlations. 18
	Models (i.e. theories) can be used to make interventions (experiments) to test
	which correlations are causal.

  then ℙ|T is wildly nonstable

	Theory confirmation. If ├ T , then ℙT|≅ 1.
	i.e., A theory is confirmed by any proposition that it infers
	Proof:
	1) ├ T 	// hypothesis
	2) ℙT = ℙ	// using 1)
	3) ℙT| = 4) ℙT| ≅ 1 ℙT ℙ	// using probability // using 3) and 4)

  ' with utmost innocence: yes, of course, otherwise we would not have made them with our own hands ii ! The Portuguese, shocked but scrupulous, not want to condemn without proof, gave the Africans one last chance: 'You can't say both that you've made your own [idols] and that they are true divinities iii ; you have to choose: it's either one or the other. Unless,' they went on indignantly, 'you really have no brains, and you're as oblivious to the principle of contraction iv as you are to the sin of idolatry.' Stunned silence from the [Africans] who failed to see any contradiction." v

	Theory Dependence
	Inference in Inconsistency Robust Direct Logic is theory dependent. For
	example [Latour 2010b]:
	" 'Are these stone, clay, and wood idols true divinities i ?' [The Africans]
	answered 'Yes!
	i Derivation by contradiction has played an important role in science (emphasized by
	Karl Popper [1962]) as formulated in his principle of refutation which in its most
	stark form is as follows:
	If ├ T Ob for some observation Ob, then it can be concluded that T is refuted (in a
	theory called Popper ), i.e., ├ Popper T
	See Suppe [1977] for further discussion.

31

For example, together ├ T  and ├ T  infer ├ T , which in Inconsistency Robust Direct Logic can be expressed as follows by Direct Argumentation: , (├ T )├ T 

  By contrast, in the Actor model, computation is conceived as distributed in space where computational devices called Actors communicate asynchronously using addresses of Actors and the entire computation is not in any well-defined state. The behavior of an Actor is defined when it receives a message and at other times may be indeterminate.Axioms of locality including Organizational and Operational hold as follows: The local storage of an Actor can include addresses only 1. that were provided when it was created or of Actors that it has created 2. that have been received in messages  Operation: In response to a message received, an Actor can 1 create more Actors 2 send messages i to addresses in the following:  the message it has just received  its local storage 3 for an exclusive ii Actor, designate how to process the next message received iii

	It is "absolutely impossible that anybody who understands the question
	[What is computation?] and knows Turing's definition should decide for a
	different concept." 42
	• Direct Argumentation (inference directly expressed)
	• Inconsistency Robustness
	• Inconsistency-robust Natural Deduction 39
	• Intuitive inferences hold including the following:
	o Propositional equivalences i
	o Reasoning by disjunctive cases, i.e.,
	(), (├ What is Computation?
	"Any problem in computer science can be solved by introducing
	another level of abstraction."
	paraphrase of Alan Perlis
	Turing's model of computation was intensely psychological. 40 He proposed
	the thesis that it included all of purely mechanical computation. 41
	Gödel declared that
	i except absorption

T ), (├ T Ω) ├ T Ω o -Elimination, i.e., ¬Φ, (ΦΨ)├ T Ψ o Entailment: A proposition entails another if an only if negation of the latter entails negation of the former, i.e., Ψ⇒ T  if and only if ¬⇒ T ¬Ψ o Theorem Use: A theorem can be used in a derivation, i.e., (├ T )├ T  o Inconsistency Robust Derivation by Contradiction: A hypothesis can be refuted by showing that it entails a contradiction, i.e., (⇒ T (¬))├ T ¬

Actor Model of Computation

The distinction between past, present and future is only a stubbornly persistent illusion. Einstein

Concurrency has now become the norm. However nondeterminism came first. See [Hewitt 2010b] for a history of models of nondeterministic computation.  Organization:

  Turing Machine: a computation can be represented as a global state that determines all information about the computation. It can be nondeterministic as to which will be the next global state, e.g.next state as a global clock advances in time, e.g.,Simula [Dahl and Nygaard 1967].43 • Actors: a computation can be represented as a configuration.Information about a configuration can be indeterminate.

							, in
	simulations	where	the	global	state	can	transition
	nondeterministically to the

i

Functions defined by lambda expressions

[Church 1941

] are special case Actors that never change.

  iii

		Inverter
	Input1
		Nand
			Nor
		`Output1
		Nxor
	Input2	Nand	Nor	Output2
		Inverter
		Arbiter Concurrency Primitive 49

  In the logic community,Mike Dunn, Sol Feferman, Mike Genesereth, Tim Hinrichs, Mike Kassoff, John McCarthy, Chris Mortensen, Graham Priest, Dana Scott, Richard Weyhrauch and Ed Zalta provided valuable feedback Dana Scott made helpful suggestions concerning inferential undecidability. Richard Waldinger provided extensive suggestions that resulted in better focusing a previous version of this paper and increasing its readability. Discussion with Pat Hayes and Bob Kowalski provided insight into the early history of Prolog. Communications from John McCarthy and Marvin Minsky suggested making common sense a focus. Mike Dunn collaborated on looking at the relationship of the Boolean Fragment of Inconsistency Robust Direct Logic to R-Mingle. Greg Restall pointed out that Inconsistency Robust Direct Logic does not satisfy some Relevantist principles. Gerry Allwein and Jeremy Forth made detailed comments and suggestions for improvement. Bob Kowalski and Erik Sandewall provided helpful pointers and discussion of the relationship with their work. Discussions with Ian Mason and Tim Hinrichs helped me develop Löb's theorem for Direct Logic. Scott Fahlman suggested introducing the roadmap in the introduction of the paper. At CMU, Wilfried Sieg introduced me to his very interesting work with Clinton Field on automating the search for proofs of the Gödel/Rosser inferential undecidability theorems. Also at CMU, I had productive discussions with Jeremy Avigad, Randy Bryant, John Reynolds, Katia Sycara, and Jeannette Wing. At my MIT seminar and afterwards, Marvin Minsky, Ted Selker, Gerry Sussman, and Pete Szolovits made helpful comments. Les Gasser, Mike Huhns, Victor Lesser, Pablo Noriega, Sascha Ossowski, Jaime Sichman, Munindar Singh, etc. provided valuable suggestions at AAMAS'07. I had a very pleasant dinner with Harvey Friedman at Chez Panisse after his 2 nd Tarski lecture. Jeremy Forth, Tim Hinrichs, Fanya S. Montalvo, and Richard Waldinger provided helpful comments and suggestions on the logically necessary inconsistencies in theories of Direct Logic. Rineke Verbrugge provided valuable comments and suggestions at MALLOW'07. Mike Genesereth and Gordon Plotkin kindly hosted my lectures at Stanford and Edinburgh, respectively, on "The Logical Necessity of Inconsistency". Inclusion of Cantor's diagonal argument as motivation was suggested by Jeremy Forth. John McCarthy pointed to the distinction between Logic Programs and the Logicist Programme for Artificial Intelligence. Reviewers at JAIR made useful suggestions. Mark S. Miller made important suggestions for improving the meta-circular definition of ActorScript. Comments by Michael Beeson helped make the presentation of Direct Logic more rigorous. Conversations with Jim Larson helped clarify the relationship between first-order logic and the inconsistency robust logic. An anonymous referee of the Journal of Logic and Computation made a useful comment. John-Jules Meyer and Albert Visser provided helpful advice and suggestions. Comments by Mike Genesereth, Eric Kao, and Mary-Anne Williams at my Stanford Logic Group seminar "Inference in Boolean Direct Logic is Computationally Decidable" on 18 November 2009 greatly improved the explanation of direct inference. Discussions at my seminar "Direct Inference for Direct Logic TM Reasoning" at SRI hosted by Richard Waldinger on 7 January 2010 helped improve the presentation of Direct Logic. Helpful comments by Emily Bender, Richard Waldinger and Jeannette Wing improved the section on Inconsistency Robustness. Eric Kao provided numerous helpful comments and discovered bugs in the principles of Self-refutation and Excluded Middle that were part of a previous version of Inconsistency Robust Direct Logic [Kao 2011]. Self-refutation has been replaced by Self-annihilation in the current version. Stuart Shapiro provided helpful information on why SNePS [Shapiro 2000] was based on Relevance Logic. Discussions with Dennis Allison, Eugene Miya, Vaughan Pratt and others were helpful in improving this article.Make Travers made suggestions and comments that greatly improved the overall organization. Richard Waldinger provided guidance on first-order logic automatic theorem provers. Illuminating conversations with Patrick Suppes provided additional ideas for improvement. Discussions with Ron Rivest greatly improved the section on probabilistic inference. Rachel Briggs helped debug the axioms for entailment.

	Bibliography
	Aarts, et. al. Estimating the reproducibility of psychological science Science.
	August 28, 2015.
	Hal Abelson and Gerry Sussman Structure and Interpretation of Computer
	Programs 1984.
	Luca Aceto and Andrew D. Gordon (editors). Algebraic Process Calculi: The
	First Twenty Five Years and Beyond Bertinoro, Italy, August, 2005.
	Sanjaya Addanki, Roberto Cremonini, and J. Scott Penberthy. "Reasoning
	about assumptions in graphs of models" Readings in Qualitative Reasoning
	about Physical Systems. Kaufman. 1989.
	Gul Agha. Actors: A Model of Concurrent Computation in Distributed
	Systems Doctoral Dissertation. 1986.
	Gul Agha, Ian Mason, Scott Smith, and Carolyn Talcott. "A foundation for
	Actor computation." Journal of Functional Programming. 1997.
	Allen, L. E., and Saxon, C. S. "More is needed in AI: Interpretation assistance
	for coping with the problem of multiple structural interpretations" ICAIL
	1991.

  14 [START_REF] Dunn | Contradictory Information: Better than the Nothing CMU Philosophy Colloquium[END_REF] 15[International Committee of Medical Journal Editors 2016] has proposed that medical study data must be shared for all published articles.16 [Ioannnidis 2005b].17 Anderson is recommending a passive very conservative Bayesian approach instead of the scientific approach of active theorizing and intervening.18 According to [Calude and Longo 2016]:

  in the middle of the nineteenth century. Interestingly, Toulmin proposed legal argumentation as a model for practical reasoning, claiming that normative models of practical reasoning should be measured by the ideals of jurisprudence. [Walton 2006] is a good starting point for getting an overview of the modern philosophy of argumentation. 29 in Rebecca Herold Managing an Information Security and Privacy Awareness and Training Program 2005. p. 101. 30 although there is no claim concerning Euclid's own orientation 31 Cf. "on the ordinary notion of proof, it is compelling just because, presented with it, we cannot resist the passage from premises to conclusion without being unfaithful to the meanings we have already given to the expressions employed in it." [Dummett 1973] 32 Anthony D'Angelo, The College Blue Book 33 Rosemary Redfield. Arsenic associated bacteria (NASA's claims) RR Research blog. Dec. 6, 2010. 34 Felisa Wolfe-Simon, et. al. A bacterium that can grow by using arsenic instead of phosphorus Science. Dec. 2, 2010.

i i.e., using only addition, subtraction, multiplication, and division ii emphasis added

i This argument appeared in[Church 1934] expressing concern that the argument meant that there is "no sound basis for supposing that there is such a thing as logic." ii See section immediately below.

i For example, there can be messages in transit that will be delivered at some time or the infrastructure will throw an exception.

i with graph {[ ] ⇝ 0, [ ] ⇝ 1, [ ] ⇝ 2, … }ii Actors are the universal conceptual primitives of concurrent computation.iii dashes are used solely to delineate crossing wires

i using binary representation. See[START_REF] Feferman | About and around computing over the reals" Computability: Gödel, Church[END_REF]] for more on computation over the reals.

i In fact,[Kowalski 1980] forcefully stated:"There is only one language suitable for representing information --whether declarative or procedural --and that is first-order predicate logic. There is only one intelligent way to process information --and that is by applying deductive inference methods." ii Note that there are two expressions (separated by "either") in the bodies which provides for nondeterminism.

i[START_REF] Jaśkowski | On the Rules of Suppositions in Formal Logic[END_REF]] developed Natural Deduction cf.[Barker-Plummer, Barwise, and Etchemendy 2011]

i Joint work with Eric Kao ii sometimes called "incomplete"

i sometimes called "incompleteness." ii There seem to be no practical uses for the Y fixed point construction for propositions in the mathematical foundations of Computer Science.

i This section builds on[START_REF] Meyer | Review of Inconsistency Robustness[END_REF]].ii that is not inconsistency robust

[START_REF] Pospesel | A tool in modeling disagreement in law: Preferring the most specific argument[END_REF]] has discussed extraneous  introduction on in terms of

The converse does generally not hold: () ⇏  If () ⇒ , then () ⇒  and therefore () ⇒  meaning  ⇒ , which is not allowed.

Acknowledgements

"Science and politics and aesthetics, these do not inhabit different domains. Instead they interweave. Their relations intersect and resonate together in unexpected ways." Law [2004 pg. 156] Sol Feferman, Mike Genesereth, David Israel, Bill Jarrold, Ben Kuipers, Pat Langley, Vladimir Lifschitz, Frank McCabe, John McCarthy, Fanya S. Montalvo, Peter Neumann, Ray Perrault, Natarajan Shankar, Mark Stickel, Richard Waldinger, and others provided valuable feedback at seminars at Stanford, SRI, and UT Austin to an earlier version of the material in this paper. For the AAAI Spring Symposium'06, Ed Feigenbaum, Mehmet Göker, David Lavery, Doug Lenat, Dan Shapiro, and others provided valuable feedback. At MIT Henry Lieberman, Ted Selker, Gerry Sussman and the members of Common Sense Research Group made valuable comments. Reviewers for AAMAS '06 and '07, KR'06, COIN@AAMAS'06 and IJCAR'06 made suggestions for improvement.

Maurice Bruynooghe, Luís Moniz Pereira, Jörg Siekmann, Maarten van Emden. "A Portrait of a Scientist as a Computational Logician" Computational Logic: Logic Programming and Beyond: Essays in Honour of Robert A. Kowalski, Part I Springer. 2004. Cristian Calude and Giuseppe Longo. "The Deluge of Spurious Correlations in Big Data" Foundations of Science Springer. March 2016. Philip Campbell, et. al. "Digital Intuition" Nature editorial. January 27, 2016. Martin Caminda. "On the Issue of Contraposition of Defeasible Rules" COMMA'08. Andrea Cantini "Paradoxes and Contemporary Logic" The Stanford Encyclopedia of Philosophy October 16, 2007. George Cantor. "Diagonal Argument" German Mathematical Union (Deutsche Mathematiker-Vereinigung) (Bd. I, S. 75-78 ) 1890-1. Rudolph Carnap. Logische Syntax der Sprache. (The Logical Syntax of Language Open Court Publishing 2003) 1934. Luca Cardelli and Andrew Gordon. "Mobile Ambients" Foundations of Software Science and Computational Structures Springer, 1998. Lewis Carroll "What the Tortoise Said to Achilles" Mind 4. No. 14. 1895. Lewis Carroll. Through the Looking-Glass Macmillan. 1871. Carlo Cellucci "Gödel's Incompleteness Theorem and the Philosophy of Open Systems" Kurt Gödel: Actes du Colloque, Neuchâtel 13-14 juin 1991, Travaux de logique N. 7, Centre de Recherches Sémiologiques, University de Neuchâtel. http://w3.uniroma1.it/cellucci/documents/Goedel.pdf Carlo Cellucci "The Growth of Mathematical Knowledge: An Open World View" The growth of mathematical knowledge Kluwer. 2000. Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang Ranking Abstractions ESOP'08. Alonzo Church "A Set of postulates for the foundation of logic (1)" Annals of Mathematics. Vol. 33, 1932. Alonzo Church "A Set of postulates for the foundation of logic (2)" Annals of Mathematics. Vol. 34, 1933. Alonzo Church. An unsolvable problem of elementary number theory Bulletin of the American Mathematical Society 19, May, 1935. American Journal of Mathematics, 58 (1936), Alonzo Church The Calculi of Lambda-Conversion Princeton University Press. 1941. Will Clinger. Foundations of Actor Semantics MIT Mathematics Doctoral Dissertation. June 1981. Paul Cohen "My Interaction with Kurt Gödel; the man and his work" Gödel Centenary: An International Symposium Celebrating the 100th Birthday of Kurt Gödel April 27-29, 2006. Alain Colmerauer and Philippe Roussel. "The birth of Prolog" History of Programming Languages ACM Press. 1996 54 Melvin Conway. Design of a separable transition-diagram compiler CACM. 1963. F. S. Correa da Silva, J. M. Abe, and M. Rillo. "Modeling Paraconsistent Knowledge in Distributed Systems". Technical Report RT-MAC-9414, Instituto de Matematica e Estatistica, Universidade de Sao Paulo, 1994. James Crawford and Ben Kuipers. "Negation and proof by contradiction in access-limited logic." AAAI-91. Haskell Curry. "Functionality in Combinatory Logic" Proceedings of the National Academy of Sciences 20. 1934. Haskell Curry. "Some Aspects of the Problem of Mathematical Rigor" Bulletin of the American Mathematical Society Vol. 4. 1941. Haskell Curry. "The combinatory foundations of mathematics" Journal of Symbolic Logic. 1942. Haskell Curry. Foundations of Mathematical Logic. McGraw-Hill. 1963. Michael Cusumano and Richard Selby, R. Microsoft Secrets: How the World's Most Powerful Software Company Creates Technology, Shapes Markets, and Manages People. Free Press. 1995 Newton da Costa Inconsistent Formal Systems (Sistemas Formais Inconsistentes in Portuguese) Doctoral dissertation. University of Paraná. 1963. Newton da Costa. "On the Theory of Inconsistent Formal Systems" Notre Dame Journal of Formal Logic October 1974. Ole-Johan Dahl and Kristen Nygaard. "Class and subclass declarations" IFIP TC2 Conference on Simulation Programming Languages. May 1967. Ole-Johan Dahl and Tony Hoare. Hierarchical Program Structures in "Structured Programming" Prentice Hall. 1972. Carlos Damásio and Luís Pereira. "A Model Theory for Paraconsistent Logic Programming" Portuguese Conference on Artificial Intelligence 1995. Giacomo Mauro D'Ariano and Alessandro Tosini. "Space-time and special relativity from causal networks" ArXiv. 1008.4805. August 2010. Julian Davies. "Popler 1.5 Reference Manual" University of Edinburgh, TPU Report No. 1, May 1973. Ernest Davis. "The Naïve Physics Perplex" AI Magazine. Winter 1998. Ernest Davis and Leora Morgenstern. "A First-Order Theory of Communication and Multi-Agent Plans" Journal of Logic and Computation, Vol. 15, No. 5, 2005. John Dawson Logical Dilemmas. The Life and Work of Kurt Gödel AK Peters. 1997 John Dawson. "What Hath Gödel Wrought?" Synthese. Jan. 1998. John Dawson. "Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science" FLOC'06. Walter Dean and Hdenori Kurokawa. "Knowledge, proof, and the Knower" TARK'09, John Kenneth Galbraith. Economics, Peace and Laughter. New American Library. 1971. Robin Gandy. "Church's Thesis and Principles of Mechanisms" The Kleene Symposium North-Holland. 1980. John Gay. "The Elephant and the Bookseller" Fifty-one Fables in Verse 1727 Michael Gelfond and Vladimir Lifschitz. "Logic programs with classical negation" International Conference on Logic Programming. MIT Press. 1990. Gerhard Gentzen. "Provability and nonprovability of restricted transfinite induction in elementary number theory" (Collected Papers of Gerhard Gentzen. North-Holland. 1969) Habilitation thesis. Göttingen. 1942. Gerhard Gentzen (1935) "Investigations into Logical Deduction." (Collected Papers of Gerhard Gentzen. North-Holland. 1969) Steve Gerrard "Wittgenstein's Philosophies of Mathematics" Synthese 87. 1991. Elizabeth Gibney. "Go players react to computer defeat" Nature News. January 27, 2016. Matt Ginsberg. "AI and nonmonotonic reasoning" in Handbook of Logic in Artificial Intelligence and Logic Programming Clarendon Press. 1994. Jean-Yves Girard. The Blind Spot: Lectures on proof-theory Roma Tre. 2004. Andreas Glausch and Wolfgang Reisig. Distributed Abstract State Machines and Their Expressive Power Informatik-Berichete 196. Humboldt University of Berlin. January 2006. Kurt Gödel (1930) "The completeness of the axioms of the functional calculus of logic" (translated in A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press. 1967) Kurt Gödel (1931) "On formally undecidable propositions of Principia Mathematica" in A Source Book in Mathematical Logic, 1879-1931. Translated by Jean van Heijenoort. Harvard Univ. Press. 1967. Kurt Gödel (1933) "An Interpretation of the Intuitionistic Propositional Calculus," in Collected Works of Kurt Gödel, Oxford University Press, Volume 3, 1995, pp. 296-302. Kurt Gödel (1944) "Russell's Mathematical Logic" in Philosophy of Mathematics(2 nd ed.) Cambridge University Press. Kurt Gödel (1951) "Some basic theorems on the foundations of mathematics and their implications" in Collected Works of Kurt Gödel, Oxford University Press, Volume 3, 1995. Kurt Gödel (1965) "On Undecidable Propositions of Formal Mathematical Systems" (a copy of Gödel's 1931 paper with his corrections of errata and added notes) in The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable problems and Computable Functions Martin Davis editor. Raven Press 1965. Kurt Gödel (1972), "Some Remarks on the Undecidability Results" in Kurt Gödel Collected Works, II. Oxford University Press. 2001. 59 Dina Goldin and Peter Wegner. "The Interactive Nature of Computing: Refuting the Strong Church-Turing Thesis" Minds and Machines March 2008. Solomon Golomb and Leonard Baumert. (1965) "Backtrack Programming" JACM. Vol. 12 No. 4. Thomas Gordon. Foundations of Argumentation Technology: Summary of Habilitation Thesis Technische Universität Berlin. 2009. C. Cordell Green: "Application of Theorem Proving to Problem Solving" IJCAI 1969. Steve Gregory. "Concurrent Logic Programming Before ICOT: A Personal Perspective" August 15, 2007. http://www.cs.bris.ac.uk/~steve/papers/ALP/CLPbeforeICOT.pdf Irene Greif. Semantics of Communicating Parallel Processes MIT EECS Doctoral Dissertation. August 1975 Ramanathan Guha. Contexts: Formalization and Some Applications PhD thesis. Stanford University. 1991. Robert Hadley. "Consistency, Turing Computablity and Gödel's First Incompleteness Theorem" Minds and Machines 18. 2008. Volker Halbach "Axiomatic theories of truth" Stanford Encyclopedia of Philosophy. 2007. Ronald Harrop. "Some structure results for propositional calculi" Journal of Symbolic Logic, 30. 1965. W. D. Hart. "Skolem Redux" Notre Dame Journal of. Formal Logic. 41, no. 4. 2000. Donna Haraway. "Situated Knowledge: the Science Question in Feminism and the Privilege of Partial Perspective" in Simians, Cyborgs, and Women: the Reinvention of Nature. Free Association Books. 1991. Pat Hayes. "Computation and Deduction" Mathematical Foundations of Computer Science: Proceedings of Symposium and Summer School, Štrbské Pleso, High Tatras, Czechoslovakia. September 1973. Pat Hayes "Some Problems and Non-Problems in Representation Theory" AISB. Sussex. July, 1974. Pat Hayes. "The Naïve Physics Manifesto". Expert Systems in the Microelectronic Age. Edinburgh University Pres. 1979. Pat Hayes. 1985a. "The Second Naïve Physics Manifesto" Formal Theories of the Commonsense World. Ablex. 1985. Pat Hayes. 1985b. "Naïve Physics 1: Ontology for Liquids" Formal Theories of the Commonsense World. Ablex. 1985. Pat Hayes. "Contexts in context." Contexts in Knowledge Representation and Natural Language. AAAI. 1997. Pat Hayes. "Context Mereology." Commonsense 2007. Jean van Heijenoort (1967) From Frege to Gödel. A Source Book in Mathematical Logic, 1897-1931, Harvard University Press. Joseph Heller. Catch-22. Simon & Schuster.1961. 60 Leon Henkin "A Problem Concerning Provability" Journal of Symbolic Logic, Vol. 17 (1952). Carl Hewitt. "Planner: A Language for Proving Theorems in Robots" IJCAI 1969. Carl Hewitt. "Procedural Embedding of Knowledge In Planner" IJCAI 1971. Carl Hewitt, Peter Bishop and Richard Steiger. "A Universal Modular Actor Formalism for Artificial Intelligence" IJCAI 1973. Carl Hewitt and Henry Baker Laws for Communicating Parallel Processes IFIP. August 1977. Carl Hewitt. "Viewing Control Structures as Patterns of Passing Messages" Journal of Artificial Intelligence. June 1977. Carl Hewitt and Peter de Jong. "Open Systems"' Perspectives on Conceptual Modeling, Brodie, Mylopoulos, and Schmidt (eds.), Springer-Verlag, 1983. Carl Hewitt. "The Challenge of Open Systems" Byte Magazine. April 1985. Carl Hewitt (1986). "Offices Are Open Systems" ACM Transactions on Information Systems 4(3) Carl Hewitt (1990). "Towards Open Information Systems Semantics" International Workshop on Distributed Artificial Intelligence Carl Hewitt (1991). "Open Information Systems Semantics" Journal of Artificial Intelligence. January 1991. Carl Hewitt and Jeff Inman. "DAI Betwixt and Between: From 'Intelligent Agents' to Open Systems Science" IEEE Transactions on Systems, Man, and Cybernetics. Nov. /Dec. 1991. Carl Hewitt and Gul Agha. "Guarded Horn clause languages: are they deductive and Logical?" International Conference on Fifth Generation Computer Systems. Ohmsha 1988. Carl Hewitt. (2006). "What is Commitment? Physical, Organizational, and Social" COIN@AAMAS'06. (Revised version to be published in Springer Verlag Lecture Notes in Artificial Intelligence. Edited by Javier Vázquez-Salceda and Pablo Noriega. 2007) April 2006. Carl Hewitt (2007a). "Organizational Computing Requires Unstratified Paraconsistency and Reflection" COIN@AAMAS. 2007. Carl Hewitt (2008a) "A historical perspective on developing foundations for privacy-friendly client cloud computing: iConsult TM & iEntertain TM Apps using Istlet TM Information Integration for CyberOrgs TM Information Systems" (Revised version of "Development of Logic Programming: What went wrong, What was done about it, and What it might mean for the future" in Proceedings of What Went Wrong and Why edited by Mehmet Gőker and Daniel Shapiro, AAAI Press. 2008 pp. 1-11) ArXiv. 0901.4934 Carl Hewitt (2008b). "Norms and Commitment for CyberOrgs TM Information Systems: Direct Logic TM and Participatory Grounding Checking" ArXiv 0906.2756 Carl Hewitt (2008c) "Large-scale Organizational Computing requires Unstratified Reflection and Strong Paraconsistency" Coordination, 61 Organizations, Institutions, and Norms in Agent Systems III Jaime Sichman, Pablo Noriega, Julian Padget and Sascha Ossowski (ed.). Springer-Verlag. http://organizational.carlhewitt.info/ Carl Hewitt (2008d) "Middle History of Logic Programming: Resolution, Planner, Edinburgh Logic for Computable Functions, Prolog and the Japanese Fifth Generation Project" ArXiv 0904.3036 Carl Hewitt (2008e). ORGs for Scalable, Robust, Privacy-Friendly Client Cloud Computing IEEE Internet Computing September/October 2008. Carl Hewitt (2009a) Perfect Disruption: The Paradigm Shift from Mental Agents to ORGs IEEE Internet Computing. Jan/Feb 2009. Carl Hewitt (2010a) ActorScript™ extension of C# ® , Java ® , and Objective C ® : iAdaptive TM concurrency for antiCloud TM privacy-friendly computing in Inconsistency Robustness. College Publications. 2015. Carl Hewitt (2010b) "Actor Model of Computation: Scalable Robust Information Systems" in Inconsistency Robustness. College Publications. 2015. Carl Hewitt (2010c) Wittgenstein versus Gödel on the Foundations of Logic Stanford Media X Logic Colloquium video recording. April 23, 2010. Carl Hewitt. Looming private information fiasco versus the new cloud business model: The next generation will ask, "Where were you when this was going down?" Risks Digest. Vol. 26: Issue 37. March 9. 2011. Carl Hewitt (editor). Inconsistency Robustness 1011 Stanford University. 2011. Carl Hewitt. What is computation? Actor Model versus Turing's Model in "A Computable Universe: Understanding Computation & Exploring Nature as Computation" Edited by Hector Zenil. World Scientific Publishing Company. 2012. David Hilbert. 1900. in "Mathematical Developments Arising From Hilbert Problems" Proceedings of Symposia in Pure Mathematics, Vol. 28. American Mathematical Society. 1976 David Hilbert (1926) "Über das Unendliche" Mathematische Annalen, 95: 161-90. ("On the Infinite" English translation in van Heijenoort. 1967). David Hilbert and Paul Bernays. Grundlagen der Mathematik I. (L'Harmattan edition 2001) 1934. David Hilbert and Paul Bernays. Grundlagen der Mathematik II. (L'Harmattan edition 2001) 1939. Tony Hoare. "Communicating Sequential Processes" CACM August, 1978. Tony Hoare. Communicating Sequential Processes. Prentice Hall. 1985. Tony Hoare. "The verifying compiler: A grand challenge for computing research" JACM. January 2003. Tony Hoare. Retrospective: An Axiomatic Basis for Computer Programming CACM 2009. Wilfrid Hodges (2006) "Tarski's Truth Definitions" Stanford Encyclopedia of Philosophy. Thomas Kuhn. The Structure of Scientific Revolutions University of Chicago Press. 1962. Ernest Kurtz and Katherine Ketcham. The Spirituality of Imperfection: Storytelling and the Search for Meaning Bantam 1993. Henry Kyburg and Choh Teng. Uncertain Inference Cambridge University Press. 2001 Imre Lakatos. "A renaissance of empiricism in the recent philosophy of mathematics?" Mathematics, Science and Epistemology. 1978. Imre Lakatos. Proofs and Refutations Cambridge University Press. 1976 Imre Lakatos. Mathematics, Science and Epistemology edited by J. Worrall and G. Currie. Cambridge University Press. 1978. Hélène Landemore. " 'Talking it Out': Deliberation with Others Versus Deliberation Within" Political Psychology. forthcoming 2011. Peter Landin. "A Generalization of Jumps and Labels" UNIVAC Systems Programming Research Report. August 1965. (Reprinted in Higher Order and Symbolic Computation. 1998) Bruno Latour Science in Action: How to Follow Scientists and Engineers Through Society Harvard University Press. 1987. Bruno Latour. (2010a) The Making of Law Polity Press. 2010. Bruno Latour. (2010b) On the Modern Cult of the Factish Gods Duke University Press. 2010. John Law. After Method: mess in social science research Routledge. 2004. Federico Laudisa and Carlo Rovelli. "Relational Quantum Mechanics" Stanford Encyclopedia of Philosophy 2008. Hannes Leitgeb. "What theories of truth should be like (but cannot be)" Philosophy Compass 2 (2). 2007. Doug Lenat "CYC: Lessons Learned in Large-Scale Ontological Engineering" November 17, 2005. Isaac Levi. Direct Inference Journal of Philosophy. Jan. 1977. Steven Levy Hackers: Heroes of the Computer Revolution Doubleday. 1984. Clarence Lewis and Cooper Langford. Symbolic Logic Century-Croft, 1932. David Lewis. "Probabilities of Conditionals, and Conditional Probabilities" Philosophical Review.1976. Philip Lewis. "Jonathon von Neumann and EDVAC" Nov. 8. 2004. www.cs.berkeley.edu/~christos/classics/paper.pdf Henry Lieberman. "A Preview of Act 1" MIT AI memo 625. June 1981. James Lighthill. "Artificial Intelligence: A General Survey" Artificial Intelligence: a paper symposium. UK Science Research Council. 1973 Martin Löb. "Solution of a problem of Leon Henkin." Journal of Symbolic Logic. Vol. 20. 1955. Per Martin-Löf. "Verificationism then and now" The Foundational Debate. Kluwer. 1995. Van McGee. "Counterexample to Modus Ponens" The Journal of Philosophy 82. 1985. 65 Eckart Menzler-Trott. Logic's Lost Genius: The Life of Gerhard Gentzen American Mathematical Society. 2007. Donald Loveland. Report of a Workshop on the Future Directions of Automated Deduction NSF 1997. http://www.cs.duke.edu/AutoDedFD/report/ Leopold Löwenheim (1915) "Über Möglichkeiten im Relativkalkül" Mathematische Annalen 76. (Translated as "On possibilities in the calculus of relatives" in Jean van Heijenoort, 1967. From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press) Michael Lynch The Nature of Truth MIT Press. 2001. Donald MacKenzie. Mechanizing Proof. MIT Press. 2001. Edwin Mares. "Relevance Logic" Stanford Encyclopedia of Philosophy. Jan. 2006. Roger Maddux Relevance Logic and the calculus of relations International Conference on. Order, Algebra and Logics. Vanderbilt. 2007. Frederick Maier, Yu Ma, and Pascal Hitzler. "Paraconsistent OWL and Related Logics" Semantic Web Journal. 2011. David Malone. Dangerous Knowledge BBC4 documentary. 2007. http://www.dailymotion.com/playlist/x1cbyd_xSilverPhinx_bbcdangerous-knowledge/1 Edwin Mares. Relevant Logic Cambridge University Press. 2007 Per Martin-Löf. "Verificationism then and now" in W. De Pauli-Schimanovich, et al., eds. The Foundational Debate Kluwer. 1995. John McCarthy. "Programs with common sense" Symposium on Mechanization of Thought Processes. National Physical Laboratory. Teddington, England. 1958. John McCarthy. "Situations, actions and causal laws" Stanford Artificial Intelligence Project: Memo 2. 1963 John McCarthy and Pat Hayes. "Some Philosophical Problems from the Standpoint of Artificial Intelligence" Machine Intelligence 4. 1969 John McCarthy, Paul Abrahams, Daniel Edwards, Timothy Hart, and Michael Levin. Lisp 1.5 Programmer's Manual MIT Computation Center and Research Laboratory of Electronics. 1962. John McCarthy. "Review of 'Artificial Intelligence: A General Survey" Artificial Intelligence: a paper symposium. UK Science Research Council. 1973. John McCarthy. "Circumscription-a form of nonmonotonic reasoning." Artificial Intelligence. 1980. John McCarthy. "Applications of circumscription to formalizing common sense knowledge" Artificial Intelligence. 1986. John McCarthy. "Generality in Artificial Intelligence" CACM. December 1987. John McCarthy. "A logical AI Approach to Context" Technical note, Stanford Computer Science Department, 1996.

APPENDIX 1: DETAILS OF DIRECT LOGIC

Formalism of Direct Logic

The aims of logic should be the creation of "a unified conceptual apparatus which would supply a common basis for the whole of human knowledge." [START_REF] Tarski | Introduction to Logic[END_REF] In Direct Logic, unrestricted recursion is allowed in programs. For example,  There are uncountably many Actors. 66 For example, Real∎[ ] can output any real number i between 0 and 1 where

Real∎[ ] ≡ [(0 either 1), ⩛Postpone Real∎[ ]]

where o (0 either 1) is the nondeterministic choice of 0 or 1, o [ first, ⩛rest] is the list that begins with first and whose remainder is rest, and o Postpone expression delays execution of expression until the value is needed.  There are uncountably many propositions (because there is a different proposition for every real number). Consequently, there are propositions that are not the abstraction of any element of a denumerable set of sentences. For example, p ≡ [xℝ]→([yℝ]→(y=x)) defines a different predicate p[x] for each real number x, which holds for only one real number, namely x. ii i using binary representation. ii For example (p[3]) [y] holds if and only if y=3.

Sentences i can be abstracted into propositions that can be asserted. Furthermore, expressions ii can be abstracted into Actors (e.g., objects in mathematics).

i which are grammar tree structures ii In Java and C++, parametrized types are called "generics", "<" is used for , and ">" is used for .

The type of τ thwarts Girard's paradox.

The following axiom holds: τ1:Typeτ2 ⇨ τ1⊑τ2 ii Type of computable procedures from τ1 into τ2.

The following axiom holds: f:([τ1]↦τ2)  x:τ1, ⇨ f ∎[x]:τ2. iii Type of functions from τ1 into τ2.

The following axiom holds: f:τ 2 𝛔 1  x:τ1 ⇨ f[x]:τ2. iv Propositionorder is the parametrized type consisting of type Proposition parametrized by order. v The type of p⟦x⟧ means that the Y fixed point construction cannot be used to construct propositions in Direct Logic.

Grammar (syntax) trees (i.e. expressions and sentences) are defined as follows :

 Expressions, i.e., an Expressionτ is a discrimination of the following:

• Constantτ:TypeConstantτ.

Propositional Substitutions

The following logical equivalences hold: i

Double Negation

Likewise classical bi-implication is denoted by ⇔. Direct Logic has the following usual principles for bi-implication:

Substitution of equivalent propositions:

Inconsistency Robust Inference

Logic merely sanctions the conquests of the intuition. Jacques Hadamard (quoted in [START_REF] Kline | Mathematical thought from ancient to modern times[END_REF])

Inference in theory T (denoted by ├ T ) is characterized by the following axioms: i

Comma: Accumulation:

Transitivity for entailment:

a universally quantified variable of a statement can be instantiated with any expression E (taking care that none of the variables in E are captured). to them it is a matter of indifference if these objects are replaced by others, provided that the relations do not change. Matter does not engage their attention, they are interested by form alone. [START_REF] Poincaré | La grandeur mathematiques et l'experience, La Science et l'Hypothése[END_REF] This appendix presents foundations for mathematics that goes beyond logicism in that it does not attempt to reduce mathematics solely to logic, solely to types, or solely to sets in a way that encompasses all of standard mathematics including the integers, reals, analysis, geometry, etc. 87

Consistency has been the bedrock of mathematics.

Platonic Ideals were to be perfect, unchanging, and eternal. 88 Beginning with the Hellenistic mathematician Euclid [circa 300BC] in Alexandria, theories were intuitively supposed to be consistent. 89 Wilhelm Leibniz, Giuseppe Peano, George Boole, Augustus De Morgan, Richard Dedekind, Gottlob Frege, Charles Peirce, David Hilbert, etc. developed mathematical logic. However, a crisis occurred with the discovery of the logical paradoxes based on self-reference by Burali-Forti [1897], Cantor [1899], [START_REF] Russell | Principles of Mathematics Norton[END_REF], etc. In response [START_REF] Russell | [END_REF] stratified types, [Zermelo 1905, Fränkel 1922, Skolem 1922] stratified sets and [START_REF] Tarski | Arithmetical extensions of relational systems[END_REF] stratified logical theories to limit self-reference. [Church 1935 andlater Turing 1936] proved that closed mathematical theories are inferentially undecidable ii , i.e., there are propositions which can neither be proved nor disproved. However, the bedrock of consistency remained.

This appendix presents Classical Direct Logic.

The following principles are available because ⊢ i is thought to be consistent by an overwhelming consensus of working professional mathematicians:

Inheritance from mathematics

Theorems of mathematics hold in every theory:

Nondeterministic Execution

Direct Logic makes use of the nondeterministic execution as follows:

proposition.

Appendix 3. Historical development of inferential undecidability ("incompleteness")

Truth versus Argumentation [START_REF] Dedekind | What are and what should the numbers be?[END_REF]] made fundamental contributions to the foundations of mathematics with the following theorems:  Natural Numbers: If X be a type satisfying the Dedekind categorical axioms for the natural numbers, then X is isomorphic to ℕ which is more powerful than the cut-down first-order theory of the natural numbers. 91  Reals: If X is a type satisfying the Dedekind categorical axioms for the real numbers, then X≈ℝ, which is strictly more powerful than cut-down first-order theory. 92 The above results categorically characterize the natural numbers (integers) and the real numbers up to isomorphism based on argumentation. There is no way to go beyond argumentation to get at some special added insight called "truth." Argumentation is all that we have.

i with no subscripted inconsistency robust theory, i.e., ⊢ is used for classical mathematics whereas ⊢ T is used for inconsistency-robust inference in theory T.

Classical Proof by Contradiction: (⊢) ⊢  i.e., the negation of a proposition can be inferred from inferring a contradiction Classical Deduction Theorem:

e., a classical implication can be proved by inference

Inadequacy of Tarskian Set Models for Theories of Practice

Standard Tarskian Set Models are inadequate for large information theories of practice because they are pervasively inconsistent and consequently have no models.

Is Provability Direct Logic computationally decidable?

Provability Direct Logic is a subset of Inconsistency Robust Direct Logic for a single theory without quantifiers as follows:

• :Proposition where :Proposition The following logical equivalences hold:

Substitution of equivalent propositions:

The following inferences hold: Allowing the proposition I'm unprovable. [ii] used in the incompleteness results of [Gödel 1931]

Inconsistency-robust Logic Programs

Logic Programs i can logically infer computational steps.

Forward Inference

Forward inference is performed using ⊢ Illustration of forward inference: Church 1932;McCarthy 1963;Hewitt 1969Hewitt , 1971Hewitt , 2010;;[START_REF] Milner | Logic for Computable Functions: description of a machine implementation[END_REF], Hayes 1973;[START_REF] Kowalski | Predicate Logic as Programming Language[END_REF]]. Note that this definition of Logic Programs does not follow the proposal in [START_REF] Kowalski | Predicate Logic as Programming Language[END_REF][Kowalski , 2011] that Logic Programs be restricted only to backward inference, e.g., to the exclusion of forward inference, etc.

(⊢ aTheory PropositionExpression ):Continuation

Assert PropositionExpression for aTheory.

(When ⊢ aTheory PropositionPattern →

Expression ):Continuation

When PropositionPattern holds for aTheory, evaluate Expression.

Backward Inference

Backward inference is performed using ⊩ Illustration of backward inference:

⊢t

⊩t Mortal[Socrates]▮ will result in asserting Mortal[Socrates] for theory t.

SubArguments

This section explains how subarguments i can be implemented in natural deduction.

When ⊩s (psi ⊢t phi) → Let t' ← extension(t), Do ⊢t' psi, ⊩t' phi → ⊢s (psi ⊢t phi))▮

Note that the following hold for t' because it is an extension of t:  When ⊢t theta → ⊢t' theta▮  When ⊩t' theta → ⊩t theta▮ i See appendix on Inconsistency Robust Natural Deduction.

(⊩ aTheory GoalPattern → Expression ):Continuation

Set GoalPattern for Theory and when established evaluate Expression.

(⊩ aTheory GoalPattern ):Expression

Set GoalPattern for Theory and return a list of assertions that satisfy the goal.

(When ⊩ aTheory GoalPattern → Expression ):Continuation

When there is a goal that matches GoalPattern for Theory, evaluate Expression. The following conclusions can be drawn for documentation, use cases, and code of large software systems for human-computer interaction:

Index

 Consistency proofs are impossible for whole systems.

 There are some consistent subtheories but they are typically mathematical. There are some other consistent microtheories as well, but they are small, make simplistic assumptions, and typically are inconsistent with other such microtheories [Addanki, Cremonini and Penberthy 1989]. Nevertheless, the Davis and Morgenstern research programme to prove consistency of microtheories can be valuable for the theories to which it can be applied. Also some of the techniques that they have developed may be able to be used to prove the consistency of the mathematical fragment of Direct Logic and to prove inconsistency robustness (see below in this article). 10 [Vogels 2009] 11 [Wittgenstein 1933[Wittgenstein -1935] ] 12 [Wittgenstein 1933[Wittgenstein -1935] ] Turing differed fundamentally on the question of inconsistency from Wittgenstein when he attended Wittgenstein's seminar on the Foundations of Mathematics [START_REF] Diamond | Wittgenstein's Lectures on the Foundations of Mathematics[END_REF]]: "Wittgenstein:... Think of the case of the Liar. It is very queer in a way that this should have puzzled anyonemuch more extraordinary than you might think... Because the thing works like this: if a man says 'I am lying' we say that it follows that he is not lying, from which it follows that he is lying and so on. Well, so what? You can go on like that until you are black in the face. Why not? It doesn't matter. ...it is just a useless language-game, and why should anyone be excited? Turing: What puzzles one is that one usually uses a contradiction as a criterion for having done something wrong. But in this case one cannot find anything done wrong. Wittgenstein: Yesand more: nothing has been done wrong, ... where will the harm come? Turing: The real harm will not come in unless there is an application, in which a bridge may fall down or something of that sort…. You cannot be confident about applying your calculus until you know that there are no hidden contradictions in it…. Although you do not know that the bridge will fall if there are no contradictions, yet it is almost certain that if there are contradictions it will go wrong somewhere." Wittgenstein followed this up with [Wittgenstein 1956, pp. 104e-106e]: "Can we say: 'Contradiction is harmless if it can be sealed off'? But what prevents us from sealing it off?" McGee [1985] has challenged modus ponens using an example that can be most simply formalized in Direct Logic as follows:

and ├ McGee RepublicanWillWin From the above, in Direct Logic it follows that:

McGee challenged the reasonableness of the above conclusion on the grounds that. intuitively, the proper inference is that if Reagan will not win, then AndersonWillWin because Carter (the Democratic candidate) will win. However, in theory McGee, it is reasonable to infer AndersonWillWin from ReaganWillWin because RepublicanWillWin holds in McGee.

McGee phrased his argument in terms of implication which in Direct Logic (see following discussion in this paper) would be as follows:

However, this makes no essential difference because, in Direct Logic, it still follows that ReaganWillWin ⇒ McGee AndersonWillWin 37 [cf. Church 1934[START_REF] Kleene | General recursive functions and natural numbers[END_REF] 38 Direct inference is defined differently in this paper from probability theory [Levy 1977, Kyburg andTeng 2001], which refers to "direct inference" of frequency in a reference class (the most specific class with suitable frequency knowledge) from which other probabilities are derived.

39 [START_REF] Jaśkowski | On the Rules of Suppositions in Formal Logic[END_REF]] 39 that doesn't require artifices such as indices (labels) on propositions or restrictions on reiteration 104 40 [START_REF] Turing | On computable numbers, with an application to the Entscheidungsproblem[END_REF]] stated:  the behavior of the computer at any moment is determined by the symbols which he [the computer] is observing, and his 'state of mind' at that moment  there is a bound B to the number of symbols or squares which the computer can observe at one moment. If he wishes to observe more, he must use successive observations. Gödel's conception of computation was formally the same as Turing but more reductionist in motivation: There is a major difference between the historical contexts in which Turing and Gödel worked. Turing tackled the Entscheidungsproblem [computational decidability of provability] as an interesting mathematical problem worth solving; he was hardly aware of the fierce foundational debates. Gödel on the other hand, was passionately interested in the foundations of mathematics. Though not a student of Hilbert, his work was nonetheless deeply entrenched in the framework of Hilbert's finitistic program, whose main goal was to provide a meta-theoretic finitary proof of the consistency of a formal system "containing a certain amount of finitary number theory." Shagrir [2006] 41 According to [START_REF] Turing | Intelligent Machinery[END_REF]:

LCMs [Logical Computing Machines: Turing's expression for Turing machines] can do anything that could be described as … "purely mechanical"…This is sufficiently well established that it is now agreed amongst logicians that "calculable by means of an LCM" is the correct accurate rendering [of phrases like "purely mechanical"] 42 [Wang 1974, p. 84] 43 An example of the global state space model is the Abstract State Machine (ASM) model [Blass, Gurevich, Rosenzweig, andRossman 2007a, 2007b;Glausch and Reisig 2006]. 44 This result is very old. It was known by Dijkstra motivating his belief that it is impossible to implement unbounded nondeterminism. Also the result played a crucial role in the invention of the Actor Model in 1972.

Consider the following Nondeterministic Turing Machine:

Step 1: Next do either Step 2 or Step 3.

Step 2: Next do Step 1.

Step 3: Halt.

It is possible that the above program does not halt. It is also possible that the above program halts. Note that above program is not equivalent to the one below in which it is not possible to halt:

Step 1: Next do Step 1.

51 See appendix of this article. 53 Note that this theorem is very different from the result [Kleene 1938], that mathematics can be extended with a proposition asserting its own consistency. 54 A prominent logician referee of this article suggested that if the proof is accepted then consistency should be made an explicit premise of every theorem of mathematics! 55 As shown above, there is a simple proof in Classical Direct Logic that Mathematics (├) is formally consistent. If Classical Direct Logic has a bug, then there might also be a proof that Mathematics is inconsistent. Of course, if a such a bug is found, then it must be repaired. The Classical Direct Logic proof that Mathematics (├) is consistent is very robust. One explanation is that consistency is built in to the very architecture of mathematics because it was designed to be consistent. Consequently, it is not absurd that there is a simple proof of the consistency of Mathematics (├) that does not use all of the machinery of Classical Direct Logic.

In reaction to paradoxes, philosophers developed the dogma of the necessity of strict separation of "object theories" (theories about basic mathematical entities such as numbers) and "meta theories" (theories about theories). This linguistic separation can be very awkward in Computer Science. Consequently, Direct Logic does not have the separation in order that some propositions can be more "directly" expressed. For example, Direct Logic can use ├├Ψ to express that it is provable that P is provable in Mathematics. It turns out in Classical Direct Logic that ├├Ψ holds if and only if ├Ψ holds. By using such expressions, Direct Logic contravenes the philosophical dogma that the proposition ├├Ψ must be expressed using Gödel numbers. 56 for example, [Øgaard 2015] 57 [Nielsen 2014] 58 [Church 1956;Boolos 1975;Corcoran 1973Corcoran , 1980]]  Ordinals are well-ordered: // an application evolves if its operator evolves 1 ⇾ 2 ⇒ F(1) ⇾ F(2)

// an application evolves if its operand evolves

91 For example, there are nondeterministic Turing machines that the theory ℕ proves always halt that cannot be proved to halt in the cut-down first-order theory. 92 Robinson [1961] 114 93 The inferability problem is to computationally decide whether a proposition defined by sentence is inferable. Theorem [Church 1935 followed by [START_REF] Turing | On computable numbers, with an application to the Entscheidungsproblem[END_REF]