The paper is concerned with the psychological relevance of a logical model for deductive reasoning. We propose a new way to analyze logical reasoning in a deductive version of the Mastermind game implemented within a popular Dutch online educational learning system (Math Garden). Our main goal is to derive predictions about the difficulty of Deductive Mastermind tasks. By means of a logical analysis we derive the number of steps needed for solving these tasks (a proxy for working memory load). Our (...) model is based on the analytic tableaux method, known from proof theory. We associate the difficulty of Deductive Mastermind game-items with the size of the corresponding logical trees obtained by the tableaux method. We derive empirical hypotheses from this model. A large group of students (over 37 thousand children, 5–12 years of age) played the Deductive Mastermind game, which gave empirical difficulty ratings of all 321 game-items. The results show that our logical approach predicts these item ratings well, which supports the psychological relevance of our model. (shrink)

Priest has provided a simple tableau calculus for Chellas's conditional logic Ck. We provide rules which, when added to Priest's system, result in tableau calculi for Chellas's CK and Lewis's VC. Completeness of these tableaux, however, relies on the cut rule.

Tableau formulations are given for the relevance logics E (Entailment), R (Relevant implication) and RM (Mingle). Proofs of equivalence to modus-ponens-based formulations are vialeft-handed Gentzen sequenzen-kalküle. The tableau formulations depend on a detailed analysis of the structure of tableau rules, leading to certain global requirements. Relevance is caught by the requirement that each node must be used; modality is caught by the requirement that only certain rules can cross a barrier. Open problems are discussed.

In this paper we present a new hierarchy of analytical tableaux systems TNDC n, 1≤n<ω, for da Costa's hierarchy of propositional paraconsistent logics Cn, 1≤n<ω. In our tableaux formulation, we introduce da Costa's “ball” operator “o”, the generalized operators “k” and “(k)”, for 1≤k, and the negations “~k”, for k≥1, as primitive operators, differently to what has been done in the literature, where these operators are usually defined operators. We prove a version of Cut Rule for the TNDC (...) n, 1≤n<ω, and also prove that these systems are logically equivalent to the corresponding systems Cn, 1≤n<ω. The systems TNDC n constitute completely automated theorem proving systems for the systems of da Costa's hierarchy Cn, 1≤n<ω. (shrink)

In this paper we give an analytic tableau calculus P L 1 6 for a functionally complete extension of Shramko and Wansing’s logic. The calculus is based on signed formulas and a single set of tableau rules is involved in axiomatising each of the four entailment relations ⊧ t, ⊧ f, ⊧ i, and ⊧ under consideration—the differences only residing in initial assignments of signs to formulas. Proving that two sets of formulas are in one of the first three (...) entailment relations will in general require developing four tableaux, while proving that they are in the ⊧ relation may require six. (shrink)

In this paper we present a new hierarchy of analytical tableaux systems TNDC n, 1≤ntableaux formulation, we introduce da Costa's ?ball? operator ?o?, the generalized operators ?k? and ?(k)?, for 1≤k, and the negations ?~k?, for k≥1, as primitive operators, differently to what has been done in the literature, where these operators are usually defined operators. We prove a version of Cut Rule for the TNDC (...) n, 1≤nshrink)

The method of analytic tableaux is employed in many introductory texts and has also been used quite extensively as a basis for automated theorem proving. In this paper, we discuss the complexity of the system as a method for refuting contradictory sets of clauses, and resolve several open questions. We discuss the three forms of analytic tableaux: clausal tableaux, generalized clausal tableaux, and binary tableaux. We resolve the relative complexity of these three forms (...) of tableaux proofs and also resolve the relative complexity of analytic tableaux versus resolution. We show that there is a quasi-polynomial simulation of tree resolution by analytic tableaux; this simulation is close to optimal, since we give a matching lower bound that is tight to within a polynomial. (shrink)

In this paper we describe an improvement of Smullyan's analytic tableau method for the propositional calculus-Improved Parent Clash Restricted (IPCR) tableau-and show that it is equivalent to SL-resolution in complexity.

