Expressing Second-order Sentences in Intuitionistic Dependence Logic

Intuitionistic dependence logic was introduced by Abramsky and Väänänen [1] as a variant of dependence logic under a general construction of Hodges’ (trump) team semantics. It was proven that there is a translation from intuitionistic dependence logic sentences into second order logic sentences. In this paper, we prove that the other direction is also true, therefore intuitionistic dependence logic is equivalent to second order logic on the level of sentences.     

Compositional Natural Language Semantics using Independence Friendly Logic or Dependence Logic

Independence Friendly Logic, introduced by Hintikka, is a logic in which a quantifier can be marked for being independent of other quantifiers. Dependence logic, introduced by Väänänen, is a logic with the complementary approach: for a quantifier it can be indicated on which quantifiers it depends. These logics are claimed to be useful for many phenomena, for instance natural language semantics. In this contribution we will compare these two logics by investigating their application in a compositional analysis of the de dicto - de re ambiguity in natural language. It will be argued that Independence Friendly logic is suitable, whereas Dependence Logic is not.     

From IF to BI

We take a fresh look at the logics of informational dependence and independence of Hintikka and Sandu and Väänänen, and their compositional semantics due to Hodges. We show how Hodges’ semantics can be seen as a special case of a general construction, which provides a context for a useful completeness theorem with respect to a wider class of models. We shed some new light on each aspect of the logic. We show that the natural propositional logic carried by the semantics is the logic of Bunched Implications due to Pym and O’Hearn, which combines intuitionistic and multiplicative connectives. This introduces several new connectives not previously considered in logics of informational dependence, but which we show play a very natural rôle, most notably intuitionistic implication. As regards the quantifiers, we show that their interpretation in the Hodges semantics is forced, in that they are the image under the general construction of the usual Tarski semantics; this implies that they are adjoints to substitution, and hence uniquely determined. As for the dependence predicate, we show that this is definable from a simpler predicate, of constancy or dependence on nothing. This makes essential use of the intuitionistic implication. The Armstrong axioms for functional dependence are then recovered as a standard set of axioms for intuitionistic implication. We also prove a full abstraction result in the style of Hodges, in which the intuitionistic implication plays a very natural rôle.     

Epistemic Operators in Dependence Logic

The properties of the ${\forall^{1}}$ quantifier defined by Kontinen and Väänänen in [13] are studied, and its definition is generalized to that of a family of quantifiers ${\forall^{n}}$ . Furthermore, some epistemic operators δ ⁿ for Dependence Logic are also introduced, and the relationship between these ${\forall^{n}}$ quantifiers and the δ ⁿ operators are investigated. The Game Theoretic Semantics for Dependence Logic and the corresponding Ehrenfeucht- Fraissé game are then adapted to these new connectives. Finally, it is proved that the ${\forall^{1}}$ quantifier is not uniformly definable in Dependence Logic, thus answering a question posed by Kontinen and Väänänen in the above mentioned paper.     

Two notions of compactness in Gödel logics

Compactness is an important property of classical propositional logic. It can be defined in two equivalent ways. The first one states that simultaneous satisfiability of an infinite set of formulae is equivalent to the satisfiability of all its finite subsets. The second one states that if a set of formulae entails a formula, then there is a finite subset entailing this formula as well.In propositional many-valued logic, we have different degrees of satisfiability and different possible definitions of entailment, hence the questions of compactness is more complex. In this paper we will deal with compactness of Gödel, Gödel_Δ, and Gödel_～ logics.There are several results (all for the countable set of propositional variables) concerning the compactness (based on satisfiability) of these logic by Cintula and Navara, and the question of compactness (based on entailment) for Gödel logic was fully answered by Baaz and Zach (see papers [3] and [2]).In this paper we give a nearly complete answer to the problem of compactness based on both concepts for all three logics and for an arbitrary cardinality of the set of propositional variables. Finally, we show a tight correspondence between these two concepts     

IF Modal Logic and Classical Negation

