This paper is concerned with counterfactual logic and its implications for the modal status of mathematical claims. It is most directly a response to an ambitious program by Yli-Vakkuri and Hawthorne (2018), who seek to establish that mathematics is committed to its own necessity. I claim that their argument fails to establish this result for two reasons. First, their assumptions force our hand on a controversial debate within counterfactual logic. In particular, they license counterfactual strengthening— the inference from ‘If A (...) were true then C would be true’ to ‘If A and B were true then C would be true’—which many reject. Second, the system they develop is provably equivalent to appending Deduction Theorem to a T modal logic. It is unsurprising that the combination of Deduction Theorem with T results in necessitation; indeed, it is precisely for this reason that many logicians reject Deduction Theorem in modal contexts. If Deduction Theorem is unacceptable for modal logic, it cannot be assumed to derive the necessity of mathematics. (shrink)

It is well known that the non-orthogonality relation between the (pure) states of a quantum system is reflexive and symmetric, and the modal logic $$\mathbf {KTB}$$ is sound and complete with respect to the class of sets each equipped with a reflexive and symmetric binary relation. In this paper, we consider two properties of the non-orthogonality relation: Separation and Superposition. We find sound and complete modal axiomatizations for the classes of sets each equipped with a reflexive and symmetric relation that (...) satisfies each one of these two properties and both, respectively. We also show that the modal logics involved are decidable. (shrink)

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property.

It is natural to ask under what conditions negating a conditional is equivalent to negating its consequent. Given a bivalent background logic, this is equivalent to asking about the conjunction of Conditional Excluded Middle (CEM, opposite conditionals are not both false) and Weak Boethius' Thesis (WBT, opposite conditionals are not both true). In the system CI.0 of consequential implication, which is intertranslatable with the modal logic KT, WBT is a theorem, so it is natural to ask which instances of CEM (...) are derivable. We also investigate the systems CIw and CI of consequential implication, corresponding to the modal logics K and KD respectively, with occasional remarks about stronger systems. While unrestricted CEM produces modal collapse in all these systems, CEM restricted to contingent formulas yields the Alt2 axiom (semantically, each world can see at most two worlds), which corresponds to the symmetry of consequential implication. It is proved that in all the main systems considered, a given instance of CEM is derivable if and only if the result of replacing consequential implication by the material biconditional in one or other of its disjuncts is provable. Several related results are also proved. The methods of the paper are those of propositional modal logic as applied to a special sort of conditional. (shrink)

Gödel logic is the extension of intuitionistic logic by the linearity axiom. Symmetric Gödel logic is a logical system, the language of which is an enrichment of the language of Gödel logic with their dual logical connectives. Symmetric Gödel logic is the extension of symmetric intuitionistic logic. The proof-intuitionistic calculus, the language of which is an enrichment of the language of intuitionistic logic by modal operator was investigated by Kuznetsov and Muravitsky. Bimodal symmetric Gödel logic is a logical system, the (...) language of which is an enrichment of the language of Gödel logic with their dual logical connectives and two modal operators. Bimodal symmetric Gödel logic is embedded into an extension of Gödel–Löb logic, the language of which contains disjunction, conjunction, negation and two modal operators. The variety of bimodal symmetric Gödel algebras, that represent the algebraic counterparts of bimodal symmetric Gödel logic, is investigated. Description of free algebras and characterization of projective algebras in the variety of bimodal symmetric Gödel algebras is given. All finitely generated projective bimodal symmetric Gödel algebras are infinite, while finitely generated projective symmetric Gödel algebras are finite. (shrink)

Trying to overcome Dugundji’s result on uncharacterisability of modal logics by finite logical matrices, Kearns and Ivlev proposed, independently, a characterisation of some modal systems by means of four-valued multivalued truth-functions , as an alternative to Kripke semantics. This constitutes an antecedent of the non-deterministic matrices introduced by Avron and Lev . In this paper we propose a reconstruction of Kearns’s and Ivlev’s results in a uniform way, obtaining an extension to another modal systems. The first part of the paper (...) is devoted to four-valued Nmatrices, including Kearns’s and Ivlev’s. Besides proving with full details Kearns’s results for T, S4 and S5, we also obtain a characterisation of the system B by four-valued Nmatrices with level valuations. Concerning Ivlev’s results, two new modal systems are introduced and char.. (shrink)