This books presents the refereed proceedings of the Fifth International Workshop on Analytic Tableaux and Related Methods, TABLEAUX '96, held in Terrasini near Palermo, Italy, in May 1996. The 18 full revised papers included together with two invited papers present state-of-the-art results in this dynamic area of research. Besides more traditional aspects of tableaux reasoning, the collection also contains several papers dealing with other approaches to automated reasoning. The spectrum of logics dealt with covers several nonclassical (...) logics, including modal, intuitionistic, many-valued, temporal and linear logic. (shrink)

We show that Smullyan's analytic tableaux cannot p-simulate the truth-tables. We identify the cause of this computational breakdown and relate it to an underlying semantic difficulty which is common to the whole tradition originating in Gentzen's sequent calculus, namely the dissonance between cut-free proofs and the Principle of Bivalence. Finally we discuss some ways in which this principle can be built into a tableau-like method without affecting its analytic nature.

In this dissertation we present proof systems for several modal logics. These proof systems are based on analytic (or semantic) tableaux. -/- Modal logics are logics for reasoning about possibility, knowledge, beliefs, preferences, and other modalities. Their semantics are almost always based on Saul Kripke’s possible world semantics. In Kripke semantics, models are represented by relational structures or, equivalently, labeled graphs. Syntactic formulas that express statements about knowledge and other modalities are evaluated in terms of such models. -/- (...) This dissertation focuses on modal logics with dynamic operators for public announcements, belief revision, preference upgrades, and so on. These operators are defined in terms of mathematical operations on Kripke models. Thus, for example, a belief revision operator in the syntax would correspond to a belief revision operation on models. -/- The ‘dynamic’ semantics of dynamic modal logics are a clever way of extending languages without compromising on intuitiveness. We present ‘dynamic’ tableau proof systems for these dynamic semantics, with the express aim to make them conceptually simple, easy to use, modular, and extensible. This we do by reflecting the semantics as closely as possible in the components of our tableau system. For instance, dynamic operations on Kripke models have counterpart dynamic relations between tableaux. -/- Soundness, completeness, and decidability are three of the most important properties that a proof system may have. A proof system is sound if and only if any formula for which a proof exists, is true in every model. A proof system is complete if and only if for any formula that is true in all models, a proof exists. A proof system is decidable if and only if any formula can be proved to be a theorem or not a theorem in a finite number of steps. All proof systems in this dissertation are sound, complete, and decidable. -/- Part of our strategy to create modular tableau systems is to delay concerns over decidability until after soundness and completeness have been established. Decidability is attained through the operations of folding and through operations on ‘tableau cascades’, which are graphs of tableaux. -/- Finally, we provide a proof-of-concept implementation of our dynamic tableau system for public announcement logic in the Clojure programming language. (shrink)

We show how to correct the analytic tableaux system from the paper Olkhovikov and Wansing, 259–279, 2018).

The paper is devoted to an approach to analytic tableaux for propositional logic, but can be successfully extended to other logics. The distinguishing features of the presented approach are:(i) a precise set-theoretical description of tableau method; (ii) a notion of tableau consequence relation is defined without help of a notion of tableau, in our universe of discourse the basic notion is a branch;(iii) we define a tableau as a finite set of some chosen branches which is enough to (...) check; hence, in our approach a tableau is only a way of choosing a minimal set of closed branches;(iv) a choice of tableau can be arbitrary, it means that if one tableau starting with some set of premisses is closed in the defined sense, then every branch in the power set of the set of formulas, that starts with the same set, is closed. (shrink)

In this paper, we present a goal-directed proof procedure for abductive reasoning. This procedure will be compared with Aliseda’s approach based on semantic tableaux. We begin with some comments on Aliseda’s algorithms for computing conjunctive abductions and show that they do not entirely live up to their aims. Next we give a concise account of goal-directed proofs and we show that abductive explanations are a natural spin-off of these proofs. Finally, we show that the goal-directed procedure solves the problems (...) we encountered in Aliseda’s algorithms. (shrink)

his paper presents a unified treatment of the propositional and first-order many-valued logics through the method of tableaux. It is shown that several important results on the proof theory and model theory of those logics can be obtained in a general way. We obtain, in this direction, abstract versions of the completeness theorem, model existence theorem (using a generalization of the classical analytic consistency properties), compactness theorem and Lowenheim-Skolem theorem. The paper is completely self-contained and includes examples of (...) application to particular many-valued formal systems. (shrink)

