Game comonads provide a categorical syntax-free approach to finite model
theory, and their Eilenberg-Moore coalgebras typically encode important
combinatorial parameters of structures. In this paper, ...we develop a framework
whereby the essential properties of these categories of coalgebras are captured
in a purely axiomatic fashion. To this end, we introduce arboreal categories,
which have an intrinsic process structure, allowing dynamic notions such as
bisimulation and back-and-forth games, and resource notions such as number of
rounds of a game, to be defined. These are related to extensional or "static"
structures via arboreal covers, which are resource-indexed comonadic
adjunctions. These ideas are developed in a general, axiomatic setting, and
applied to relational structures, where the comonadic constructions for
pebbling, Ehrenfeucht-Fra\"iss\'e and modal bisimulation games recently
introduced by Abramsky et al. are recovered, showing that many of the
fundamental notions of finite model theory and descriptive complexity arise
from instances of arboreal covers.
We provide a direct and elementary proof of the fact that the category of Nachbin’s compact ordered spaces is dually equivalent to an
ℵ
1
-ary variety of algebras. Further, we show that
ℵ
1
is a ...sharp bound: compact ordered spaces are not dually equivalent to any
SP
-class of finitary algebras.
A classical result due to Lovász (1967) shows that the isomorphism type of a graph is determined by homomorphism counts. That is, graphs G and H are isomorphic whenever the number of homomorphisms ...K→G is the same as the number of homomorphisms K→H for all graphs K. Variants of this result, for various classes of finite structures, have been exploited in a wide range of research fields, including graph theory and finite model theory.
We provide a categorical approach to homomorphism counting based on the concept of polyadic (finite) set. The latter is a special case of the notion of polyadic space introduced by Joyal (1971) and related, via duality, to Boolean hyperdoctrines in categorical logic. We also obtain new homomorphism counting results applicable to a number of infinite structures, such as trees and profinite algebras.
A systematic theory of structural limits for finite models has been developed
by Nesetril and Ossona de Mendez. It is based on the insight that the
collection of finite structures can be embedded, ...via a map they call the Stone
pairing, in a space of measures, where the desired limits can be computed. We
show that a closely related but finer grained space of (finitely additive)
measures arises -- via Stone-Priestley duality and the notion of types from
model theory -- by enriching the expressive power of first-order logic with
certain "probabilistic operators". We provide a sound and complete calculus for
this extended logic and expose the functorial nature of this construction.
The consequences are two-fold. On the one hand, we identify the logical gist
of the theory of structural limits. On the other hand, our construction shows
that the duality theoretic variant of the Stone pairing captures the adding of
a layer of quantifiers, thus making a strong link to recent work on semiring
quantifiers in logic on words. In the process, we identify the model theoretic
notion of types as the unifying concept behind this link. These results
contribute to bridging the strands of logic in computer science which focus on
semantics and on more algorithmic and complexity related areas, respectively.
The Stone-Weierstrass Theorem for compact Hausdorff spaces is a basic result of functional analysis with far-reaching consequences. We introduce an equational logic ⊨Δ associated with an infinitary ...variety Δ and show that the Stone-Weierstrass Theorem is a consequence of the Beth definability property of ⊨Δ, stating that every implicit definition can be made explicit. Further, we define an infinitary propositional logic ⊢Δ by means of a Hilbert-style calculus and prove a strong completeness result whereby the semantic notion of consequence associated with ⊢Δ coincides with ⊨Δ.
We show that, if S is a finite semiring, then the free profinite S-semimodule on a Boolean Stone space X is isomorphic to the algebra of all S-valued measures on X, which are finitely additive maps ...from the Boolean algebra of clopens of X to S. These algebras naturally appear in the logic approach to formal languages as well as in idempotent analysis. Whenever S is a (pro)finite idempotent semiring, the S-valued measures are all given uniquely by continuous density functions. This generalises the classical representation of the Vietoris hyperspace of a Boolean Stone space in terms of continuous functions into the Sierpiński space.
We adopt a categorical approach to profinite algebra which is based on profinite monads. The latter were first introduced by Adámek et al. as a special case of the notion of codensity monads.
It has long been known that a key ingredient for a sheaf representation of a universal algebra A consists in a distributive lattice of commuting congruences on A. The sheaf representations of ...universal algebras (over stably compact spaces) that arise in this manner have been recently characterised by Gehrke and van Gool (J. Pure Appl. Algebra, 2018), who identified the central role of the notion of softness.
In this paper, we extend the scope of this theory by replacing varieties of algebras with Barr-exact categories, thus encompassing a number of “non-algebraic” examples. Our approach is based on the notion of K-sheaf: intuitively, whereas sheaves are defined on open subsets, K-sheaves are defined on compact ones. Throughout, we consider sheaves on complete lattices rather than spaces; this allows us to obtain point-free versions of sheaf representations whereby spaces are replaced with frames.
These results are used to construct sheaf representations for the dual of the category of compact ordered spaces, and to recover Banaschewski and Vermeulen's point-free sheaf representation of commutative Gelfand rings (Quaest. Math., 2011).
The classical homomorphism preservation theorem, due to Łoś, Lyndon and Tarski, states that a first-order sentence φ is preserved under homomorphisms between structures if, and only if, it is ...equivalent to an existential positive sentence ψ. Given a notion of (syntactic) complexity of sentences, an “equi-resource” homomorphism preservation theorem improves on the classical result by ensuring that ψ can be chosen so that its complexity does not exceed that of φ.
We describe an axiomatic approach to equi-resource homomorphism preservation theorems based on the notion of arboreal category. This framework is then employed to establish novel homomorphism preservation results, and improve on known ones, for various logic fragments, including first-order, guarded and modal logics.
It has been known since the work of Duskin and Pelletier four decades ago that Kop, the opposite of the category of compact Hausdorff spaces and continuous maps, is monadic over the category of sets. ...It follows that Kop is equivalent to a possibly infinitary variety of algebras Δ in the sense of Słomiński and Linton. Isbell showed in 1982 that the Lawvere–Linton algebraic theory of Δ can be generated using a finite number of finitary operations, together with a single operation of countably infinite arity. In 1983, Banaschewski and Rosický independently proved a conjecture of Bankston, establishing a strong negative result on the axiomatisability of Kop. In particular, Δ is not a finitary variety – Isbell's result is best possible. The problem of axiomatising Δ by equations has remained open. Using the theory of Chang's MV-algebras as a key tool, along with Isbell's fundamental insight on the semantic nature of the infinitary operation, we provide a finite axiomatisation of Δ.
PDF