In this paper we provide frame definability results for weak versions of classical modal axioms that can be expressed in Fitting's many-valued modal languages. These languages were introduced by M. Fitting in the early '90s and are built on Heyting algebras which serve as the space of truth values. The possible-worlds frames interpreting these languages are directed graphs whose edges are labelled with an element of the underlying Heyting algebra, providing us a form of many-valued accessibility relation. Weak axioms of (...) the form we treat here have been examined from the completeness perspective and further explored for applications in non-monotonic reasoning. Here, we introduce more weak many-valued modal axioms and prove a frame correspondence result for all of them. The classes of corresponding labelled frames possess algebraic properties which are strongly reminiscent of many classical ones, such as the Church-Rosser property, reflexivity, transitivity, partial functionality, etc. (shrink)

Here, we provide a detailed description of the mutual relation of formulas with finite propositional variables p1, …, pm in modal logic S4. Our description contains more information on S4 than those given in Shehtman (1978) and Moss (2007); however, Shehtman (1978) also treated Grzegorczyk logic and Moss (2007) treated many other normal modal logics. Specifically, we construct normal forms, which behave like the principal conjunctive normal forms in the classical propositional logic. The results include finite and effective methods to (...) find a normal form equivalent to a given formula A by clarifying the behavior of connectives and giving a finite method to list all exact models. (shrink)

The paper is a brief survey of the most important semantic constructions founded on the concept of possible world. It is impossible to capture in one short paper the whole variety of the problems connected with manifold applications of possible worlds. Hence, after a brief explanation of some philosophical matters I take a look at possible worlds from rather technical standpoint of logic and focus on the applications in formal semantics. In particular, I would like to focus on the fruitful (...) marriage of possible world semantics and algebra and its evolution leading to very general construction of Wójcicki called referential semantics and some of its refinements. The presentation is informal and sketchy; the main purpose is to put in one place a short, and readable I hope, description of the most important constructions and to point out the main sources of these solutions. (shrink)

Jean-Yves Béziau (‘Classical Negation can be Expressed by One of its Halves’, Logic Journal of the IGPL 7 (1999), 145–151) has given an especially clear example of a phenomenon he considers a sufficiently puzzling to call the ‘paradox of translation’: the existence of pairs of logics, one logic being strictly weaker than another and yet such that the stronger logic can be embedded within it under a faithful translation. We elaborate on Béziau’s example, which concerns classical negation, as well as (...) giving some additional background (especially from intuitionistic logic) to the example. Our interest is more on the logical exploration of the phenomenon Béziau’s case exemplifies than on the question of whether that phenomenon is (even prima facie ) paradoxical, though in Section 5 we do approach the latter question – somewhat obliquely – by considering an analogous phenomenon which it is hard to find puzzling. (shrink)

Only propositional logics are at issue here. Such a logic is contra-classical in a superficial sense if it is not a sublogic of classical logic, and in a deeper sense, if there is no way of translating its connectives, the result of which translation gives a sublogic of classical logic. After some motivating examples, we investigate the incidence of contra-classicality (in the deeper sense) in various logical frameworks. In Sections 3 and 4 we will encounter, originally as an example of (...) what (in Section 2) we call a contra-classical modal logic, an unusual logic boasting a connective (" demi-negation" ) whose double application is equivalent to a single application of the negation connective. Pondering the example points the way to a general characterization of contra-classicality (Theorems 3.3 and 4.6). In an Appendix (Section 5), we look at one alternative to classical logic as the target for such translational assimilation, intuitionistic logic, calling logics which resist the assimilation, in this case, contra- intuitionistic. We will show that one such logic is classical logic itself, thereby strengthening a result of Wojcicki's to the effect that the consequence relation of classical logic cannot be faithfully embedded by any connective-by-connective translation into that of intuitionistic logic. (What the "faithfully" means here is that not only is the translation of anything provable in the 'source' logic.. (shrink)

