We compare the logic HYPE recently suggested by H. Leitgeb as a basic propositional logic to deal with hyperintensional contexts and Heyting-Ockham logic introduced in the course of studying logical aspects of the well-founded semantics for logic programs with negation. The semantics of Heyting-Ockham logic makes use of the so-called Routley star negation. It is shown how the Routley star negation can be obtained from Dimiter Vakarelov’s theory of negation and that propositional HYPE coincides with the logic characterized by the (...) class of all involutive Routley star information frames. This result provides a much simplified semantics for HYPE and also a simplified axiomatization, which shows that HYPE is identical with the modal symmetric propositional calculus introduced by G. Moisil in 1942. Moreover, it is shown that HYPE can be faithfully embedded into a normal bi-modal logic based on classical logic. Against this background, we discuss the notion of hyperintensionality. (shrink)

In this paper we present a solution of the axiomatization problem for the Fmla-Fmla versions of the Pietz and Rivieccio exactly true logic and the non-falsity logic dual to it. To prove the completeness of the corresponding binary consequence systems we introduce a specific proof-theoretic formalism, which allows us to deal simultaneously with two consequence relations within one logical system. These relations are hierarchically organized, so that one of them is treated as the basic for the resulting logic, and the (...) other is introduced as an extension of this basic relation. The proposed bi-consequences systems allow for a standard Henkin-style canonical model used in the completeness proof. The deductive equivalence of these bi-consequence systems to the corresponding binary consequence systems is proved. We also outline a family of the bi-consequence systems generated on the basis of the first-degree entailment logic up to the classic consequence. (shrink)

Following a proposal by Kooi and Tamminga, we introduce a conservative translation manual for every four-valued truth-functional propositional logic into a modal logic. However, the application of this translation does not preserve the intuitive reading of the truth-values for every four-valued logic. In order to solve this problem, we modify the translation manual and prove its conservativity by exploiting the method of generalized truth-values.

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, bi-intuitionistic multilattice logic, which is a combination of multilattice logic and the bi-intuitionistic logic also known as Heyting–Brouwer logic, is introduced as a Gentzen-type sequent calculus. A Kripke semantics is developed for this logic, and the completeness theorem with respect to this semantics is proved via theorems for embedding this logic into bi-intuitionistic logic. The logic proposed is an extension of first-degree entailment logic and can be regarded as a bi-intuitionistic variant of the original classical multilattice logic (...) determined by the algebraic structure of multilattices. Similar completeness and embedding results are also shown for another logic called bi-intuitionistic connexive multilattice logic, obtained by replacing the connectives of intuitionistic implication and co-implication with their connexive variants. (shrink)

In a recent paper we have defined an analytic tableau calculus PL_16 for a functionally complete extension of Shramko and Wansing's logic based on the trilattice SIXTEEN_3. This calculus makes it possible to define syntactic entailment relations that capture central semantic relations of the logic---such as the relations |=_t, |=_f, and |=_i that each correspond to a lattice order in SIXTEEN_3; and |=, the intersection of |=_t and |=_f,. -/- It turns out that our method of characterising these semantic relations---as (...) intersections of auxiliary relations that can be captured with the help of a single calculus---lends itself well to proving interpolation. All entailment relations just mentioned have the interpolation property, not only when they are defined with respect to a functionally complete language, but also in a range of cases where less expressive languages are considered. For example, we will show that |=, when restricted to L_{tf}, the language originally considered by Shramko and Wansing, enjoys interpolation. This answers a question that was recently posed by M. Takano. (shrink)

Shramko [. Truth, falsehood, information and beyond: The American plan generalized. In K. Bimbo, J. Michael Dunn on information based logics, outstanding contributions to logic...

Sequent calculi for trilattice logics, including those that are determined by the truth entailment, the falsity entailment and their intersection, are given. This partly answers the problems in Shramko-Wansing.

Paradefinite logics are logics that can be used for handling contradictory or partial information. As such, paradefinite logics should be both paraconsistent and paracomplete. In this paper we consider the simplest semantic framework for introducing paradefinite logics. It consists of the four-valued matrices that expand the minimal matrix which is characteristic for first degree entailments: Dunn–Belnap matrix. We survey and study the expressive power and proof theory of the most important logics that can be developed in this framework.

The aim of the present paper is to introduce a system, where the epistemic state of an agent is represented truth-functionally. In order to obtain this system, we propose a four-valued logic, that we call the logic of rational agent, where the fact of knowing something is formalized at the level of valuations, without the explicit use of epistemic knowledge operator. On the basis of this semantics, a sound and complete system with two distinct truth-functional negations is provided. These negations (...) allow us to express the statements about knowing or not knowing something at the syntactic level. Moreover, such a system is applied to the analysis of knowability paradox. In particular, we show that the paradox is not derivable in terms of the logic of rational agent. (shrink)

The Fregean-inspired Principle of Compositionality of Meaning for formal languages asserts that the meaning of a compound expression is analysable in terms of the meaning of its constituents, taking into account the mode in which these constituents are combined so as to form the compound expression. From a logical point of view, this amounts to prescribing a constraint—that may or may not be respected—on the internal mechanisms that build and give meaning to a given formal system. Within the domain of (...) formal semantics and of the structure of logical derivations, the PoC is often directly reflected by metaproperties such as truth-functionality and analyticity, characteristic of computationally well-behaved logical systems. (shrink)