The present paper provides novel results on the model theory of Independence friendly modal logic. We concentrate on its particularly well-behaved fragment that was introduced in Tulenheimo and Sevenster (Advances in Modal Logic, 2006). Here we refer to this fragment as ‘Simple IF modal logic’ (IFML _s ). A model-theoretic criterion is presented which serves to tell when a formula of IFML _s is not equivalent to any formula of basic modal logic (ML). We generalize the notion of bisimulation familiar from ML; the resulting asymmetric simulation concept is used to prove that IFML _s is not closed under complementation. In fact we obtain a much stronger result: the only IFML _s formulas admitting their classical negation to be expressed in IFML _s itself are those whose truth-condition is in fact expressible in ML.     

Three-valued Logics in Modal Logic

Every truth-functional three-valued propositional logic can be conservatively translated into the modal logic S5. We prove this claim constructively in two steps. First, we define a Translation Manual that converts any propositional formula of any three-valued logic into a modal formula. Second, we show that for every S5-model there is an equivalent three-valued valuation and vice versa. In general, our Translation Manual gives rise to translations that are exponentially longer than their originals. This fact raises the question whether there are three-valued logics for which there is a shorter translation into S5. The answer is affirmative: we present an elegant linear translation of the Logic of Paradox and of Strong Three-valued Logic into S5.     

Extending Łukasiewicz Logics with a Modality: Algebraic Approach to Relational Semantics

This paper presents an algebraic approach of some many-valued generalizations of modal logic. The starting point is the definition of the [0, 1]-valued Kripke models, where [0, 1] denotes the well known MV-algebra. Two types of structures are used to define validity of formulas: the class of frames and the class of ? _n -valued frames. The latter structures are frames in which we specify in each world u the set (a subalgebra of ? _n ) of the allowed truth values of the formulas in u. We apply and develop algebraic tools (namely, canonical and strong canonical extensions) to generate complete modal n + 1-valued logics and we obtain many-valued counterparts of Shalqvist canonicity result.     

Deductive temporal reasoning with constraints

When modelling realistic systems, physical constraints on the resources available are often required. For example, we might say that at most N processes can access a particular resource at any moment, exactly M participants are needed for an agreement, or an agent can be in exactly one mode at any moment. Such situations are concisely modelled where literals are constrained such that at most N, or exactly M, can hold at any moment in time. In this paper we consider a logic which is a combination of standard propositional linear time temporal logic with cardinality constraints restricting the numbers of literals that can be satisfied at any moment in time. We present the logic and show how to represent a number of case studies using this logic. We propose a tableau-like algorithm for checking the satisfiability of formulae in this logic, provide details of a prototype implementation and present experimental results using the prover.     

Ideal Paraconsistent Logics

We define in precise terms the basic properties that an ??ideal propositional paraconsistent logic?? is expected to have, and investigate the relations between them. This leads to a precise characterization of ideal propositional paraconsistent logics. We show that every three-valued paraconsistent logic which is contained in classical logic, and has a proper implication connective, is ideal. Then we show that for every n > 2 there exists an extensive family of ideal n-valued logics, each one of which is not equivalent to any k-valued logic with k < n.     

Automorphisms of the Lattice of Classical Modal Logics

In this paper we analyze the propositional extensions of the minimal classical modal logic system E, which form a lattice denoted as CExtE. Our method of analysis uses algebraic calculations with canonical forms, which are a generalization of the normal forms applicable to normal modal logics. As an application, we identify a group of automorphisms of CExtE that is isomorphic to the symmetric group S₄.     

A cut-free gentzen-type system for the logic of the weak law of excluded middle

The logic of the weak law of excluded middleKC _p is obtained by adding the formula A A as an axiom scheme to Heyting's intuitionistic logicH _p . A cut-free sequent calculus for this logic is given. As the consequences of the cut-elimination theorem, we get the decidability of the propositional part of this calculus, its separability, equality of the negationless fragments ofKC _p andH _p , interpolation theorems and so on. From the proof-theoretical point of view, the formulation presented in this paper makes clearer the relations betweenKC _p ,H _p , and the classical logic. In the end, an interpretation of classical propositional logic in the propositional part ofKC _p is given.     

Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)