The purpose of this paper is to develop a class of semantic tableau systems for some counterfactual logics. All in all I will discuss 1024 systems. Possible world semantics is used to interpret our formal languages. Soundness results are obtained for every tableau system and completeness results for a large subclass of these.

It has been maintained by Smullyan that the importance of cut-free proofs does not stem from cut elimination per se but rather from the fact that they satisfy the subformula property. In accordance with such a viewpoint in this paper we introduce analytic cut trees, a system from which cuts cannot be eliminated but satisfying the subformula property. Like tableaux analytic cut trees are a refutation system but unlike tableaux they have a single inference rule and (...) several branch closure rules. The main advantage of analytic cut trees over tableaux is efficiency: while analytic cut trees can simulate tableaux with an increase in complexity by at most a constant factor, tableaux cannot polynomially simulate analytic cut trees. Indeed analytic cut trees are intrinsically more efficient than any cut-free system. (shrink)

The purpose of this paper is to develop a class of semantic tableau systems for some dyadic deontic logics. We will consider 16 different pure dyadic deontic tableau systems and 32 different alethic dyadic deontic tableau systems. Possible world semantics is used to interpret our formal languages. Some relationships between our systems and well known dyadic deontic logics in the literature are pointed out and soundness results are obtained for every tableau system. Completeness results are obtained for all 16 pure (...) dyadic deontic systems and for 16 alethic dyadic deontic systems. (shrink)

William Parry conceived in the early thirties a theory of entail-
ment, the theory of analytic implication, intended to give a formal expression to the idea that the content of the conclusion of a valid argument must be included in the content of its premises. This paper introduces a system of analytic, paraconsistent and quasi-classical propositional logic that does not validate the paradoxes of Parry’s analytic implication. The interpretation of the expressions of this logic will be given in (...) terms of a four-valued semantics,and its proof theory will be provided by a system of signed semantic tableaux that incorporates the techniques developed to improve the efficiency of the tableaux method for many-valued logics.
1. Introduction. (shrink)

Van Lambalgen (1990) proposed a translation from a language containing a generalized quantifierQ into a first-order language enriched with a family of predicatesR i, for every arityi (or an infinitary predicateR) which takesQxg(x, y1,..., yn) to x(R(x, y1,..., y1) (x,y1,...,yn)) (y 1,...,yn are precisely the free variables ofQx). The logic ofQ (without ordinary quantifiers) corresponds therefore to the fragment of first-order logic which contains only specially restricted quantification. We prove that it is decidable using the method of analytic (...) class='Hi'>tableaux. Related results were obtained by Andréka and Németi (1994) using the methods of algebraic logic. (shrink)

Recent years have been blessed with an abundance of logical systems, arising from a multitude of applications. A logic can be characterised in many different ways. Traditionally, a logic is presented via the following three components: 1. an intuitive non-formal motivation, perhaps tie it in to some application area 2. a semantical interpretation 3. a proof theoretical formulation. There are several types of proof theoretical methodologies, Hilbert style, Gentzen style, goal directed style, labelled deductive system style, and so on. The (...) tableau methodology, invented in the 1950s by Beth and Hintikka and later per fected by Smullyan and Fitting, is today one of the most popular, since it appears to bring together the proof-theoretical and the semantical approaches to the pre of a logical system and is also very intuitive. In many universities it is sentation the style first taught to students. Recently interest in tableaux has become more widespread and a community crystallised around the subject. An annual tableaux conference is being held and proceedings are published. The present volume is a Handbook a/Tableaux pre senting to the community a wide coverage of tableaux systems for a variety of logics. It is written by active members of the community and brings the reader up to frontline research. It will be of interest to any formal logician from any area. (shrink)

In their recent paper Bi-facial truth: a case for generalized truth values Zaitsev and Shramko [7] distinguish between an ontological and an epistemic interpretation of classical truth values. By taking the Cartesian product of the two disjoint sets of values thus obtained, they arrive at four generalized truth values and consider two “semi-classical negations” on them. The resulting semantics is used to define three novel logics which are closely related to Belnap’s well-known four valued logic. A syntactic characterization of these (...) logics is left for further work. In this paper, based on our previous work on a functionally complete extension of Belnap’s logic, we present a sound and complete tableau calculus for these logics. It crucially exploits the Cartesian nature of the four values, which is reflected in the fact that each proof consists of two tableaux. The bi-facial notion of truth of Z&S is thus augmented with a bi-facial notion of proof. We also provide translations between the logics for semi-classical negation and classical logic and show that an argument is valid in a logic for semi-classical negation just in case its translation is valid in classical logic. (shrink)

