Search

We propose in this paper a family of algebraic models of ZFC based on the three-valued paraconsistent logic LPT0, a linguistic variant of da Costa and D'Ottaviano's logic J3. The semantics is given by twist structures defined over complete Boolean agebras. The Boolean-valued models of ZFC are adapted to twist-valued models of an expansion of ZFC by adding a paraconsistent negation. This allows for inconsistent sets w satisfying 'not (w = w)', where 'not' stands for the paraconsistent negation. Finally, our framework is adapted to provide a class of twist-valued models generalizing Löwe and Tarafder's model based on logic (PS3,∗), showing that they are paraconsistent models of ZFC. The present approach offers more options for investigating independence results in paraconsistent set theory. [ABSTRACT FROM AUTHOR]

Let MK3 I and MK3 I I be Kleene's strong 3-valued matrix with only one and two designated values, respectively. Next, let MK3 G (resp., MK3 d G ) be defined exactly as MK3 I (resp., MK3 I I ), except that the characteristic Łukasiewicz-type negation of Kleene's strong 3-valued matrix is replaced by a 'Gödel-type' negation (resp., 'dual Gödel-type' negation). The aim of this paper is to axiomatize the logics determined by all natural implicative expansions of MK3 G and MK3 d G . The axiomatic formulations are defined by using a 'two-valued' Belnap-Dunn semantics. [ABSTRACT FROM AUTHOR]

Pretabularity is the attribute of logics that are not characterised by finite matrices, but all of whose proper extensions are. Two of the first-known pretabular logics were Dummett's famous super-intuitionistic logic LC and the well-known semi-relevance logic RM (= R-Mingle). In this paper, we investigate Anderson and Belnap's relevance logic R with the extra axiom: (p → q) ∨ (q → p), which we name LR, and which is (much) weaker than RM, and so is not pretabular. This means that over LR, there may be some pretabular extensions other than RM, two of which this paper presents and with which it provides axiomatizations, characteristic algebras, and Routley-Meyer semantics. [ABSTRACT FROM AUTHOR]

This note presents some new results from [1] about the Suszko operator and truth‐equational logics, following the works of Czelakowski [11] and Raftery [17]. It is proved that the Suszko operator relative to a truth‐equational logic S preserves suprema and commutes with endomorphisms. Together with injectivity, proved by Raftery in [17], the Suszko operator relative to a truth‐equational logic is a structural representation, as defined in [15]. Furthermore, if Alg(S) is a quasivariety, then the Suszko operator relative to a truth‐equational logic is continuous. Finally, it is proved that truth is equationally definable in the class LModSu(S) if and only if Alg(S) is a τ∞‐algebraic semantics for S and the Suszko operator Ω∼SFm:ThS→CoAlg(S)Fm preserves suprema and commutes with substitutions. [ABSTRACT FROM AUTHOR]

From the 1960s to the present day, Aristotelian aporias have been at the forefront of the question of the epistemological nature of first science. Authors vary from a purely dialectical interpretation of the aporias to an acquisitive interpretation of knowledge. The present article attempts to show the existence of objective, i.e. acquisitive aporias of knowledge. These aporias are based on an Aristotelian theory of objectivity which, overcoming the Platonic theory of contrariety, is expressed in his theory of contradiction, which bases the relation between reality and knowledge on the different levels of the metaphysical and logical structure of reality: semantic, propositional and inferential. Thus, objective aporias are those that express the determination of the object as substance and, from it, a possibility of reconciling the diaporematic method with Aristotelian epistemological realism. [ABSTRACT FROM AUTHOR]

Refinement relations, such as trace containment, simulation preorder, and their alternating versions, have been successfully applied in formal verification of concurrent systems. Recently, trace containment and simulation preorder have been adopted and developed in fuzzy systems, but the generalization of their alternating versions to fuzzy systems has not been investigated. To satisfy the need for modeling and analyzing fuzzy systems, this article proposes two types of refinement relations called fuzzy alternating trace containment and fuzzy alternating simulation preorder, based on fuzzy concurrent game structures (FCGSs) under the Gödel semantics. These two fuzzy notions inherit properties from the corresponding classical setting. For example, fuzzy alternating simulation preorder for finite-state FCGSs can be computed in polynomial time; fuzzy alternating simulation preorder is a fuzzy subset of fuzzy alternating trace containment, and both relations can be logically characterized in terms of fuzzy version of alternating-time temporal logic. These properties make the theory developed here suitable for the modeling and verification of fuzzy systems. [ABSTRACT FROM AUTHOR]

