Tractability Frontiers in Probabilistic Team Semantics and Existential Second-Order Logic over the Reals

Team semantics is the mathematical basis of modern logics of dependence and independence. In contrast to classical Tarski semantics, a formula is evaluated not for a single assignment of values to the free variables, but on a set of such assignments, called a team. Team semantics is appropriate for a purely logical understanding of dependency notions, where only the presence or absence of data matters, but being based on sets, it does not take into account multiple occurrences of data values. It is therefore insufficient in scenarios where such multiplicities matter, in particular for reasoning about probabilities and statistical independencies. Therefore, an extension from teams to multiteams (i.e. multisets of assignments) has been proposed by several authors. In this paper we aim at a systematic development of logics of dependence and independence based on multiteam semantics. We study atomic dependency properties of finite multiteams and discuss the appropriate meaning of logical operators to extend the atomic dependencies to full-fledged logics for reasoning about dependence properties in a multiteam setting. We explore properties and expressive power of a wide spectrum of different multiteam logics and compare them to second-order logic and to logics with team semantics. In many cases the results resemble what is known in team semantics, but there are also interesting differences. While in team semantics, the combination of inclusion and exclusion dependencies leads to a logic with the full power of both independence logic and existential second-order logic, independence properties of multiteams are not definable by any combination of properties that are downwards closed or union closed and thus are strictly more powerful than inclusion-exclusion logic. We also study the relationship of logics with multiteam semantics with existential second-order logic for a specific class of metafinite structures. It turns out that inclusion-exclusion logic can be characterised in a precise sense by the Presburger fragment of this logic, but for capturing independence, we need to go beyond it and add some form of multiplication. Finally, we also consider multiteams with weights in the reals and study the expressive power of formulae by means of topological properties.

Download Full-text

On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics

Logical Methods in Computer Science ◽

10.46298/lmcs-17(3:14)2021 ◽

2021 ◽

Vol Volume 17, Issue 3 ◽

Author(s):

Matthias Hoelzel ◽

Richard Wilke

Keyword(s):

Normal Form ◽

Second Order ◽

Order Logic ◽

First Order Logic ◽

First Order ◽

Team Semantics ◽

Key Factor ◽

Undecidable Property ◽

Open Question ◽

Second Order Logic

We present syntactic characterisations for the union closed fragments of existential second-order logic and of logics with team semantics. Since union closure is a semantical and undecidable property, the normal form we introduce enables the handling and provides a better understanding of this fragment. We also introduce inclusion-exclusion games that turn out to be precisely the corresponding model-checking games. These games are not only interesting in their own right, but they also are a key factor towards building a bridge between the semantic and syntactic fragments. On the level of logics with team semantics we additionally present restrictions of inclusion-exclusion logic to capture the union closed fragment. Moreover, we define a team based atom that when adding it to first-order logic also precisely captures the union closed fragment of existential second-order logic which answers an open question by Galliani and Hella.

Download Full-text

Categoricity and the sets

10.1093/oso/9780198790396.003.0008 ◽

2018 ◽

Author(s):

Tim Button ◽

Sean Walsh

Keyword(s):

Set Theory ◽

Second Order ◽

Order Logic ◽

First Order ◽

The Status ◽

Second Order Logic ◽

Philosophy Of Set Theory ◽

Order Set

In this chapter, the focus shifts from numbers to sets. Again, no first-order set theory can hope to get anywhere near categoricity, but Zermelo famously proved the quasi-categoricity of second-order set theory. As in the previous chapter, we must ask who is entitled to invoke full second-order logic. That question is as subtle as before, and raises the same problem for moderate modelists. However, the quasi-categorical nature of Zermelo's Theorem gives rise to some specific questions concerning the aims of axiomatic set theories. Given the status of Zermelo's Theorem in the philosophy of set theory, we include a stand-alone proof of this theorem. We also prove a similar quasi-categoricity for Scott-Potter set theory, a theory which axiomatises the idea of an arbitrary stage of the iterative hierarchy.

Download Full-text

Monadic second-order logic on finite sequences

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages - POPL 2017 ◽

10.1145/3009837.3009844 ◽

2017 ◽

Cited By ~ 4

Author(s):

Loris D'Antoni ◽

Margus Veanes

Keyword(s):

Second Order ◽

Order Logic ◽

Finite Sequences ◽

Second Order Logic ◽

Monadic Second Order Logic

Download Full-text

Algorithmic Logic with Stacks and Its Model-Theoretical Properties

Fundamenta Informaticae ◽

10.3233/fi-1984-7402 ◽

1984 ◽

Vol 7 (4) ◽

pp. 391-428

Author(s):

Wiktor Dańko

Keyword(s):

Second Order ◽

Order Logic ◽

Algorithmic Logic ◽

Second Order Logic

In this paper we propose to transform the Algorithmic Theory of Stacks (cf. Salwicki [30]) into a logic for expressing and proving properties of programs with stacks. We compare this logic to the Weak Second Order Logic (cf. [11, 15]) and prove theorems concerning axiomatizability without quantifiers (an analogon of Łoś-Tarski theorem) and χ 0 - categoricity (an analogon of Ryll-Nardzewski’s theorem).

Download Full-text