Angell's logic of analytic containment AC has been shown to be characterized by a 9-valued matrix NC by Ferguson, and by a 16-valued matrix by Fine. We show that the former is the image of a surjective homomorphism from the latter, i.e., an epimorphic image. The epimorphism was found with the help of MUltlog, which also provides a tableau calculus for NC extended by quantifiers that generalize conjunction and disjunction.

Our aim is to express in exact terms the old idea of solving problems by pure questioning. We consider the problem of derivability: "Is A derivable from Δ by classical propositional logic?". We develop a calculus of questions E*; a proof (called a Socratic proof) is a sequence of questions ending with a question whose affirmative answer is, in a sense, evident. The calculus is sound and complete with respect to classical propositional logic. A Socratic proof in E* can be (...) transformed into a Gentzen-style proof in some sequent calculi. Next we develop a calculus of questions E**; Socratic proofs in E** can be transformed into analytic tableaux. We show that Socratic proofs can be grounded in Inferential Erotetic Logic. After a slight modification, the analyzed systems can also be viewed as hypersequent calculi. (shrink)

We present a semantic game for Gödel logic and its extensions, where the players’ interaction stepwise reduces arbitrary claims about the relative order of truth degrees of complex formulas to atomic ones. The paper builds on a previously developed game for Gödel logic with projection operator in Fermüller et al., Information processing and management of uncertainty in knowledge-based systems, Springer, Cham, 2020, pp. 257–270). This game is extended to cover Gödel logic with involutive negations and constants, and then lifted to (...) a provability game using the concept of disjunctive strategies. Winning strategies in the provability game, with and without constants and involutive negations, turn out to correspond to analytic proofs in a version of \ :1941–1958, 2010) and in a sequent-of-relations calculus, Automated reasoning with analytic tableaux and related methods, Springer, Berlin, 1999, pp. 36–51) respectively. (shrink)