Three-valued logics are standardly used to formalize gappy languages, i.e., interpreted languages in which sentences can be true, false or neither. A three-valued logic that assigns the same truth value to all gappy sentences is, in our view, insufficient to capture important semantic differences between them. In this paper we will argue that there are two different kinds of pathologies that should be treated separately and we defend the usefulness of a four-valued logic to represent adequately these two types of gappy sentences. Our purpose is to begin the formal exploration of the four-valued logics that could be used to represent the phenomena in question and to show that these phenomena are present in natural language, at least according to some semantic theories of natural language. [ABSTRACT FROM AUTHOR]

We argue for a compositional semantics grounded in a strongly typed ontology that reflects our commonsense view of the world and the way we talk about it. Assuming such a structure we show that the semantics of various natural language phenomena may become nearly trivial.

In Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti (1936) and Reichenbach (1935, 1944) on the one hand, and by Cooper (Inquiry, 11, 295–320, 1968) and Cantwell (Notre Dame Journal of Formal Logic, 49, 245–260, 2008) on the other. Here we provide the proof theory for the resulting logics DF/TT and CC/TT, using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: DF/TT allows for algebraic completeness, but not for the construction of a canonical model, while CC/TT fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects. [ABSTRACT FROM AUTHOR]

This paper explores trivalent truth conditions for indicative conditionals, examining the "defective" truth table proposed by de Finetti (1936) and Reichenbach (1935, 1944). On their approach, a conditional takes the value of its consequent whenever its antecedent is true, and the value Indeterminate otherwise. Here we deal with the problem of selecting an adequate notion of validity for this conditional. We show that all standard validity schemes based on de Finetti's table come with some problems, and highlight two ways out of the predicament: one pairs de Finetti's conditional (DF) with validity as the preservation of non-false values (TT-validity), but at the expense of Modus Ponens; the other modifies de Finetti's table to restore Modus Ponens. In Part I of this paper, we present both alternatives, with specific attention to a variant of de Finetti's table (CC) proposed by Cooper (Inquiry 11, 295–320, 1968) and Cantwell (Notre Dame Journal of Formal Logic 49, 245–260, 2008). In Part II, we give an in-depth treatment of the proof theory of the resulting logics, DF/TT and CC/TT: both are connexive logics, but with significantly different algebraic properties. [ABSTRACT FROM AUTHOR]

The preferential conditional logic |$ \mathbb{PCL} $|⁠ , introduced by Burgess, and its extensions are studied. First, a natural semantics based on neighbourhood models, which generalizes Lewis' sphere models for counterfactual logics, is proposed. Soundness and completeness of |$ \mathbb{PCL} $| and its extensions with respect to this class of models are proved directly. Labelled sequent calculi for all logics of the family are then introduced. The calculi are modular and have standard proof-theoretical properties, the most important of which is admissibility of cut that entails a syntactic proof of completeness of the calculi. By adopting a general strategy, root-first proof search terminates, thereby providing a decision procedure for |$ \mathbb{PCL} $| and its extensions. Finally, semantic completeness of the calculi is established: from a finite branch in a failed proof attempt it is possible to extract a finite countermodel of the root sequent. The latter result gives a constructive proof of the finite model property of all the logics considered. [ABSTRACT FROM AUTHOR]

I introduce a proof system for the logic of relative fundamentality, as well as a natural semantics with respect to which the system is both sound and complete. I then "modalise" the logic, and finally I discuss the properties of grounding given a suggested account of this notion in terms of necessity and relative fundamentality. [ABSTRACT FROM AUTHOR]