Este livro marca o início da Série Investigação Filosófica. Uma série de livros de traduções de textos de plataformas internacionalmente reconhecidas, que possa servir tanto como material didático para os professores das diferentes subáreas e níveis da Filosofia quanto como material de estudo para o desenvolvimento pesquisas relevantes na área. Nós, professores, sabemos o quão difícil é encontrar bons materiais em português para indicarmos. E há uma certa deficiência na graduação brasileira de filosofia, principalmente em localizações menos favorecidas, com relação (...) ao conhecimento de outras línguas, como o inglês e o francês. Tentamos, então, suprir essa deficiência, ao introduzirmos traduções de textos importantes ao público de língua portuguesa, sem nenhuma finalidade comercial e meramente pela glória da filosofia. O presente volume é constituído de três traduções de verbetes importantes sobre lógica, da Enciclopédia de Filosofia da Stanford: (1) A Lógica de Aristóteles, (2) Lógica Clássica, (3) Lógica Modal. (shrink)

Propositional logic is understood as a set of theorems defined by a deductive system: a set of axioms and a set of rules. Superintuitionistic logic is a logic extending intuitionistic propositional logic \. A rule is admissible for a logic if any substitution that makes each premise a theorem, makes the conclusion a theorem too. A deductive system \ is structurally complete if any rule admissible for the logic defined by \ is derivable in \. It is known that any (...) logic can be defined by a structurally complete deductive system—its structural completion. The main goal of the paper is to study the following problem: given a superintuitionistic logic L, is the structural completion of L hereditarily structurally complete? It is shown that, on the one hand, there is continuum many of such logics, including \, and many of its standard extensions. On the other hand, there is continuum many superintutitionistic logics structural completion of which is not hereditarily structurally complete. It is observed that the class of hereditarily structurally complete superintuitionistic consequence relations does not have the smallest element and it contains continuum many members lacking the finite model property. The following statement is instrumental in obtaining negative results: if a Lindenbaum algebra of formulas on one variable is finite and has more than 15 elements, then a structural completion of such a logic is not hereditarily structurally complete. (shrink)

The paper presents a family of propositional epistemic logics such that languages of these logics are extended by quantification over modal operators or over agents of knowledge and extended by predicate symbols that take modal operators as arguments. Denote this family by \}\). There exist epistemic logics whose languages have the above mentioned properties :311–350, 1995; Lomuscio and Colombetti in Proceedings of ATAL 1996. Lecture Notes in Computer Science, vol 1193, pp 71–85, 1996). But these logics are obtained from first-order (...) modal logics, while a logic of \}\) can be regarded as a propositional multi-modal logic whose language includes quantifiers over modal operators and predicate symbols that take modal operators as arguments. Among the logics of \}\) there are logics with a syntactical distinction between two readings of epistemic sentences: de dicto and de re. We show the decidability of logics of \}\) with the help of the loosely guarded fragment of first-order logic. Namely, we generalize LGF to a higher-order decidable loosely guarded fragment. The latter fragment allows us to construct various decidable propositional epistemic logics with quantification over modal operators. The family of this logics coincides with \}\). There are decidable propositional logics such that these logics implicitly contain quantification over agents of knowledge, but languages of these logics are usual propositional epistemic languages without quantifiers and predicate symbols :345–378, 1993). Some logics of \}\) can be regarded as counterparts of logics defined in Grove and Halpern :345–378, 1993). We prove that the satisfiability problem for these logics of \}\) is Pspace-complete using their counterparts in Grove and Halpern :345–378, 1993). (shrink)

We show that if we interpret modal diamond as the derived set operator of a topological space, then the modal logic of Stone spaces isK4and the modal logic of weakly scattered Stone spaces isK4G. As a corollary, we obtain thatK4is also the modal logic of compact Hausdorff spaces andK4Gis the modal logic of weakly scattered compact Hausdorff spaces.

Kolmogorov introduced an informal calculus of problems in an attempt to provide a classical semantics for intuitionistic logic. This was later formalised by Medvedev and Muchnik as what has come to be called the Medvedev and Muchnik lattices. However, they only formalised this for propositional logic, while Kolmogorov also discussed the universal quantifier. We extend the work of Medvedev to first-order logic, using the notion of a first-order hyperdoctrine from categorical logic, to a structure which we will call the hyperdoctrine (...) of mass problems. We study the intermediate logic that the hyperdoctrine of mass problems gives us, and we study the theories of subintervals of the hyperdoctrine of mass problems in an attempt to obtain an analogue of Skvortsova’s result that there is a factor of the Medvedev lattice characterising intuitionistic propositional logic. Finally, we consider Heyting arithmetic in the hyperdoctrine of mass problems and prove an analogue of Tennenbaum’s theorem on computable models of arithmetic. (shrink)