In this paper we devise non-distributive relatives of Exactly true logic by Pietz and Riveccio and its dual Non-falsity logic by Shramko, Zaitsev and Belikov. We consider two pre-orders which are algebraic counterparts of the ETL’s and NFL’s entailment relations on the de Morgan lattice 4. We generalise these pre-orders and determine which distributive properties that hold on 4 are not forced by either of the pre-orders. We then construct relatives of ETL and NFL but lack such distributive properties. For (...) these logics we also devise a truth table semantics which uses non-distributive lattice M3 as their lattice of truth values. We also provide analytic tableaux systems which work with sequents of the form \. We then prove correctness and completeness results for these proof systems and provide a neat generalisation for non-distributive ETL- and NFL-like logics built over a certain family of non-distributive modular lattices. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Reviewed by:The Logic Pamphlets of Charles Lutwidge Dodgson and Related PiecesIrving H. AnellisFrancine F. Abeles, editor. The Logic Pamphlets of Charles Lutwidge Dodgson and Related Pieces. The Pamphlets of Lewis Carroll, 4. New York-Charlottesville-London: Lewis Carroll Society of North America-University Press of Virginia, 2010. Pp. xx + 271. Cloth, $75.00.Until William Bartley’s rediscovery and reconstruction of Dodgson’s lost Part II of Symbolic Logic, Lewis Carroll’s reputation in logic, when (...) taken seriously, rested upon his few published articles on logical paradoxes and puzzles, while his published books, The Game of Logic and Symbolic Logic, were regarded as suitable perhaps as pedagogical tools, but dismissed otherwise as amusements, on a par with the Alice works. Richard Braithwaite asserted (“Lewis Carroll as Logician”) that “Carroll regarded formal and symbolic logic not as a corpus of systematic knowledge about valid thought nor yet as an art for teaching a person to think correctly.” He suggested that Dodgson used his pseudonym for his popular and whimsical writings, reserving his legal name only for his serious mathematical products. Philosophers practicing linguistic analysis in their assault on nonsense deriving from misuse of language meanwhile developed an interest in Carroll (e.g. George Pitcher, “Wittgenstein, Nonsense, and Lewis Carroll”). Abeles, on the contrary, stresses the seriousness of Dodgson’s pedagogical and popularizing mission (195–99).Bartley’s discovery opened the door for reevaluating Dodgson as a serious logician, and Abeles has been in the forefront of that reevaluation. Her general introduction and introductions to the main divisions of this collection of Carroll’s publications (and additional material from his Nachlass and a handful of publications of others, composed in response to Carroll’s published articles) place his serious logical work and its significance in historical perspective, providing a deeper, more sophisticated view than found in Bartley’s “Editor’s Introduction” to Lewis Carroll’s Symbolic Logic. Abeles also offers brief introductions to the individual entries, which describe their physical characteristics and circumstances of composition.Dodgson aligned with the majority of those British logicians of his day, starting with George Boole, who understood formal logic to be Aristotelian syllogistic, and symbolic logic to be syllogistic logic expressed algebraically. His notational innovation was employing indices to terms so that, independently of the arrangement of terms, propositions could easily be read; thus, “xy0” can be read as “no x are y” or “no y are x” and “x1y0” as “all x are not y” or “no x are y”. In dealing with the classical elimination problem in the class calculus—to determine the maximum information, without duplications, obtainable from a given set of premises—Dodgson in his later work and unpublished letters anticipated several concepts of automated theorem proving.Central to both geometry and to formal logic are the rules of logical inference that establish the validity of arguments and guarantee that conclusions inferred from true [End Page 506] premises are true. The modern analytic tableaux, or tree method, is a fundamental tool in this regard, both for deriving theorems and for determining the validity or invalidity of the proofs for propositional calculus and first-order predicate calculus.Introducing his reconstruction of Part II of Symbolic Logic, Bartley noted that, along with the logic diagrams that Carroll devised, he also devised a tableau method that strongly resembled Beth’s semantic tableaux. Abeles went more deeply and convincingly into that resemblance in her earlier research. Beth’s tableaux, together with Hintikka’s model sets, were the direct ancestors of Smullyan’s analytic tableaux, which in turn are the theoretical basis for the Robinson resolution method that continues to be central to much work in programming logic.Abeles has also shown that the work in Studies in Logic by Charles Peirce and his logic students at Johns Hopkins University served as a source of inspiration for Dodgson. More critically, she demonstrated that Dodgson devised and employed the tree method for carrying out proofs of syllogisms and chains of syllogisms, or soriteses, in Part II of Symbolic Logic (see her “Lewis Carroll’s Method of Trees: Its Origins in Studies in Logic,” Modern Logic 1 [1990]: 25–34). The tree... (shrink)

In this paper we propose a tableaux method for the intermediate syllogistic of Peterson and Thompson by using the algebra of Sommers and Englebretsen. The result is an analytic tableaux method capable of modeling inference in basic, relational, and intermediate syllogistic.

Smullyan wrote his famous book of puzzles before the boom in automated theorem proving and he solved the puzzles by hand. Hence it is interesting to investigate whether all the puzzles can be solved with one method or not. The paper shows how this can be done with analytic tableaux.

Could there be a single logical system that would allow us to work simultaneously with classical, paraconsistent, and paracomplete negations? These three negations were separately studied in logics whose negations bear their names. Initially we will restrict our analysis to propositional logics by analyzing classical negation, ¬c, as treated by Classical Propositional Logic (LPC); the paraconsistent negation, ¬p, as treated through the hierarchy of Paraconsistent Propositional Calculi Cn (0 ≤ n ≤ ω); and the paracomplete negation, ¬q, as treated by (...) the hierarchy of Paracomplete Propositional Calculi Pn (0 ≤ n ≤ ω). In “Logics that are both paraconsistent and paracomplete” (1989), Newton da Costa proposed a system with approximate characteristics to what we are looking for. In the hierarchy of Non-Alethical Propositional Calculi Nn (0 ≤ n ≤ ω), only one negation is introduced (as primitive), called a “non-alethic” (¬n), whose operation preserves the properties of classical, or paraconsistent or paracomplete negation -- depending on the well or ill behavior of the formula connected to it. However, as we shall see, in the hierarchy Nn we can not reiterate negations with different behaviors in a same formula (e.g., ¬p¬cα or ¬q¬c¬p α), or even analyze a formula like ¬cα → ¬pα. In view of these problems, can we really say that the hierarchy Nn allows us to understand the relationships and interactions of the three types of negations? In order to deal with this, given the initial problem, we will present four axiomatic systems (KG) in which, unlike Nn, the three negations are directly introduced -- offering a semantics and a method of proofs by analytic tableaux. Through the KG Systems we will show how the negations interact, obtaining non-demonstrable theorems in LPC, Cn, Pn, and Nn (0 ≤ n ≤ ω). Finally, we will also offer a first-order extension for the KG Systems. (shrink)

