Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity

Sentential Calculus with Identity ($$\mathsf {SCI}$$ SCI ) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In $$\mathsf {SCI}$$ SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of $$\mathsf {SCI}$$ SCI -formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for $$\mathsf {SCI}$$ SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for $$\mathsf {SCI}$$ SCI (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.

Quantum logic

The topic of quantum logic was introduced by Birkhoff and von Neumann (1936), who described the formal properties of a certain algebraic system associated with quantum theory. To avoid begging questions, it is convenient to use the term ‘logic’ broadly enough to cover any algebraic system with formal characteristics similar to the standard sentential calculus. In that sense it is uncontroversial that there is a logic of experimental questions (for example, ‘Is the particle in region R?’ or ‘Do the particles have opposite spins?’) associated with any physical system. Having introduced this logic for quantum theory, we may ask how it differs from the standard sentential calculus, the logic for the experimental questions in classical mechanics. The most notable difference is that the distributive laws fail, being replaced by a weaker law known as orthomodularity. All this can be discussed without deciding whether quantum logic is a genuine logic, in the sense of a system of deduction. Putnam argued that quantum logic was indeed a genuine logic, because taking it as such solved various problems, notably that of reconciling the wave-like character of a beam of, say, electrons, as it passes through two slits, with the thesis that the electrons in the beam go through one or other of the two slits. If Putnam’s argument succeeds this would be a remarkable case of the empirical defeat of logical intuitions. Subsequent discussion, however, seems to have undermined his claim.

EXISTENTIAL GRAPHS AS AN INSTRUMENT OF LOGICAL ANALYSIS: PART I. ALPHA

Peirce considered the principal business of logic to be the analysis of reasoning. He argued that the diagrammatic system of Existential Graphs, which he had invented in 1896, carries the logical analysis of reasoning to the furthest point possible. The present paper investigates the analytic virtues of the Alpha part of the system, which corresponds to the sentential calculus. We examine Peirce’s proposal that the relation of illation is the primitive relation of logic and defend the view that this idea constitutes the fundamental motive of philosophy of notation both in algebraic and graphical logic. We explain how in his algebras and graphs Peirce arrived at a unifying notation for logical constants that represent both truth-function and scope. Finally, we show that Shin’s argument for multiple readings of Alpha graphs is circular.

Extending Metacompleteness to Systems with Classical Formulae

In honour of Bob Meyer, the paper extends the use of his concept of metacompleteness to include various classical systems, as much as we are able. To do this for the classical sentential calculus, we add extra axioms so as to treat the variables like constants. Further, we use a one-sorted and a two-sorted approach to add classical sentential constants to the logic DJ of my book, Universal Logic. It is appropriate to use rejection to represent classicality in the one-sorted case. We then extend these methods to the quantified logics, but we use a finite domain of individual constants to do this.

The complexity of the modal predicate logic of “true in every transitive model of ZF”

Robert Solovay [8] investigated the version of the modal sentential calculus one gets by taking “□ϕ” to mean “ϕ is true in every transitive model of Zermelo-Fraenkel set theory (ZF).” Defining an interpretation to be a function * taking formulas of the modal sentential calculus to sentences of the language of set theory that commutes with the Boolean connectives and sets (□ϕ)* equal to the statement that ϕ* is true in every transitive model of ZF, and stipulating that a modal formula ϕ is valid if and only if, for every interpretation *, ϕ* is true in every transitive model of ZF, Solovay obtained a complete and decidable set of axioms.In this paper, we stifle the hope that we might continue Solovay's program by getting an analogous set of axioms for the modal predicate calculus. The set of valid formulas of the modal predicate calculus is not axiomatizable; indeed, it is complete .We also look at a variant notion of validity according to which a formula ϕ counts as valid if and only if, for every interpretation *, ϕ* is true. For this alternative conception of validity, we shall obtain a lower bound of complexity: every set which is in the set of sentences of the language of set theory true in the constructible universe will be 1-reducible to the set of valid modal formulas.

A geometric proof of the completeness of the Łukasiewicz calculus

We give a self-contained geometric proof of the completeness theorem for the infinite-valued sentential calculus of Łukasiewicz.