In this paper we study natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T, B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple labelfree natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the subformula property in the intuitionistic case.

We prove that all extensions of Heyting Arithmetic with a logic that has the finite frame property possess the de Jongh property.

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the (...) explanation of the rules. (shrink)

Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the apparent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that (...) restricts its use to cases in which the premiss does not depend on assumptions. This restriction is entirely analogous to the restriction of the rule of universal generalization of first-order logic. A necessitation rule with this restriction permits a proof of the deduction theorem in its usual formulation. Other suggestions presented in the literature to deal with the problem are reviewed, and the present solution is argued to be preferable to the other alternatives. A contraction-and cut-free sequent calculus equivalent to the Hubert system for basic modal logic shows the standard failure argument untenable by proving the underivability of DA from A. (shrink)

This work treats the problem of axiomatizing the truth and falsity consequence relations, $ \vDash _t $ and $ \vDash _f $, determined via truth and falsity orderings on the trilattice SIXTEEN₃. The approach is based on a representation of SIXTEEN₃ as a twist-structure over the two-element Boolean algebra.

Standard models for model predicate logic consist of a Kripke frame whose worlds come equipped with relational structures. Both modal and two-sorted predicate logic are natural languages for speaking about such models. In this paper we compare their expressivity. We determine a fragment of the two-sorted language for which the modal language is expressively complete on S5-models. Decidable criteria for modal definability are presented.

