Search

We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to Łukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of Łukasiewicz ’s problem was automatically discovered that is much shorter than any proof found before by man or machine. [ABSTRACT FROM AUTHOR]

Shramko [(2016). Truth, falsehood, information and beyond: The American plan generalized. In K. Bimbo (Ed.), J. Michael Dunn on information based logics, outstanding contributions to logic (pp. 191–212). Dordrecht: Springer] formulated multilattice logic and the algebraic completeness theorem for it. However, the proof has not been presented. In this paper, we consider Kamide and Shramko's multilattice logic M L n [Kamide & Shramko (2017a). Embedding from multilattice logic into classical logic and vice versa. Journal of Logic and Computation, 27(5), 1549–1575] which is an extension of Shramko's original multilattice logic by several implications and coimplications. Using the technique of algebraic embedding, we show that Kamide and Shramko's sequent calculus for multilattice logic M L n is sound and complete with respect to multilattices. Moreover, we introduce yet another algebraic semantics for this logic based on the notion of a De Morgan multilattice. Using Lindenbaum-Tarski algebras, we show that M L n is sound and complete with respect to De Morgan multilattices. Besides, we modify Kamide and Shramko's notion of modal multilattice [Kamide & Shramko (2017b). Modal multilattice logic. Logica Universalis, 11(3), 317–343], i.e. we present the concept of De Morgan modal multilattice. We prove that Kamide and Shramko's modal multilattice logic (Kamide & Shramko, 2017b) is adequate with respect to De Morgan modal multilattices. [ABSTRACT FROM AUTHOR]

In this paper, we introduce the notions of connexive and bi-intuitionistic multilattices and develop on their base the algebraic semantics for Kamide, Shramko, and Wansing's connexive and bi-intuitionistic multilattice logics which were previously known in the form of sequent calculi and Kripke semantics. We prove that these logics are sound and complete with respect to the presented algebraic structures. [ABSTRACT FROM AUTHOR]

This is the culmination of a discussion on Berry's Paradox with Graham Priest, over an extended period from 1983 to 2019, the central point being whether the Paradox can be avoided or not by removal of the Law of Excluded Middle (LEM). Priest is of the view that a form of the Paradox can be derived without the LEM, whilst Brady disputes this. We start by conceptualizing negation in the logic MC of meaning containment and introduce the LEM as part of the classical recapture. We then examine the usage of the LEM in some other paradoxes and see that it is applied to cases of self-reference. In relation to Priest's [2019] paper, we go on to find a similar use of the LEM in Priest's derivation of Berry's Paradox. However, it is found to be deeper and trickier than other paradoxes, requiring a special effort to untangle the relationships between the LEM, self-reference and meta-theoretic influence. We then examine Brady's previous formalization of Berry's Paradox, considering Brady's most recent view of restricted quantification and his recursive account of the least number satisfying a property. We show that neither of these methods can be used to formalize the paradox. [ABSTRACT FROM AUTHOR]

H. Omori and H. Wansing introduced in a recent paper possible alternatives for the negation of the logic of first-degree entailment. One of their observations with regard to these alternative negations is that some of them turn out to induce negation inconsistency, meaning that some contradictions become provable (under an arbitrary premise) when used in place of the original negation. Omori and Wansing also considered a non-deterministic generalisation of such operators, but it was left open whether the generalised negation similarly induces negation inconsistency. In this paper, we provide an answer to this question in the positive, and moreover look into further generalisation and characterisation of non-deterministic operators which satisfy the formal criteria of negation inconsistency and its pair notion of negation incompleteness in the setting of Omori and Wansing. [ABSTRACT FROM AUTHOR]

In 1944 Hans Reichenbach developed a three-valued propositional logic (RQML) in order to account for certain causal anomalies in quantum mechanics. In this logic, the truth-value indeterminate is assigned to those statements describing physical phenomena that cannot be understood in causal terms. However, Reichenbach did not develop a deductive calculus for this logic. The aim of this paper is to develop such a calculus by means of First Degree Entailment logic (FDE) and to prove it sound and complete with respect to RQML semantics. In Section 1 we explain the main physical and philosophical motivations of RQML. Next, in Sections 2 and 3, respectively, we present RQML and FDE syntax and semantics and explain the relation between both logics. Section 4 introduces Q calculus, an FDE-based tableaux calculus for RQML. In Section 5 we prove that Q calculus is sound and complete with respect to RQML three-valued semantics. Finally, in Section 6 we consider some of the main advantages of Q calculus and we apply it to Reichenbach's analysis of causal anomalies. [ABSTRACT FROM AUTHOR]