We present a coinductive definition of models for modal logics and show that it provides a homogeneous framework in which it is possible to include different modal languages ranging from classical modalities to operators from hybrid and memory logics. Moreover, results that had to be proved separately for each different language—but whose proofs were known to be mere routine—now can be proved in a general way. We show, for example, that we can have a unique definition of bisimulation for all these languages, and prove a single invariance-under-bisimulation theorem.We then use the new framework to investigate normal forms for modal logics. The normal form we introduce may have a smaller modal depth than the original formula, and it is inspired by global modalities like the universal modality and the satisfiability operator from hybrid logics. These modalities can be extracted from under the scope of other operators. We provide a general definition of extractable modalities and show how to compute extracted normal forms. As it is the case with other classical normal forms—e.g., the conjunctive normal form of propositional logic—the extracted normal form of a formula can be exponentially bigger than the original formula, if we require the two formulas to be equivalent. If we only require equi-satisfiability, then every modal formula has an extracted normal form which is only polynomially bigger than the original formula, and it can be computed in polynomial time.     

Actuality in Propositional Modal Logic

We show that the actuality operator A is redundant in any propositional modal logic characterized by a class of Kripke models (respectively, neighborhood models). Specifically, we prove that for every formula ${\phi}$ in the propositional modal language with A, there is a formula ${\psi}$ not containing A such that ${\phi}$ and ${\psi}$ are materially equivalent at the actual world in every Kripke model (respectively, neighborhood model). Inspection of the proofs leads to corresponding proof-theoretic results concerning the eliminability of the actuality operator in the actuality extension of any normal propositional modal logic and of any “classical” modal logic. As an application, we provide an alternative proof of a result of Williamson’s to the effect that the compound operator A□ behaves, in any normal logic between T and S5, like the simple necessity operator □ in S5.     

The Decision Problem of Modal Product Logics with a Diagonal,and Faulty Counter Machines

In the propositional modal (and algebraic) treatment of two-variable first-order logic equality is modelled by a ‘diagonal’ constant, interpreted in square products of universal frames as the identity (also known as the ‘diagonal’) relation. Here we study the decision problem of products of two arbitrary modal logics equipped with such a diagonal. As the presence or absence of equality in two-variable first-order logic does not influence the complexity of its satisfiability problem, one might expect that adding a diagonal to product logics in general is similarly harmless. We show that this is far from being the case, and there can be quite a big jump in complexity, even from decidable to the highly undecidable. Our undecidable logics can also be viewed as new fragments of first-order logic where adding equality changes a decidable fragment to undecidable. We prove our results by a novel application of counter machine problems. While our formalism apparently cannot force reliable counter machine computations directly, the presence of a unique diagonal in the models makes it possible to encode both lossy and insertion-error computations, for the same sequence of instructions. We show that, given such a pair of faulty computations, it is then possible to reconstruct a reliable run from them.     

A Generalization of Inquisitive Semantics

This paper introduces a generalized version of inquisitive semantics, denoted as GIS, and concentrates especially on the role of disjunction in this general framework. Two alternative semantic conditions for disjunction are compared: the first one corresponds to the so-called tensor operator of dependence logic, and the second one is the standard condition for inquisitive disjunction. It is shown that GIS is intimately related to intuitionistic logic and its Kripke semantics. Using this framework, it is shown that the main results concerning inquisitive semantics, especially the axiomatization of inquisitive logic, can be viewed as particular cases of more general phenomena. In this connection, a class of non-standard superintuitionistic logics is introduced and studied. These logics share many interesting features with inquisitive logic, which is the strongest logic of this class.     

The Greatest Extension of S4 into which Intuitionistic Logic is Embeddable

This paper gives a characterization of those quasi-normal extensions of the modal system S4 into which intuitionistic propositional logic Int is embeddable by the Gödel translation. It is shown that, as in the normal case, the set of quasi-normal modal companions of Int contains the greatest logic, M*, for which, however, the analog of the Blok-Esakia theorem does not hold. M* is proved to be decidable and Halldén-complete; it has the disjunction property but does not have the finite model property.     

Decidability of Quantified Propositional Intuitionistic Logic and S4 on Trees of Height and Arity ≤ω

Quantified propositional intuitionistic logic is obtained from propositional intuitionistic logic by adding quantifiers p, p, where the propositional variables range over upward-closed subsets of the set of worlds in a Kripke structure. If the permitted accessibility relations are arbitrary partial orders, the resulting logic is known to be recursively isomorphic to full second-order logic (Kremer, 1997). It is shown that if the Kripke structures are restricted to trees of at height and width at most , the resulting logics are decidable. This provides a partial answer to a question by Kremer. The result also transfers to modal S4 and some Gödel–Dummett logics with quantifiers over propositions.