  Weighted monadic second-order logic is a weighted extension of monadic
second-order logic that captures exactly the behaviour of weighted automata.
Its semantics is parameterized with respect to a semiring on which the values
that weighted formulas output are evaluated. Gastin and Monmege (2018) gave
abstract semantics for a version of weighted monadic second-order logic to give
a more general and modular proof of the equivalence of the logic with weighted
automata. We focus on the abstract semantics of the logic and we give a
complete axiomatization both for the full logic and for a fragment without
general sum, thus giving a more fine-grained understanding of the logic. We
discuss how common decision problems for logical languages can be adapted to
the weighted setting, and show that many of these are decidable, though they
inherit bad complexity from the underlying first- and second-order logics.
However, we show that a weighted adaptation of satisfiability is undecidable
for the logic when one uses the abstract interpretation.
