Ternary Relational Semantics for the Variants of BN4 and E4 which Contain Routley and Meyer's Logic B

Six hopefully interesting variants of the logics BN4 and E4 – which can be considered as the 4-valued logics of the relevant conditional and (relevant) entailment, respectively – were previously developed in the literature. All these systems are related to the family of relevant logics and contain Routley and Meyer's basic logic B, which is well-known to be specifically associated with the ternary relational semantics. The aim of this paper is to develop reduced general Routley-Meyer semantics for them. Strong soundness and completeness theorems are proved for each one of the logics.

Strong Depth Relevance

Relevant logics infamously have the property that they only validate a conditional when some propositional variable is shared between its antecedent and consequent. This property has been strengthened in a variety of ways over the last half-century. Two of the more famous of these strengthenings are the strong variable sharing property and the depth relevance property. In this paper I demonstrate that an appropriate class of relevant logics has a property that might naturally be characterized as the supremum of these two properties. I also show how to use this fact to demonstrate that these logics seem to be constructive in previously unknown ways.

Arithmetic Formulated Relevantly

The purpose of this paper is to formulate first-order Peano arithmetic within the resources of relevant logic, and to demonstrate certain properties of the system thus formulated. Striking among these properties are the facts that (1) it is trivial that relevant arithmetic is absolutely consistent, but (2) classical first-order Peano arithmetic is straightforwardly contained in relevant arithmetic. Under (1), I shall show in particular that 0 = 1 is a non-theorem of relevant arithmetic; this, of course, is exactly the formula whose unprovability was sought in the Hilbert program for proving arithmetic consistent. Under (2), I shall exhibit the requisite translation, drawing some Goedelian conclusions therefrom. Left open, however, is the critical problem whether Ackermann’s rule γ is admissible for theories of relevant arithmetic. The particular system of relevant Peano arithmetic featured in this paper shall be called R♯. Its logical base shall be the system R of relevant implication, taken in its first-order form RQ. Among other Peano arithmetics we shall consider here in particular the systems C♯, J♯, and RM3♯; these are based respectively on the classical logic C, the intuitionistic logic J, and the Sobocinski-Dunn semi-relevant logic RM3. And another feature of the paper will be the presentation of a system of natural deduction for R♯, along lines valid for first-order relevant theories in general. This formulation of R♯ makes it possible to construct relevantly valid arithmetical deductions in an easy and natural way; it is based on, but is in some respects more convenient than, the natural deduction formulations for relevant logics developed by Anderson and Belnap in Entailment.

TRANSLATIONS BETWEEN LINEAR AND TREE NATURAL DEDUCTION SYSTEMS FOR RELEVANT LOGICS

Anderson and Belnap presented indexed Fitch-style natural deduction systems for the relevant logics R, E, and T. This work was extended by Brady to cover a range of relevant logics. In this paper I present indexed tree natural deduction systems for the Anderson–Belnap–Brady systems and show how to translate proofs in one format into proofs in the other, which establishes the adequacy of the tree systems.

Non-Boolean classical relevant logics II: Classicality through truth-constants

This paper gives an account of Anderson and Belnap’s selection criteria for an adequate theory of entailment. The criteria are grouped into three categories: criteria pertaining to modality, those pertaining to relevance, and those related to expressive strength. The leitmotif of both this paper and its prequel is the relevant legitimacy of disjunctive syllogism. Relevant logics are commonly held to be paraconsistent logics. It is shown in this paper, however, that both E and R can be extended to explosive logics which satisfy all of Anderson and Belnap’s selection criteria, provided the truth-constant known as the Ackermann constant is available. One of the selection criteria related to expressive strength is having an “enthymematic” conditional for which a deduction theorem holds. I argue that this allows for a new interpretation of Anderson and Belnap’s take on logical consequence, namely as committing them to pluralism about logical consequence.

Complete decision procedure for the theory of bounded pointer arithmetic based on quantifier instantiation and SMT

The process of developing C programs is quite often prone to errors related to the uses of pointer arithmetic and operations on memory addresses. This promotes a need in developing various tools for automated program verification. One of the techniques frequently employed by those tools is invocation of appropriate decision procedures implemented within existing SMT-solvers. But at the same time both the SMT standard and most existing SMT-solvers lack the relevant logics (combinations of logical theories) for directly and precisely modelling the semantics of pointer operations in C. One of the possible ways to support these logics is to implement them in an SMT solver, but this approach can be time-consuming (as requires modifying the solver’s source code), inflexible (introducing any changes to the theory’s signature or semantics can be unreasonably hard) and limited (every solver has to be supported separately). Another way is to design and implement custom quantifier instantiation strategies. These strategies can be then used to translate formulas in the desired theory combinations to formulas in well-supported decidable logics such as QF_UFLIA. In this paper, we present an instantiation procedure for translating formulas in the theory of bounded pointer arithmetic into the QF_UFLIA logic. We formally proved soundness and completeness of our instantiation procedure in Isabelle/HOL. The paper presents an informal description of this proof of the proposed procedure. The theory of bounded pointer arithmetic itself was formulated based on known errors regarding the correct use of pointer arithmetic operations in industrial code as well as the semantics of these operations specified in the C standard. Similar procedure can also be defined for a practically relevant fragment of the theory of bit vectors (monotone propositional combinations of equalities between bitwise expressions). Our approach is sufficient to obtain efficient decision procedures implemented as Isabelle/HOL proof methods for several decidable logical theories used in C program verification by relying on the existing capabilities of well-known SMT solvers, such as Z3 and proof reconstruction capabilities of the Isabelle/HOL proof assistant.