I apply Kooi and Tamminga's (2012) idea of correspondence analysis for many-valued logics to strong three-valued logic (K3). First, I characterize each possible single entry in the truth-table of a unary or a binary truth-functional operator that could be added to K3 by a basic inference scheme. Second, I define a class of natural deduction systems on the basis of these characterizing basic inference schemes and a natural deduction system for K3. Third, I show that each of the resulting natural (...) deduction systems is sound and complete with respect to its particular semantics. Among other things, I thus obtain a new proof system for Lukasiewicz's three-valued logic. (shrink)

Kleene’s strong three-valued logic extends naturally to a four-valued logic proposed by Belnap. We introduce a guard connective into Belnap’s logic and consider a few of its properties. Then we show that by using it four-valued analogs of Kleene’s weak three-valued logic, and the asymmetric logic of Lisp are also available. We propose an extension of these ideas to the family of distributive bilattices. Finally we show that for bilinear bilattices the extensions do not produce any new equivalences.

In order to fulfil their essential roles as the bearers of truth and the relata of logical relations, propositions must be public and shareable. That requirement has favoured Platonist and other nonmental views of them, despite the well-known problems of Platonism in general. Views that propositions are mental entities have correspondingly fallen out of favour, as they have difficulty in explaining how propositions could have shareable, objective properties. We revive a mentalist view of propositions, inspired by Artificial Intelligence work on (...) perceptual algorithms, which shows how perception causes persistent mental entities with shareable properties that allow them to fulfil the traditional roles of (one core kind of) propositions. The clustering algorithms implemented in perception produce outputs which are (implicit) atomic propositions in different minds. Coordination of them across minds proceeds by game-theoretic processes of communication. The account does not rely on any unexplained notions such as mental content, representation, or correspondence (although those notions are applicable in philosophical analysis of the result). (shrink)

Bilateralists hold that the meanings of the connectives are determined by rules of inference for their use in deductive reasoning with asserted and denied formulas. This paper presents two bilateral connectives comparable to Prior's tonk, for which, unlike for tonk, there are reduction steps for the removal of maximal formulas arising from introducing and eliminating formulas with those connectives as main operators. Adding either of them to bilateral classical logic results in an incoherent system. One way around this problem is (...) to count formulas as maximal that are the conclusion of reductio and major premise of an elimination rule and to require their removability from deductions. The main part of the paper consists in a proof of a normalisation theorem for bilateral logic. The closing sections address philosophical concerns whether the proof provides a satisfactory solution to the problem at hand and confronts bilateralists with the dilemma that a bilateral notion of stability sits uneasily with the core bilateral thesis. (shrink)

This article follows on the introductory article “Direct Logic for Intelligent Applications” [Hewitt 2017a]. Strong Types enable new mathematical theorems to be proved including the Formal Consistency of Mathematics. Also, Strong Types are extremely important in Direct Logic because they block all known paradoxes[Cantini and Bruni 2017]. Blocking known paradoxes makes Direct Logic safer for use in Intelligent Applications by preventing security holes. Inconsistency Robustness is performance of information systems with pervasively inconsistent information. Inconsistency Robustness of the community of professional (...) mathematicians is their performance repeatedly repairing contradictions over the centuries. In the Inconsistency Robustness paradigm, deriving contradictions has been a progressive development and not “game stoppers.” Contradictions can be helpful instead of being something to be “swept under the rug” by denying their existence, which has been repeatedly attempted by authoritarian theoreticians. Such denial has delayed mathematical development. This article reports how considerations of Inconsistency Robustness have recently influenced the foundations of mathematics for Computer Science continuing a tradition developing the sociological basis for foundations. Mathematics here means the common foundation of all classical mathematical theories from Euclid to the mathematics used to prove Fermat's Last [McLarty 2010]. Direct Logic provides categorical axiomatizations of the Natural Numbers, Real Numbers, Ordinal Numbers, Set Theory, and the Lambda Calculus meaning that up a unique isomorphism there is only one model that satisfies the respective axioms. Good evidence for the consistency Classical Direct Logic derives from how it blocks the known paradoxes of classical mathematics. Humans have spent millennia devising paradoxes for classical mathematics. Having a powerful system like Direct Logic is important in computer science because computers must be able to formalize all logical inferences without requiring recourse to human intervention. Any inconsistency in Classical Direct Logic would be a potential security hole because it could be used to cause computer systems to adopt invalid conclusions. After [Church 1934], logicians faced the following dilemma: • 1st order theories cannot be powerful lest they fall into inconsistency because of Church’s Paradox. • 2nd order theories contravene the philosophical doctrine that theorems must be computationally enumerable. The above issues can be addressed by requiring Mathematics to be strongly typed using so that: • Mathematics self proves that it is “open” in the sense that theorems are not computationally enumerable. • Mathematics self proves that it is formally consistent. • Strong mathematical theories for Natural Numbers, Ordinals, Set Theory, the Lambda Calculus, Actors, etc. are inferentially decidable, meaning that every true proposition is provable and every proposition is either provable or disprovable. Furthermore, theorems of these theories are not enumerable by a provably total procedure. (shrink)