If □ is conceived as an operator, i.e., an expression that gives applied to a formula another formula, the expressive power of the language is severely restricted when compared to a language where □ is conceived as a predicate, i.e., an expression that yields a formula if it is applied to a term. This consideration favours the predicate approach. The predicate view, however, is threatened mainly by two problems: Some obvious predicate systems are inconsistent, and possible-worlds semantics for predicates of (...) sentences has not been developed very far. By introducing possible-worlds semantics for the language of arithmetic plus the unary predicate □, we tackle both problems. Given a frame (W, R) consisting of a set W of worlds and a binary relation R on W, we investigate whether we can interpret □ at every world in such a way that □ $\ulcorner A \ulcorner$ holds at a world ᵆ ∊ W if and only if A holds at every world $\upsilon$ ∊ W such that ᵆR $\upsilon$ . The arithmetical vocabulary is interpreted by the standard model at every world. Several 'paradoxes' (like Montague's Theorem, Gödel's Second Incompleteness Theorem, McGee's Theorem on the ω-inconsistency of certain truth theories, etc.) show that many frames, e.g., reflexive frames, do not allow for such an interpretation. We present sufficient and necessary conditions for the existence of a suitable interpretation of □ at any world. Sound and complete semi-formal systems, corresponding to the modal systems K and K4, for the class of all possible-worlds models for predicates and all transitive possible-worlds models are presented. We apply our account also to nonstandard models of arithmetic and other languages than the language of arithmetic. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

In this paper we give an example of intertranslatability between an ontology of individuals (nominalism), an ontology of properties (realism), and an ontology of facts (factualism). We demonstrate that these three ontologies are dual to each other, meaning that each ontology can be translated into, and recaptured from, each of the others. The aiin of the enterprise is to raise the possibility that, at least in some settings, there may be no need for considerations of ontological primacy. Whether the world (...) is made up of things, or properties, or facts, may be no more than a matter of how we look at it. (shrink)

We show that the lattices of the normal extensions of four well-known logics—propositional intuitionistic logic \, Grzegorczyk logic \, modalized Heyting calculus \ and \—can be joined in a commutative diagram. One connection of this diagram is an isomorphism between the lattices of the normal extensions of \ and \; we show some preservation properties of this isomorphism. Two other connections are join semilattice epimorphims of the lattice of the normal extensions of \ onto that of \ and of the (...) lattice of the normal extensions of \ onto that of \. The link between \ and \ is a well-known isomorphism established by the Blok–Esakia theorem. (shrink)

We establish the dichotomy property for stable canonical multi-conclusion rules for IPC, K4, and S4. This yields an alternative proof of existence of explicit bases of admissible rules for these logics.

Skvortsova showed that there is a factor of the Medvedev lattice which captures intuitionistic propositional logic (IPC). However, her factor is unnatural in the sense that it is constructed in an ad hoc manner. We present a more natural example of such a factor. We also show that the theory of every non-trivial factor of the Medvedev lattice is contained in Jankov’s logic, the deductive closure of IPC plus the weak law of the excluded middle $${\neg p \vee \neg \neg (...) p}$$. This answers a question by Sorbi and Terwijn. (shrink)

In this paper we study the expressive power and definability for modal languages interpreted on topological spaces. We provide topological analogues of the van Benthem characterization theorem and the Goldblatt–Thomason definability theorem in terms of the well-established first-order topological language.

MIPC is a well-known intuitionistic modal logic of Prior and Bull . It is shown that every normal intuitionistic modal logic L over MIPC has the finite model property whenever L is Kripke-complete and universal.

Our investigation is concerned with the finite model property with respect to admissible rules. We establish general sufficient conditions for absence of fmp w. r. t. admissibility which are applicable to modal logics containing K4: Theorem 3.1 says that no logic λ containing K4 with the co-cover property and of width > 2 has fmp w. r. t. admissibility. Surprisingly many, if not to say all, important modal logics of width > 2 are within the scope of this theorem–K4 itself, (...) S4, GL, K4.1, K4.2, S4.1, S4.2, GL.2, etc. Thus the situation is completely opposite to the case of the ordinary fmp–the absolute majority of important logics have fmp, but not with respect to admissibility. As regards logics of width ≤ 2, there exists a zone for fmp w. r. t. admissibility. It is shown that all modal logics A of width ≤ 2 extending S4 which are not sub-logics of three special tabular logics have fmp w.r.t. admissibility. (shrink)

This paper partly answers the question “what a frame may be exactly like when it characterizes a pretabular logic in NExtK4”. We prove the pretabularity crieria for the logics of finite depth in NExtK4. In order to find out the criteria, we create two useful concepts—“pointwise reduction” and “invariance under pointwise reductions”, which will remain important in dealing with the case of infinite depth.

Earlier algebraic semantics for Belnapian modal logics were defined in terms of twist-structures over modal algebras. In this paper we introduce the class of BK -lattices, show that this class coincides with the abstract closure of the class of twist-structures, and it forms a variety. We prove that the lattice of subvarieties of the variety of BK -lattices is dually isomorphic to the lattice of extensions of Belnapian modal logic BK . Finally, we describe invariants determining a twist-structure over a (...) modal algebra. (shrink)

The aim of this paper is to give new kinds of modal logics suitable for reasoning about regions in discrete spaces. We call them dynamic logics of the region-based theory of discrete spaces. These modal logics are linguistic restrictions of propositional dynamic logic with the global diamond E. Their formulas are equivalent to Boolean combinations of modal formulas like E(A ∧ ⟨α⟩ B) where A and B are Boolean terms and α is a relational term. Examining what we can say (...) about dynamic models when we use formulas to describe them, we successively address the axiomatization/completeness issue and the decidability/complexity issue of our dynamic logics of the region-based theory of discrete spaces. (shrink)

ABSTRACT The paper studies propositional logics in a bimodal language, in which the first modality is interpreted as the local truth, and the second as the universal truth. The logic S4UC is introduced, which is finitely axiomatizable, has the f.m.p. and is determined by every connected separable metric space.

A logic is called metacomplete if formulas that are true in a certain preferred interpretation of that logic are theorems in its metalogic. In the area of relevant logics, metacompleteness is used to prove primeness, consistency, the admissibility of γ and so on. This paper discusses metacompleteness and its applications to a wider class of modal logics based on contractionless relevant logics and their neighbours using Slaney’s metavaluational technique.

We prove strong completeness of the □-version and the ◊-version of a Gödel modal logic based on Kripke models where propositions at each world and the accessibility relation are both infinitely valued in the standard Gödel algebra [0,1]. Some asymmetries are revealed: validity in the first logic is reducible to the class of frames having two-valued accessibility relation and this logic does not enjoy the finite model property, while validity in the second logic requires truly fuzzy accessibility relations and this (...) logic has the finite model property. Analogues of the classical modal systems D, T, S4 and S5 are considered also, and the completeness results are extended to languages enriched with a discrete well ordered set of truth constants. (shrink)

This work treats the problem of axiomatizing the truth and falsity consequence relations, ⊨ t and ⊨ f, determined via truth and falsity orderings on the trilattice SIXTEEN 3 (Shramko and Wansing, 2005). The approach is based on a representation of SIXTEEN 3 as a twist-structure over the two-element Boolean algebra.

This paper investigates a generalized version of inquisitive semantics. A complete axiomatization of the associated logic is established, the connection with intuitionistic logic and several intermediate logics is explored, and the generalized version of inquisitive semantics is argued to have certain advantages over the system that was originally proposed by Groenendijk (2009) and Mascarenhas (2009).

In a previous work we introduced the algorithm \SQEMA\ for computing first-order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of (...) \SQEMA\ where that syntactic condition is replaced by a semantic one, viz. downward monotonicity. For the first, and most general, extension \SSQEMA\ we prove correctness for a large class of modal formulae containing an extension of the Sahlqvist formulae, defined by replacing polarity with monotonicity. By employing a special modal version of Lyndon's monotonicity theorem and imposing additional requirements on the Ackermann rule we obtain restricted versions of \SSQEMA\ which guarantee canonicity, too. (shrink)

In the paper we consider complexity of intuitionistic propositional logic and its natural fragments such as implicative fragment, finite-variable fragments, and some others. Most facts we mention here are known and obtained by logicians from different countries and in different time since 1920s; we present these results together to see the whole picture.

The modal logic of Gödel sentences, termed as GS, is introduced to analyze the logical properties of 'true but unprovable' sentences in formal arithmetic. The logic GS is, in a sense, dual to Grzegorczyk's Logic, where modality can be interpreted as 'true and provable'. As we show, GS and Grzegorczyk's Logic are, in fact, mutually embeddable. We prove Kripke completeness and arithmetical completeness for GS. GS is also an extended system of the logic of 'Essence and Accident' proposed by Marcos (...) (Bull Sect Log 34(1):43-56, 2005). We also clarify the relationships between GS and the provability logic GL and between GS and Intuitionistic Propositional Logic. (shrink)

The literature on quantum logic emphasizes that the algebraic structures involved with orthodox quantum mechanics are non distributive. In this paper we develop a particular algebraic structure, the quasi-lattice ( $${\mathfrak{I}}$$ -lattice), which can be modeled by an algebraic structure built in quasi-set theory $${\mathfrak{Q}}$$. This structure is non distributive and involve indiscernible elements. Thus we show that in taking into account indiscernibility as a primitive concept, the quasi-lattice that ‘naturally’ arises is non distributive.

Since 1993, when Hudelmaier developed an O(n log n)-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and Fc with a new set of rules to treat signed formulas of the kind T((A → B) → C) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search and the (...) width of proofs with respect to Hudelmaier's one. These improvements have a significant influence on the performances of the implementation. (shrink)

The trilattice SIXTEEN3 introduced in Shramko & Wansing (2005) is a natural generalization of the famous bilattice FOUR2. Some Hilbert-style proof systems for trilattice logics related to SIXTEEN3 have recently been studied (Odintsov, 2009; Shramko & Wansing, 2005). In this paper, three sequent calculi GB, FB, and QB are presented for Odintsovs coordinate valuations associated with valuations in SIXTEEN3. The equivalence between GB, FB, and QB, the cut-elimination theorems for these calculi, and the decidability of B are proved. In addition, (...) it is shown how the sequent systems for B can be extended to cut-free sequent calculi for Odintsov’s LB, which is an extension of B by adding classical implication and negation connectives. (shrink)

This paper presents a generalization of Fine’s completeness theorem for transitive logics of finite width, and proves the Kripke completeness of transitive logics of finite “suc-eq-width”. The frame condition for each finite suc-eq-width axiom requires, in rooted transitive frames, a finite upper bound of cardinality for antichains of points with different proper successors. The paper also presents a generalization of Rybakov’s completeness theorem for transitive logics of prefinite width, and proves the Kripke completeness of transitive logics of prefinite “suc-eq-width”. The (...) frame condition for each prefinite suc-eq-width axiom requires, in rooted transitive frames, a finite upper bound of cardinality for antichains of points that have a finite lower bound of depth and have different proper successors. We will construct continuums of transitive logics of finite suc-eq-width but not of finite width, and continuums of those of prefinite suc-eq-width but not of prefinite width. This shows that our new completeness results cover uncountably many more logics than Fine’s theorem and Rybakov’s theorem respectively. (shrink)

S4.2 is the modal logic of directed partial pre-orders and/or the modal logic of reflexive and transitive relational frames with a final cluster. It holds a distinguished position in philosophical...