We determine the modal logic of fixed-point models of truth and their axiomatizations by Solomon Feferman via Solovay-style completeness results. Given a fixed-point model $\mathcal {M}$ , or an axiomatization S thereof, we find a modal logic M such that a modal sentence $\varphi $ is a theorem of M if and only if the sentence $\varphi ^*$ obtained by translating the modal operator with the truth predicate is true in $\mathcal {M}$ or a theorem of S under all such translations. To this end, we introduce a novel version of possible worlds semantics featuring both classical and nonclassical worlds and establish the completeness of a family of noncongruent modal logics whose internal logic is nonclassical with respect to this semantics. [ABSTRACT FROM AUTHOR]

We characterize Weihrauch reducibility in $ \operatorname {\mathrm {E-PA^{\omega }}} + \operatorname {\mathrm {QF-AC^{0,0}}}$ and all systems containing it by the provability in a linear variant of the same calculus using modifications of Gödel's Dialectica interpretation that incorporate ideas from linear logic, nonstandard arithmetic, higher-order computability, and phase semantics. [ABSTRACT FROM AUTHOR]

Artificial intelligence (AI) research enjoyed an initial period of enthusiasm in the 1970s and 80s, but this enthusiasm was tempered by a long interlude of frustration when genuinely useful AI applications failed to be forthcoming. Today, we are experiencing once again a period of enthusiasm, fired above all by the successes of the technology of deep neural networks or deep machine learning. In this paper we draw attention to what we take to be serious problems underlying current views of artificial intelligence encouraged by these successes, especially in the domain of language processing. We then show an alternative approach to language-centric AI, in which we identify a role for philosophy. [ABSTRACT FROM AUTHOR]

A logical framework is presented to model legal interpretation and bring an appropriate construction of legal arguments. Reasoning with assumptions allows the construction of hypotheses. This is proposed in the context of legal procedures' dynamics, where the framework evolves as part of the investigation prior to each trial instance. Two gender-biased legal cases from the Argentinian jurisprudence are analyzed in the light of the proposed theory. Afterward, some proof standards for civil law systems are discussed as a way to define a specialized dialectical argumentation semantics. We claim that the application of the proposed theory would bring software assistance for controlling the influence of external factors of the law in the investigation of a legal case. [ABSTRACT FROM AUTHOR]