This text is a short introduction to logic that was primarily used for accompanying an introductory course in Logic for Linguists held at the New University of Lisbon (UNL) in fall 2010. The main idea of this course was to give students the formal background and skills in order to later assess literature in logic, semantics, and related fields and perhaps even use logic on their own for the purpose of doing truth-conditional semantics. This course in logic does not replace (...) a proper introduction to semantics and is not intended as such, although parts of Chapter 1 and 4 could be used to supplement an introductory course in semantics. In contrast to other introductions it has a certain focus on ‘writing things down correctly.’ Proofs of metatheorems are omitted, though. -/- This is work in progress. Please send suggestions and corrigenda to [email protected]. Have fun! (shrink)

In her book Abductive Reasoning Atocha Aliseda (2006) stresses the attention to the logical models of abduction, centering on the semantic tableaux as a method for extending and improving both the whole cognitive/philosophical view on it and on other more restricted logical approaches. I will provide further insight on two aspects. The first is re-lated to the importance of increasing logical knowledge on abduction: Aliseda clearly shows how the logical study on abduction in turn helps us to extend and (...) modernize the classical and received idea of logic. The second refers to some ideas coming from the so-called distributed cognition and concerns the role of logical models as forms of cognitive exter-nalizations of preexistent in-formal human reasoning performances. The logical externalization in objective systems, communicable and sharable, is able to grant stable perspectives endowed with symbolic, abstract, and rigorous cogni-tive features. I will also emphasize that Aliseda especially stresses that this character of stability and objectivity of logical achievements are not usually present in models of abduction that are merely cognitive and epistemological, and of ex-treme importance from the computational point of view. (shrink)

This is a remarkable new French language introduction to elementary logical methods. Although designed primarily for computer and information specialists, it is also sure to interest philosophers and logicians because of its diversity of subjects, emphasis on graphic calculation techniques, and extensive historical background. The book is intelligently divided into nine main chapters with detailed descriptive subsections. It begins with the most fundamental principles of Aristotelian syllogistic and Boolean algebra, working through the essentials of Frege's predicate calculus and Gödel's consistency-completeness (...) metaproofs before systematically articulating standard propositional and predicate logics, interestingly, from synthetic and then analytic perspectives. This leads to a largely informal exposition of Tarski-style model set theoretical semantics, and the modern limiting metatheoretical results underlying what the authors call the "crisis" in the foundations of mathematical logic. Here are included such typical and more unusual topics as Herbrand models, König's Lemma, Herbrand's Theorem, Post machines, Floyd's Theorem, and Church's Theorem. The volume culminates in an expansive treatment of first order theories, including theories of order and models, and decidability. The exposition is somewhat rigorous, but should not be excessively demanding for nonprofessionals interested in the important implications of logic for philosophy, foundations of mathematics, and informatique. Among the book's virtues must be mentioned its profuse illustration of so many different graphic methods in mathematical logic, including Venn diagrams, the square of opposition, Smullyan truth trees, Wallen's reduction technique, Beth's and Hintikka's semantic tableaux method, and several styles of axiomatic and natural deduction. The work is certain to be a valuable resource for French readers in need of a lucid, comprehensive guide to the history and practical techniques of logic in its elementary applications to the philosophy of mathematics and information sciences.--Dale Jacquette, The Pennsylvania State University. (shrink)

