second order logic
Recently Published Documents

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.

Every adult male of the little roundworm Caenorhabditis elegans is always and invariably comprised of exactly 1031 somatic cells, not one more, not one less; and so it is for the adult hermaphrodite (959 somatic cells); its intestine founder cell (the ‘E’ blastomere), if isolated and cultured, undergoes the same number of divisions as in the whole embryo (Robertson et al., 2014); the zygote of Drosophila melanogaster executes 13 cycles of asynchronous cell divisions without cellularization: how are these numbers counted? Artificial Intelligence (First and Second Order Logic, Knowledge graph Engineering) infers that, to perform precise stereotypical numbers of asynchronous cell divisions, a nucleic (genomic) counter is indispensable. Made up of tandemly repeated similar monomers, satellite DNA (satDNA) corresponds to iterable objects used in programming. The purpose of this article is to show how satDNA sequences can be iterated over to count a deterministic number of cell divisions: computational models (attached for free download) are introduced that handle DNA repeated sequences as iterable counters and simulate their use in cells through an epigenetic marker (cytosine methylation) as an iterator. SatDNA, because of its propensity to remodel its structure, can also operate as a strong accelerator in the evolution of complex organs and provides a basis to control interspecific variability of shapes.

How transnational are European Parliament (EP) campaigns? Building on research on the Euro-pean public sphere and the politicisation of the EU, this study investigates to what extent the 2019 EP campaign was transnational and which factors were associated with ‘going transna-tional’. It conceptualises Twitter linkages of EP candidates as constitutive elements of a transna-tional campaign arena distinguishing interactions with EP candidates from other countries (hori-zontal transnationalisation) and interactions with the supranational European party families and lead candidates (vertical transnationalisation). The analysis of tweets sent by EP candidates from all 28 member states reveals that most linkages remain national. Despite this evidence for the second-order logic, there are still relevant variations contingent on EU positions of parties, the adoption of the Spitzenkandidaten system and socialisation in the EP. The findings have impli-cations for debates on the European public sphere and institutional reform proposals such as transnational party lists that might mitigate the EU’s democratic deficit.

<p>Bodlaender et al. [7] proved a converse to Courcelle's Theorem for graphs [15] for the class of chordal graphs of bounded treewidth. Hliněný [25] generalised Courcelle's Theorem for graphs to classes of matroids represented over finite fields and of bounded branchwidth. This thesis has investigated the possibility of obtaining a generalisation of chordality to matroids that would enable us to prove a converse of Hliněný's Theorem [25].  There is a variety of equivalent characterisations for chordality in graphs. We have investigated the relationship between their generalisations to matroids. We prove that they are equivalent for binary matroids but typically inequivalent for more general classes of matroids.  Supersolvability is a well studied property of matroids and, indeed, a graphic matroid is supersolvable if and only if its underlying graph is chordal. This is among the stronger ways of generalising chordality to matroids. However, to obtain the structural results that we need we require a stronger property that we call supersolvably saturated.  Chordal graphs are well known to induce canonical tree decompositions. We show that supersolvably saturated matroids have the same property. These tree decompositions of supersolvably saturated matroids can be processed by a finite state automaton. However, they can not be completely described in monadic second-order logic.  In order to express the matroids and their tree decompositions in monadic second-order logic we need to extend the logic over an extension field for each matroid represented over a finite field. We then use the fact that each maximal round modular flat of the tree decomposition for every matroid represented over a finite field, and in the specified class, spans a point in the vector space over the extension field. This enables us to derive a partial converse to Hliněný's Theorem.</p>

<p>Bodlaender et al. [7] proved a converse to Courcelle's Theorem for graphs [15] for the class of chordal graphs of bounded treewidth. Hliněný [25] generalised Courcelle's Theorem for graphs to classes of matroids represented over finite fields and of bounded branchwidth. This thesis has investigated the possibility of obtaining a generalisation of chordality to matroids that would enable us to prove a converse of Hliněný's Theorem [25].  There is a variety of equivalent characterisations for chordality in graphs. We have investigated the relationship between their generalisations to matroids. We prove that they are equivalent for binary matroids but typically inequivalent for more general classes of matroids.  Supersolvability is a well studied property of matroids and, indeed, a graphic matroid is supersolvable if and only if its underlying graph is chordal. This is among the stronger ways of generalising chordality to matroids. However, to obtain the structural results that we need we require a stronger property that we call supersolvably saturated.  Chordal graphs are well known to induce canonical tree decompositions. We show that supersolvably saturated matroids have the same property. These tree decompositions of supersolvably saturated matroids can be processed by a finite state automaton. However, they can not be completely described in monadic second-order logic.  In order to express the matroids and their tree decompositions in monadic second-order logic we need to extend the logic over an extension field for each matroid represented over a finite field. We then use the fact that each maximal round modular flat of the tree decomposition for every matroid represented over a finite field, and in the specified class, spans a point in the vector space over the extension field. This enables us to derive a partial converse to Hliněný's Theorem.</p>

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound and complete with respect to an intuitive and simple algebraic semantics.

AbstractOften philosophers, logicians, and mathematicians employ a notion of intended structure when talking about a branch of mathematics. In addition, we know that there are foundational mathematical theories that can find representatives for the objects of informal mathematics. In this paper, we examine how faithfully foundational theories can represent intended structures, and show that this question is closely linked to the decidability of the theory of the intended structure. We argue that this sheds light on the trade-off between expressive power and meta-theoretic properties when comparing first-order and 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.

While plural logic can be interpreted in monadic second-order logic, the full system of second-order logic cannot be interpreted in plural logic. This means it is formally possible to eliminate plural logic in favor of monadic second-order logic. However, a number of philosophical considerations militate against such an elimination. The conclusion of this chapter echoes that of the preceding ones: although the two systems can occasionally be used for similar purposes, the notions they represent are different and must be kept apart.