The present paper develops a unified correspondence treatment of the Sahlqvist theory for possibility semantics, extending the results in the work by Yamamoto (2016, Journal of Logic and Computation , 27 , 2411–2430) from Sahlqvist formulas to the strictly larger class of inductive formulas and from the full possibility frames to filter-descriptive possibility frames. Specifically, we define the possibility semantics version of the algorithm Ackermann lemma based algorithm (ALBA) and an adapted interpretation of the expanded modal language used in the algorithm. One notable feature of the adaptation of ALBA to possibility frames setting is that the so-called nominal variables, which are interpreted as complete join-irreducibles in the standard setting, are interpreted as regular open closures of 'singletons' in the present setting, which is a novelty of the present paper. We prove the soundness of the algorithm with respect to both (the dual algebras of) full possibility frames and (the dual algebras of) filter-descriptive possibility frames, use the algorithm to give an alternative proof to the one in the work by Holliday (2016, Possibility frames and forcing for modal logic. UC Berkeley Working Paper in Logic and the Methodology of Science. URL. http://escholarship.org/uc/item/9v11r0dq) that the inductive formulas are constructively canonical and show that the algorithm succeeds on inductive formulas. We make some comparisons among different semantic settings in the design of the algorithms and fit possibility semantics into this broader picture. [ABSTRACT FROM AUTHOR]

This paper provides some model-theoretic analysis for probability (modal) logic (⁠|$PL$|⁠). It is known that this logic does not enjoy the compactness property. However, by passing into the sublogic of |$PL$|⁠ , namely basic probability logic (⁠|$BPL$|⁠), it is shown that this logic satisfies the compactness property. Furthermore, by drawing some special attention to some essential model-theoretic properties of |$PL$|⁠ , a version of Lindström characterization theorem is investigated. In fact, it is verified that probability logic has the maximal expressive power among those abstract logics extending |$PL$| and satisfying both the filtration and disjoint unions properties. Finally, by alternating the semantics to the finitely additive probability models (⁠|$\mathcal{F}\mathcal{P}\mathcal{M}$|⁠) and introducing positive sublogic of |$PL$| including |$BPL$|⁠ , it is proved that this sublogic possesses the compactness property with respect to |$\mathcal{F}\mathcal{P}\mathcal{M}$|⁠. [ABSTRACT FROM AUTHOR]

In 2016, Béziau introduced the notion of genuine paraconsistent logic as logic that does not verify the principle of non-contradiction; as an important example, he presented the genuine paraconsistent logic S P 3 A in terms of three connectives , , and. In this paper, we show that S P 3 A is an axiomatic extension of C 1 through the introduction of a non-primitive deductive implication. Furthermore, we prove that S P 3 A is an algebraisable logic with Blok-Pigozzi's method. From the proof that C 1 is non-algebraisable logic, we are able to see that C ω is not algebraisable logic and studying the borders of algebrisabilty, we can give an enumerable family of new genuine, paraconsistent and non-algebraisable logics, extensions of C ω . Finally, we introduced n-valued ( n < ω) and infinite-valued C ω logic and show that they are genuine and non-algebraisable paraconsistent ones; in addition, we present semantics for this extensions of C ω by means of Fidel's structures. [ABSTRACT FROM AUTHOR]

When we say "I know why he was late", we know not only the fact that he was late, but also an explanation of this fact. We propose a logical framework of "knowing why" inspired by the existing formal studies on why-questions, scientific explanation, and justification logic. We introduce the K y i operator into the language of epistemic logic to express "agent i knows why φ " and propose a Kripke-style semantics of such expressions in terms of knowing an explanation of φ . We obtain two sound and complete axiomatizations w.r.t. two different model classes depending on different assumptions about introspection. Finally we connect our logic with justification logic technically by providing an alternative semantics and an in-depth comparison on various design choices. [ABSTRACT FROM AUTHOR]

We investigate an expansion of positive intuitionistic logic obtained by adding a constant Ω introduced by Lloyd Humberstone. Our main results include a sound and strongly complete axiomatization, some comparisons to other expansions of intuitionistic logic obtained by adding actuality and empirical negation, and an algebraic semantics. We also brie y discuss its connection to classical logic. [ABSTRACT FROM AUTHOR]

Epistemic Logic is our basic universal science, the method of our cognitive confrontation in reality to prove the truth of our basic cognitions and theories. Hence, by proving their true representation of reality we can self-control ourselves in it, and thus refuting the Berkeleyian solipsism and Kantian a priorism. The conception of epistemic logic is that only by proving our true representation of reality we achieve our knowledge of it, and thus we can prove our cognitions to be either true or rather false, and otherwise they are doubtful. Therefore, truth cannot be separated from being proved and we cannot hold anymore the principle of excluded middle, as it is with formal semantics of metaphysical realism. In distinction, the intuitionistic logic is based on subjective intellectual feeling of correctness in constructing proofs, and thus it is epistemologically encapsulated in the metaphysical subject. However, epistemic logic is our basic science which enable us to prove the truth of our cognitions, including the epistemic logic itself. [ABSTRACT FROM AUTHOR]

Regarding strictly monadic second‐order logic (SMSOL), which is the fragment of monadic second‐order logic in which all predicate constants are unary and there are no function symbols, we show that a standard deductive system with full comprehension is sound and complete with respect to standard semantics. This result is achieved by showing that in the case of SMSOL, the truth value of any formula in a faithful identity‐standard Henkin structure is preserved when the structure is "standardized"; that is, the predicate domain is expanded into the set of all unary relations. In addition, we obtain a simpler proof of the decidability of SMSOL. [ABSTRACT FROM AUTHOR]

In a recent book, Logical Form: between Logic and Natural Language, Andrea Iacona argues that semantic form and logical form are distinct. The semantic form of a sentence is something that (together with the meanings of its parts) determines what it means; the logical from of a sentence is something that (all by itself) determines whether it is a logical truth. Semantic form does not depend on context but logical form does: for example, whether 'This is this' is a logical truth depends on whether the two occurrences of 'this' are used to demonstrate the same individual. I respond by claiming that logical form is indifferent to reference and is sensitive only to obligatory co-reference. When the speaker intends both occurrences of 'this' to be interpreted the same way the logical from of 'This is this' is a=a, while in a context where the speaker has no such intention it is a=b. This proposal allows a much more conservative revision of the traditional picture than the one suggested by Iacona. Instead of identifying the logical form of a natural language sentence by seeking a formalization in an artificial language, we obtain it through abstraction from its syntactic analysis: replacing the non-logical expressions by schematic letters, making sure that we use identical ones if and only if the speaker intended co-reference. [ABSTRACT FROM AUTHOR]

We consider Hilbert-style non–well-founded derivations in the Gödel-Löb provability logic GL and establish that GL with the obtained derivability relation is globally complete for algebraic and neighbourhood semantics. [ABSTRACT FROM AUTHOR]

In recent work, Stalnaker proposes a logical framework in which belief is realized as a weakened form of knowledge 35. Building on Stalnaker's core insights, and using frameworks developed in 11 and 3, we employ topological tools to refine and, we argue, improve on this analysis. The structure of topological subset spaces allows for a natural distinction between what is known and (roughly speaking) what is knowable; we argue that the foundational axioms of Stalnaker's system rely intuitively on both of these notions. More precisely, we argue that the plausibility of the principles Stalnaker proposes relating knowledge and belief relies on a subtle equivocation between an "evidence-in-hand" conception of knowledge and a weaker "evidence-out-there" notion of what could come to be known. Our analysis leads to a trimodal logic of knowledge, knowability, and belief interpreted in topological subset spaces in which belief is definable in terms of knowledge and knowability. We provide a sound and complete axiomatization for this logic as well as its uni-modal belief fragment. We then consider weaker logics that preserve suitable translations of Stalnaker's postulates, yet do not allow for any reduction of belief. We propose novel topological semantics for these irreducible notions of belief, generalizing our previous semantics, and provide sound and complete axiomatizations for the corresponding logics. [ABSTRACT FROM AUTHOR]

If one takes seriously the idea that a scientific language must be extensional, and accepts Quine's notion of truth-value-related extensionality, and also recognizes that a scientific language must allow for singular terms that do not refer to existing objects, then there is a problem, since this combination of assumptions must be inconsistent. I will argue for a particular solution to the problem, namely, changing what is meant by the word 'extensionality', so that it would not be the truth-value that had to be preserved under the substitution of co-extensional expressions, but the state of affairs that the sentence described. The question is whether or not elementary sentences containing empty singular terms, such as 'Vulcan rotates', are extensional in the substitutivity sense. Five conditions are specified under which extensionality in the substitutivity sense of such sentences can be secured. It is demonstrated that such sentences are state-of-affairs-as-extension-related extensional. This implies (in accordance with the basic idea of state-of-affairs semantics) that such sentences are also truth-value-related extensional in Quine's sense, but not truth-value-as-extension-related extensional. [ABSTRACT FROM AUTHOR]

Cyber-physical systems (CPSs) are systems with both physical and software components, for example, cars and industrial robots. Since these systems exhibit both discrete and continuous dynamics, they are complex and it is thus difficult to verify that they behave as expected. Falsification of temporal logic properties is an approach to find counterexamples to CPSs by means of simulation. In this article, we propose two additions to enhance the capability of falsification and make it more viable in a large-scale industrial setting. The first addition is a framework for transforming specifications from a signal-based model into signal temporal logic. The second addition is the use of valued Booleans and an additive robust semantics in the falsification process. We evaluate the performance of the additive robust semantics on a set of benchmark models, and we can see that which semantics are preferable depend both on the model and on the specification. [ABSTRACT FROM AUTHOR]

The paper starts by briefly describing the so‐called truth‐functional approach to sentential operators, typical to logic, as opposed to the more multi‐faceted approach of linguistics. The latter reflects the more complex, substantial relations between the contents of utterances, emphasizing the logico‐semantical relations and functions of sentential operators. However, as an alternative to the pragmatically inclined critique of the truth‐functional approach, the paper proposes two possible directions of explaining the specific content of sentential operators by virtue of which they transcend the role of mere truth functions. Firstly, the paper summarizes our previous investigations into the interactions between sentential operators and (1) the vector of the course of events described by a compound sentence, and (2) the direction of grammatical time captured by a compound sentence. The paper focuses on how this interaction is coordinated with the particular epistemic goal (prediction, explanation etc.) pursued when using the meaning of a complex sentence. Using the concepts of necessary and sufficient conditions, and by characterizing the vectors of condition (the if‐vector), time and relevance (dominance or the epistemic vector), the paper demarcates the rules of correspondence for conditional operators as cases of combinatorics, as described by some linguists. Secondly, based on a distinction between different constructions the same operators as truth‐functions, the paper provides a logico‐semantical explanation of the specific meaning of the else, unless and although connectives, traditionally discussed by linguists. We believe that the extensions proposed here move the camp defending a logico‐semantic approach to sentential operators at least somewhat closer to the camp of linguistic investigation. [ABSTRACT FROM AUTHOR]

The purpose of this paper is to present a formalization of the language, semantics and axiomatization of justification logic in Coq. We present proofs in a natural deduction style derived from the axiomatic approach of justification logic. Additionally, we present possible world semantics in Coq based on Fitting models to formalize the semantic satisfaction of formulas. As an important result, with this implementation, it is possible to give a proof of soundness for |$\mathsf{L}\mathsf{P}$| with respect to Fitting models. [ABSTRACT FROM AUTHOR]

Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define Polyteam Semantics in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatization for the associated implication problem. We relate polyteam semantics to team semantics and investigate in which cases logics over the former can be simulated by logics over the latter. We also characterize the expressive power of poly-dependence logic by properties of polyteams that are downwards closed and definable in existential second-order logic (⁠|$\textsf{ESO}$|⁠). The analogous result is shown to hold for poly-independence logic and all |$\textsf{ESO}$| -definable properties. We also relate poly-inclusion logic to greatest fixed point logic. [ABSTRACT FROM AUTHOR]

We provide a new semantics and a slightly different formalisation for the propositional logic with superposition (PLS) introduced and studied in Tzouvaras [(2018). Propositional superposition logic. Logic Journal of the IGPL, 26(1), 149–190]. PLS results from Propositional Logic (PL) by adding a new binary connective | construed as the 'superposition operation' and a few axioms about it. The original semantics used in the above paper was the so-called sentence choice semantics (SCS), based on choice functions for all pairs of classical formulas of PL. In contrast, the algebraic or Boolean-value choice semantics (BCS) developed in this paper is based on choice functions for pairs of elements of a Boolean algebra B in which the classical sentences take truth values. The Boolean-value choice functions can be subject to similar constraints as those imposed on sentence choice functions. The new axiomatisation is based on the same set of axioms as the previous one but uses a new inference rule, called Rule of Analogy (RA), in place of the rule Salva Veritate (SV) of the previous systems. The Deduction Theorem fails in the systems containing the new rule. As a consequence the completeness theorems for them hold conditionally again, namely the systems are complete with respect to BCS if and only if every consistent set of sentences is extended to a consistent and complete set. Finally connections are established between tautologies of the semantics SCS and those of BCS. [ABSTRACT FROM AUTHOR]

Logical pluralism is commonly described as the view that there is more than one correct logic. It has been claimed that, in order for that view to be interesting, there has to be at least a potential for rivalry between the correct logics. This paper offers a detailed assessment of this suggestion. I argue that an interesting version of logical pluralism is hard, if not impossible, to achieve. I first outline an intuitive understanding of the notions of rivalry and correctness. I then discuss a natural account of rivalry in terms of disagreement about validity claims and the argument from meaning variance that has been raised against it. I explore a more refined picture of the meaning of validity claims that makes use of the character-content distinction of classical two dimensional semantics. There are three ways in which pluralists can use that framework to argue for the view that different logics may be rivals but could nevertheless be equally correct. I argue that none of them is convincing. [ABSTRACT FROM AUTHOR]

Rough set theory is studied to manage uncertain and inconsistent information. Because Pawlak's decision logic for rough sets is based on the classical two-valued logic, it is inconvenient for handling inconsistent information. We propose a bilattice logic as the deduction basis for the decision logic of rough sets to address inconsistent and ambiguous information. To enhance the decision logic to bilattice semantics, we introduce Variable Precision Rough Set (VPRS). As a deductive basis for bilattice decision logic, we define a consequence relation for Belnap's four-valued semantics and provide a bilattice semantic tableau TB4 for a deduction system. We demonstrate the soundness and completeness of TB4 and enhance it with weak negation. [ABSTRACT FROM AUTHOR]