In this paper we present tableau methods for two-dimensional modal logics. Although models for such logics are well known, proof systems remain rather unexplored as most of their developments have been purely axiomatic. The logics herein considered contain first-order quantifiers with identity, and all the formulas in the language are doubly-indexed in the proof systems, with the upper indices intuitively representing the actual or reference worlds, and the lower indices representing worlds of evaluation—first and second dimensions, respectively. The tableaux (...) modulate over different notions of validity such as local, general, and diagonal, besides being general enough for several two-dimensional logics proposed in the literature. We also motivate the introduction of a new operator into two-dimensional languages and explore some of the philosophical questions raised by it concerning the relations there are between actuality, necessity, and the a priori, that seem to undermine traditional intuitive interpretations of two-dimensional operators. (shrink)

We offer tableaux systems for logics of essence and accident and logics of non-contingency, showing their soundness and completeness for Kripke semantics. We also show an interesting parallel between these logics based on the semantic insensitivity of the two non-normal operators by which these logics are expressed.

Academia is a competitive environment. Early Career Researchers (ECRs) are limited in experience and resources and especially need achievements to secure and expand their careers. To help with these issues, this book offers a new approach for conducting research using the combination of mindsponge innovative thinking and Bayesian analytics. This is not just another analytics book. 1. A new perspective on psychological processes: Mindsponge is a novel approach for examining the human mind’s information processing mechanism. This conceptual framework is used (...) to construct models in studies. The framework is highly flexible and widely applicable for many different types of information processes. The mindsponge approach can help researchers discover interesting ideas or even formulate their very own theories when investigating psychosocial phenomena. This approach brings a fresh wind to the current landscape of social sciences and humanities (SSH). 2. Easy-to-follow analysis protocol: The Bayesian Mindsponge Framework (BMF analytics) is useful in terms of computing and visualizing power but also easy to learn and apply. Contrary to being intimidating, the Bayesian analytics section of this book is presented in a reader-friendly manner with a detailed yet clear step-by-step procedure. Examples are from published BMF articles, allowing readers to immediately practice the method and quickly create their own applications. With educational purposes in mind, the book is very suitable for ECRs who are looking to innovate their research methods. 3. Advocating for low-cost, high-quality research: Doing science can be very costly. Mindsponge innovative thinking and BMF analytics help produce impactful studies using openly available data on online repositories. This is based on the authors’ previous works and experiences. The book presents examples of employing the open R package bayesvl on secondary data from different sources. With less financial constraints, researchers can have more freedom of thought to pursue their curiosity and creativity. ECRs in low- and middle-income countries may find this aspect crucial in their careers. 4. Support and collaboration: The authors share their insights from experiences in the academic publishing system to help readers get through the processes of manuscript writing and peer-reviewing more easily. The authors are also ready to support other researchers with further inquiries and collaboration opportunities at the following website, mindsponge(dot)info. This book is for: a) ECRs whose only abundant resources are their innovation capacity and strength of will; b) Researchers in SSH who want to explore a novel approach to thinking and study conducting; c) Low- and middle-income countries’ researchers looking for a cost-effective research protocol; and, d) Innovative thinkers who want to turn their interesting thoughts into good publications. (shrink)

In the paper, we examine tableau systems for R. Epstein’s logics of content relationship: D (Dependence Logic), DD (Dual Dependence Logic), Eq (Logic of Equality of Content), S (Symmetric Relatedness Logic) and R (Nonsymmetric Relatedness Logic) (cf. Epstein in Philos Stud 36:137–173, 1979, Epstein in Rep. Math. Logic 21:19–34, 1987, Klonowski in Logic Log Philos 30(4):579–629, 2021, Krajewski in J Non Class Logic 8:7–33, 1991). The first tableau systems for those logics were defined by Carnielli. However, his approach has some (...) limitations, for example, it requires a proof of functional completeness and axiomatization. Notwithstanding the first two constraints, it does not include all Epstein logics, e.g., logic Eq. Unlike Carnielli’s approach, here we use set-assignment semantics to determine those logics. Since syntax and semantics of a given logic usually determine a minimal syntax and structure of a tableau system for the logic along with other properties, we propose a uniform tableau framework for the logics determined by set-assignment semantics. What distinguishes our tableau systems is that they combine the features of tableaux for propositional logics and syllogistic logics when the problem of content of propositions is analysed in tableau proofs. To denote the content of propositions in the proofs, we use generalised labels (see Jarmużek and Goré in Landscapes in Logic, College Publications, London, 2021). (shrink)