We develop a common semantic framework for the interpretation both of IPC , the intuitionistic propositional calculus, and of logics weaker than IPC (substructural and subintuitionistic logics). To this end, we prove a choice-free representation and duality theorem for implicative lattices, which may or may not be distributive. The duality specializes to a choice-free duality for the full subcategory of Heyting algebras and a category of topological sorted frames with a ternary sorted relation. [ABSTRACT FROM AUTHOR]

In this article, we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalize the residuated frames in Reference [34] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LE-logics in full uniformity. We prove semantic cut elimination for the display calculi \(\mathrm{D.LE}\) associated with the basic normal LE-logics and their axiomatic extensions with analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus \(\mathrm{D.LE}\) , as well as for its extensions with analytic structural rules satisfying certain additional properties. [ABSTRACT FROM AUTHOR]

Reasoning with quantifier expressions in natural language combines logical and arithmetical features, transcending strict divides between qualitative and quantitative. Our topic is this cooperation of styles as it occurs in common linguistic usage and its extension into the broader practice of natural language plus 'grassroots mathematics'. We begin with a brief review of $\mathsf {FO}(\#)$ , first-order logic with counting operators and cardinality comparisons. This system is known to be of very high complexity, and drowns out finer aspects of the combination of logic and counting. We therefore move to a small fragment that can represent numerical syllogisms and basic reasoning about comparative size: monadic first-order logic with counting, $\mathsf {MFO}(\#)$. We provide normal forms that allow for axiomatization, determine which arithmetical notions can be defined on finite and on infinite models, and conversely, we discuss which logical notions can be defined out of purely arithmetical ones, and what sort of (non-)classical logics can be induced. Next, we investigate a series of strengthenings of $\mathsf {MFO}(\#)$ , again using normal form methods. The monadic second-order version is close, in a precise sense, to additive Presburger Arithmetic, while versions with the natural device of tuple counting take us to Diophantine equations, making the logic undecidable. We also define a system $\mathsf {ML}(\#)$ that combines basic modal logic over binary accessibility relations with counting, needed to formulate ubiquitous reasoning patterns such as the Pigeonhole Principle. We prove decidability of $\mathsf {ML}(\#)$ , and provide a new kind of bisimulation matching the expressive power of the language. As a complement to the fragment approach pursued here, we also discuss two other ways of lowering the complexity of $\mathsf {FO}(\#)$ by changing the semantics of counting in natural ways. A first approach replaces cardinalities by abstract but well-motivated values of 'mass' or other mereological aggregating notions. A second approach keeps the cardinalities but generalizes the meaning of counting to work in models that allow dependencies between variables. Finally, we return to our starting point in natural language, confronting the architecture of our formal systems with linguistic quantifier vocabulary and syntax, as well as with natural reasoning modules such as the monotonicity calculus. In addition to these encounters with formal semantics, we discuss the role of counting in semantic evaluation procedures for quantifier expressions and determine, for instance, which binary quantifiers are computable by finite 'semantic automata'. We conclude with some general thoughts on yet further entanglements of logic and counting in formal systems, on rethinking the qualitative/quantitative divide, and on connecting our analysis to empirical findings in cognitive science. [ABSTRACT FROM AUTHOR]

We present a new frame semantics for positive relevant and substructural propositional logics. This frame semantics is both a generalisation of Routley–Meyer ternary frames and a simplification of them. The key innovation of this semantics is the use of a single accessibility relation to relate collections of points to points. Different logics are modeled by varying the kinds of collections used: they can be sets, multisets, lists or trees. We show that collection frames on trees are sound and complete for the basic positive distributive substructural logic $\mathsf {B}^+$ , that collection frames on multisets are sound and complete for $\mathsf {RW}^+$ (the relevant logic $\mathsf {R}^+$ , without contraction, or equivalently, positive multiplicative and additive linear logic with distribution for the additive connectives), and that collection frames on sets are sound for the positive relevant logic $\mathsf {R}^+$. The completeness of set frames for $\mathsf {R}^+$ is, currently, an open question. [ABSTRACT FROM AUTHOR]

N. Kamide introduced a pair of classical and constructive logics, each with a peculiar type of negation: its double negation behaves as classical and intuitionistic negation, respectively. A consequence of this is that the systems prove contradictions but are non-trivial. The present paper aims at giving insights into this phenomenon by investigating subsystems of Kamide's logics, with a focus on a system in which the double negation behaves as the negation of minimal logic. We establish the negation inconsistency of the system and embeddability of contradictions from other systems. In addition, we attempt at an informational interpretation of the negation using the dimathematical framework of H. Wansing. [ABSTRACT FROM AUTHOR]

The degrees of belief of rational agents should be guided by the evidence available to them. This paper takes as a starting point the view—argued elsewhere—that the formal model best able to capture this idea is one that represents degrees of belief using Dempster–Shafer belief functions. However, degrees of belief should not only respect evidence; they also guide decision and action. Whatever formal model of degrees of belief we adopt, we need a decision theory that works with it: that takes as input degrees of belief so represented. The task of this paper is to develop such a decision theory for the belief function model of degrees of belief. This is not the first paper to attempt that task, but compared to the existing literature it takes a more abstract route to its destination, via a consideration of the very idea of rational decision making in light of one's beliefs and desires. After presenting the new decision theory and comparing it to existing views, the paper goes on to consider diachronic decision situations. [ABSTRACT FROM AUTHOR]

This paper reformulates and decides a certain conjecture in Dunn's 'Relevant Predication 1: The Formal Theory' ( Journal of Philosophical Logic 16, 347-381, 1987). This conjecture of Dunn's relates his object-language characterisation of a property's being relevant in a variable x to certain grammatical characterisations of relevance, analogous to some given by Helman, in 'Relevant Implication and Relevant Functions' (to appear in Entailment: The Logic of Relevance and Necessity, vol. 2, by Alan Ross Anderson, Nuel Belnap, and J. Michael Dunn et al.) In the course of the investigation this paper also investigates Kit Fine's semantics for quantified relevance logics, which appears in his appropriately titled 'Semantics for Quantified Relevance Logics' [ABSTRACT FROM AUTHOR]

This paper will develop ideas from [ 44 ]. We will generalize their work in two directions. First, we provide axioms for justification logics over the base logic B and show that the logic permits a proof of the internalization theorem. Second, we provide alternative frames that more closely resemble the standard versions of the ternary relational frames, as well as a more general approach to the completeness proof. We prove that soundness and completeness hold for justification logics over a wide variety of base logics. Finally, we will strengthen Belnap's variable sharing for the justification logic context, demonstrating that the justifications are properly relevant justifications. [ABSTRACT FROM AUTHOR]

I introduce a novel and quite intuitive interpretation of the ternary relation that figures in the relational semantics of many relevance logics. Conceptually, my interpretation makes use only of incompatibility and parthood relations, defined over a set of states. In this way, the proposed interpretation—of the ternary relation and the conditional—extends Dunn's and Restall's works on negation and the Routley star operator. Therefore, the interpretation is unified, and hence not only intuitive but also parsimonious. Additionally, the interpretation provides us with a cogent argument to the effect that a ternary relation is indispensable, and we cannot merely do with a binary relation. [ABSTRACT FROM AUTHOR]

In the paper, we introduce multilattice versions of the basic congruent and monotonic modal logics. In the case of congruent and monotonic ones, we also study their extensions by Gödel's rule. We formulate these logics in the form of sequent calculi and prove syntactic embedding theorems (as a consequence, we obtain cut admissibility and decidability). Then we present them algebraically and semantically: via modal multilattices and via general and descriptive neighbourhood frames. We show the dual equivalency of the categories of modal multilattices and descriptive neighbourhood frames. Using Lindenbaum–Tarski algebras, we prove that the sequent calculi under consideration are sound and complete with respect to modal multilattices. [ABSTRACT FROM AUTHOR]

This paper is concerned with knowledge graph embedding with background knowledge, taking the formal perspective of logics. In knowledge graph embedding, knowledge--expressed as a set of triples of the form (a R b) ("a is R-related to b")--is embedded into a real-valued vector space. The embedding helps exploiting geometrical regularities of the space in order to tackle typical inductive tasks of machine learning such as link prediction. Recent embedding approaches also consider incorporating background knowledge, in which the intended meanings of the symbols a, R, b are further constrained via axioms of a theory. Of particular interest are theories expressed in a formal language with a neat semantics and a good balance between expressivity and feasibility. In that case, the knowledge graph together with the background can be considered to be an ontology. This paper develops a cone-based theory for embedding in order to advance the expressivity of the ontology: it works (at least) with ontologies expressed in the description logic ALC, which comprises restricted existential and universal quantifiers, as well as concept negation and concept disjunction. In order to align the classical Tarskian Style semantics for ALC with the sub-symbolic representation of triples, we use the notion of a geometric model of an ALC ontology and show, as one of our main results, that an ALC ontology is satisfiable in the classical sense iff it is satisfiable by a geometric model based on cones. The geometric model, if treated as a partial model, can even be chosen to be faithful, i.e., to reflect all and only the knowledge captured by the ontology. We introduce the class of axis-aligned cones and show that modulo simple geometric operations any distributive logic (such as ALC) interpreted over cones employs this class of cones. Cones are also attractive from a machine learning perspective on knowledge graph embeddings since they give rise to applying conic optimization techniques. [ABSTRACT FROM AUTHOR]