Search

This work presents a proof-theoretical and model-theoretical approach to probabilistic temporal logic. We present two novel logics; each of them extends both the language of linear time logic (LTL) and the language of probabilistic logic with polynomial weight formulas. The first logic is designed for reasoning about probabilities of temporal events, allowing statements like "the probability that A will hold in next moment is at least the probability that B will always hold" and conditional probability statements like "probability that A will always hold, given that B holds, is at least one half", where A and B are arbitrary statements. We axiomatize this logic, provide corresponding sigma additive semantics and prove that the axiomatization is sound and strongly complete. We show that the satisfiability problem for our logic is decidable, by presenting a procedure which runs in polynomial space. We also present a logic with much richer language, in which probabilities are not attached only to temporal events, but the language allows arbitrary nesting of probability and temporal operators, allowing statements like "probability that tomorrow the chance of rain will be less than 80% is at least a half". For this logic we prove a decidability result. [ABSTRACT FROM AUTHOR]

It is well known that the completeness theorem for L ω 1 ω fails with respect to Tarski semantics. Mansfield showed that it holds for L ∞ ∞ if one replaces Tarski semantics with Boolean valued semantics. We use forcing to improve his result in order to obtain a stronger form of Boolean completeness (but only for L ∞ ω). Leveraging on our completeness result, we establish the Craig interpolation property and a strong version of the omitting types theorem for L ∞ ω with respect to Boolean valued semantics. We also show that a weak version of these results holds for L ∞ ∞ (if one leverages instead on Mansfield's completeness theorem). Furthermore we bring to light (or in some cases just revive) several connections between the infinitary logic L ∞ ω and the forcing method in set theory. [ABSTRACT FROM AUTHOR]

Hintikka and Sandu originally proposed Independence Friendly Logic (▪) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantics of natural language. The logic allows for expressing independence constraints among quantified variables, in a similar vein to Henkin quantifiers, and has a nice game-theoretic semantics in terms of imperfect information games. However, the ▪ semantics exhibits some limitations, at least from a purely logical perspective. It treats the players asymmetrically, considering only one of the two players as having imperfect information when evaluating truth, resp. , falsity, of a sentence. In addition, truth and falsity of sentences coincide with the existence of a uniform winning strategy for one of the two players in the semantic imperfect information game. As a consequence, ▪ does admit undetermined sentences, which are neither true nor false, thus failing the law of excluded middle. These idiosyncrasies limit its expressive power to the existential fragment of Second Order Logic (▪). In this paper, we investigate an extension of ▪, called Alternating Dependence/Independence Friendly Logic (▪), tailored to overcome these limitations. To this end, we introduce a novel compositional semantics , generalising the one based on trumps proposed by Hodges for ▪. The new semantics (i) allows for meaningfully restricting both players at the same time, (ii) enjoys the property of game-theoretic determinacy, (iii) recovers the law of excluded middle for sentences, and (iv) grants ▪ the full descriptive power of ▪. We also provide an equivalent Herbrand-Skolem semantics and a game-theoretic semantics for the prenex fragment of ▪, the latter being defined in terms of a determined infinite-duration game that precisely captures the other two semantics on finite structures. [ABSTRACT FROM AUTHOR]

In this paper we study the expressive power of k -ary exclusion logic, EXC[ k ], that is obtained by extending first order logic with k -ary exclusion atoms. It is known that without arity bounds exclusion logic is equivalent with dependence logic. By observing the translations, we see that the expressive power of EXC[ k ] lies in between k -ary and (k + 1)-ary dependence logics. We will show that, at least in the case when k = 1 , both of these inclusions are proper. In a recent work by the author it was shown that k -ary inclusion-exclusion logic is equivalent with k -ary existential second order logic, ESO[ k ]. We will show that, on the level of sentences, it is possible to simulate inclusion atoms with exclusion atoms, and in this way express ESO[ k ]-sentences by using only k -ary exclusion atoms. For this translation we also need to introduce a novel method for "unifying" the values of certain variables in a team. As a consequence, EXC[ k ] captures ESO[ k ] on the level of sentences, and we obtain a strict arity hierarchy for exclusion logic. It also follows that k -ary inclusion logic is strictly weaker than EXC[ k ]. Finally we use similar techniques to formulate a translation from ESO[ k ] to k -ary inclusion logic with an alternative strict semantics. Consequently, for any arity fragment of inclusion logic, strict semantics is strictly more expressive than lax semantics. [ABSTRACT FROM AUTHOR]

Probabilistic team semantics is a framework for logical analysis of probabilistic dependencies. Our focus is on the axiomatizability, complexity, and expressivity of probabilistic inclusion logic and its extensions. We identify a natural fragment of existential second-order logic with additive real arithmetic that captures exactly the expressivity of probabilistic inclusion logic. We furthermore relate these formalisms to linear programming, and doing so obtain PTIME data complexity for the logics. Moreover, on finite structures, we show that the full existential second-order logic with additive real arithmetic can only express NP properties. Lastly, we present a sound and complete axiomatization for probabilistic inclusion logic at the atomic level. [ABSTRACT FROM AUTHOR]

This article provides an algebraic study of intermediate inquisitive and dependence logics. While these logics are usually investigated using team semantics, here we introduce an alternative algebraic semantics and we prove it is complete for all intermediate inquisitive and dependence logics. To this end, we define inquisitive and dependence algebras and we investigate their model-theoretic properties. We then focus on finite, core-generated, well-connected inquisitive and dependence algebras: we show they witness the validity of formulas true in inquisitive algebras, and of formulas true in well-connected dependence algebras. Finally, we obtain representation theorems for finite, core-generated, well-connected, inquisitive and dependence algebras and we prove some results connecting team and algebraic semantics. [ABSTRACT FROM AUTHOR]

Separation logic is a successful logical system for formal reasoning about programs that mutate their data structures. Team semantics, on the other side, is the basis of modern logics of dependence and independence. Separation logic and team semantics have been introduced with quite different motivations, and are investigated by research communities with rather different backgrounds and objectives. Nevertheless, there are obvious similarities between these formalisms. Both separation logic and logics with team semantics involve the manipulation of second-order objects, such as heaps and teams, by first-order syntax without reference to second-order variables. Moreover, these semantical objects are closely related; it is for instance obvious that a heap can be seen as a team, and the separating conjunction of separation logic is (essentially) the same as the team-semantical disjunction. Based on such similarities, the possible connections between separation logic and team semantics have been raised as a question at several occasions, and lead to informal discussions between these research communities. The objective of this paper is to make this connection precise, and to study its potential but also its obstacles and limitations. [ABSTRACT FROM AUTHOR]

In team semantics, which is the basis of modern logics of dependence and independence, formulae are evaluated on sets of assignments, called teams. Multiteam semantics instead takes mulitplicities of data into account and is based on multisets of assignments, called multiteams. Logics with multiteam semantics can be embedded into a two-sorted variant of existential second-order logics, with arithmetic operations on multiplicities. Here we study the Presburger fragment of such logics, permitting only addition, but not multiplication on multiplicities. It can be shown that this fragment corresponds to inclusion-exclusion logic in multiteam semantics, but, in contrast to the situation in team semantics, that it is strictly contained in independence logic. We give different characterisations of this fragment by various atomic dependency notions. [ABSTRACT FROM AUTHOR]

Abstract: In the present paper, we start studying epistemic updates using the standard toolkit of duality theory. We focus on public announcements, which are the simplest epistemic actions, and hence on Public Announcement Logic (PAL) without the common knowledge operator. As is well known, the epistemic action of publicly announcing a given proposition is semantically represented as a transformation of the model encoding the current epistemic setup of the given agents; the given current model being replaced with its submodel relativized to the announced proposition. We dually characterize the associated submodel-injection map as a certain pseudo-quotient map between the complex algebras respectively associated with the given model and with its relativized submodel. As is well known, these complex algebras are complete atomic BAOs (Boolean algebras with operators). The dual characterization we provide naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras (HAOs). Thanks to this construction, the benefits and the wider scope of applications given by a point-free, intuitionistic theory of epistemic updates are made available. As an application of this dual characterization, we axiomatize the intuitionistic analogue of PAL, which we refer to as IPAL, prove soundness and completeness of IPAL w.r.t. both algebraic and relational models, and show that the well known Muddy Children Puzzle can be formalized in IPAL. [Copyright &y& Elsevier]

We present a setting in which the search for a proof of or a refutation of (i.e., a proof of ) can be carried out simultaneously: in contrast, the usual approach in automated deduction views proving or proving as two, possibly unrelated, activities. Our approach to proof and refutation is described as a two-player game in which each player follows the same rules. A winning strategy translates to a proof of the formula and a counter-winning strategy translates to a refutation of the formula. The game is described for multiplicative and additive linear logic (MALL). A game theoretic treatment of the multiplicative connectives is intricate and our approach to it involves two important ingredients. First, labeled graph structures are used to represent positions in a game and, second, the game playing must deal with the failure of a given player and with an appropriate resumption of play. This latter ingredient accounts for the fact that neither player might win (that is, neither nor might be provable). [Copyright &y& Elsevier]

Abstract: We tackle the problem of preservation of totality by composition in arena games. We first explain how this problem reduces to a finiteness theorem on what we call pointer structures, similar to the parity pointer functions of Harmer, Hyland & Melliès and the interaction sequences of Coquand. We discuss how this theorem relates to normalization of linear head reduction in simply-typed -calculus, leading us to a semantic realizability proof à la Kleene of our theorem. We then present another proof of a more combinatorial nature. Finally, we discuss the exact class of strategies to which our theorems apply. [Copyright &y& Elsevier]

Abstract: The description of resources in game semantics has never achieved the simplicity and precision of linear logic, because of the misleading conception that linear logic is more primitive than game semantics. Here, we defend the opposite view, and thus advocate that game semantics is conceptually more primitive than linear logic. This revised point of view leads us to introduce tensor logic, a primitive variant of linear logic where negation is not involutive. After formulating its categorical semantics, we interpret tensor logic in a model based on Conway games equipped with a notion of payoff, in order to reflect the various resource policies of the logic: linear, affine, relevant or exponential. [Copyright &y& Elsevier]

Abstract: In this paper, we introduce a new approach to independent quantifiers, as originally introduced in Informational independence as a semantic phenomenon by Hintikka and Sandu (1989) under the header of independence-friendly (IF) languages. Unlike other approaches, which rely heavily on compositional methods, we shall analyze independent quantifiers via equilibriums in strategic games. In this approach, coined equilibrium semantics, the value of an IF sentence on a particular structure is determined by the expected utility of the existential player in any of the game’s equilibriums. This approach was suggested in Henkin quantifiers and complete problems by Blass and Gurevich (1986) but has not been taken up before. We prove that each rational number can be realized by an IF sentence. We also give a lower and upper bound on the expressive power of IF logic under equilibrium semantics. [Copyright &y& Elsevier]

Abstract: This paper studies the complexity of behavior of multi-agent systems. Behavior properties are formulated using classical temporal logic languages and are checked with respect to the transition system induced by the definition of the multi-agent system. We establish various tight complexity bounds of the behavior properties under natural structural and semantic restrictions on agent programs and actions. [Copyright &y& Elsevier]

A new semantics is presented for the logic of proofs (LP), (Technical Report MSI 95-29, Cornell University (1995), Bull. Symbolic Logic 7 (2001) 1) based on the intuition that it is a logic of explicit knowledge. This semantics is used to give new proofs of several basic results concerning LP. In particular, the realization of S4 into LP is established in a way that carefully examines and explicates the role of the + operator. Finally connections are made with the conventional approach, via soundness and completeness results. [Copyright &y& Elsevier]

Contacts of the two logicians are listed, and all Go¨del's written mentions of Tarski's work are quoted. Why did Go¨del almost never mention Tarski's definition of truth in his notes and papers? This puzzle of Go¨del's silence, proposed by Feferman, is not merely biographical or psychological but has interesting connections to Go¨del's philosophical views.No satisfactory answer is given by the three “standard” explanations: (i) no need to repeat the work already done; (ii) Tarski's achievement was obvious to Go¨del; (iii) Go¨del's exceptional caution. In fact, (i), Tarski had done the work, but Go¨del almost never mentioned the achievement; (ii), the obviousness is no explanation for the omission of Tarski's work in contexts in which an application of the definition of satisfaction was useful, and even necessary; (iii), the point was not just caution: if Go¨del had felt the need to mention the program of scientific semantics he could easily have done that in his manuscripts, or in conversations.Three ideas, detectable in Go¨del's approach, can help us understand Go¨del's silence: (A) the idea of truth as the intuitive provability in the most general sense; defining it set-theoretically would contribute nothing. (B) the idea of truth as an inexhaustible idea in the sense of Kant; “truth in general” is a category that must be applicable to all kinds of sentential expressions; also, while for Go¨del language was secondary, Tarski's definition is focused on language. (C) the idea of logic as the universal language, in Hintikka's sense, as opposed to the perception of logic as a reinterpretable calculus; hence the thesis that semantics is inexpressible. Go¨del always remains a Platonist who asks a natural question: what does really happen in the realm of abstract objects? [Copyright &y& Elsevier]

We study propositional probabilistic logics (LPP –logics) with probability operators of the form P ≥ r ("the probability is at least r ") with σ –additive semantics. For regular infinite cardinals κ and λ , the probabilistic logic L P P κ , λ has λ propositional variables, allows conjunctions of < κ formulas, and allows iterations of probability operators. L P P κ , λ , 2 denotes the fragment of L P P κ , λ where iterations of probability operators is not allowed. Besides the well known non-compactness of LPP –logics, we show that L P P κ , λ , 2 –logics are not countably compact for any λ ≥ ω 1 and any κ , and that are not 2 ℵ 0 + –compact for κ ≥ ω 1 and any λ. We prove the equivalence of our adaptation of the Hoover's continuity rule (Rule (5) in [13]) and Goldblat's Countable Additivity Rule [9] and show their necessity for complete axiomatization with respect to the class of all σ –additive models. The main result is the strong completeness theorem for countable fragments L P P A and L P P A , 2 of L P P ω 1 , ω. [ABSTRACT FROM AUTHOR]