2.1 From counting to logic

Let us restrict attention to a very small fragment of the language $\mathcal {L}_\#$ described above. Given some variables $\mathsf {Var}$ and predicate symbols $\mathsf {Pred}$ , we only allow two types of atomic formulas and one operation for building complex formulas. Let $\mathcal {L}_\#^-$ be generated by the grammar:

$$ \begin{align*} \varphi ::= P(x_1,\dots,x_n) \quad\mid\quad x\neq y \quad\mid\quad \#_x\varphi \succsim \#_y\varphi. \end{align*} $$

Aside from predication and variable inequality, we can only compare cardinalities.

A first observation is that Boolean implication can already be defined in $\mathcal {L}_\#^-$ . Where x occurs free in neither $\varphi $ nor $\psi $ , we can take

(2.3) $$ \begin{align} \psi \rightarrow \varphi \equiv \#_x\varphi \succsim \#_x\psi. \end{align} $$

Boolean negation can also be defined. Where $\mathsf {0}$ is an abbreviation for the formula $\#_x (x \neq x)$ (cf. Frege), and again x is a variable that does not occur free in $\varphi $ , we can define

(2.4) $$ \begin{align} \neg \varphi \equiv \mathsf{0} \succsim \#_x\varphi. \end{align} $$

With these we recover any other Boolean connective, as well as variable equality. In some respect, count comparison already incorporates Boolean structure, and familiar Boolean laws emerge as principles of count comparisons. For instance, the pattern $\varphi \rightarrow (\psi \rightarrow \varphi )$ is encoded simply as $\#_x(\#_x\varphi \succsim \#_x\psi ) \succsim \#_x\varphi $ .

Going further, first-order quantification is expressible in $\mathcal {L}_\#^-$ :

(2.5) $$ \begin{align} \exists x. \varphi \equiv \#_x\varphi \succ \mathsf{0}. \end{align} $$

This thus brings us back to full $\mathsf {FO}(\#)$ , in which we can again define the infinity quantifier $\exists ^\infty $ in (2.1), its dual $\forall ^\infty $ , and so on. From rather austere (atomic) primitives, count comparisons already encode a significant amount of logic, provided of course that we allow iteration of comparisons within comparisons.

2.2 From logic to counting

While pure $\mathsf {FO}$ is also capable of encoding facts about counting and arithmetic, it is far less extensive. As already mentioned, first-order logic can define the simple counting quantifiers like $\exists ^{\geq n}x$ ; however, first-order logic does so by means of counting in the syntax. That is, the formula expressing that there are at least n objects satisfying a given condition achieves this by concatenating n existential quantifiers and adding n conjuncts. Basic arithmetic principles like $\exists ^{\geq m}x.\varphi \rightarrow \exists ^{\geq n}x.\varphi $ for $m\geq n$ , thus follow from elementary logical patterns like distribution of existential quantification over conjunction, applied the requisite number of times (e.g., $m-n$ times). This style of counting in the syntax also produces a case-by-case formulation of the Pigeonhole Principle:Footnote ²

Example 2.7. Suppose we have k monadic predicate symbols $P_1,\dots ,P_k$ and let $n>k$ . Then,

(2.6) $$ \begin{align} \big( \exists^{= n}x. \bigvee_{i \leq k} P_i(x) \wedge \forall x. \bigwedge_{i \neq j} \neg (P_i(x) \wedge P_j(x)) \big)\rightarrow \bigvee_{i \leq k} \exists^{\geq 2}x. P_i(x) \end{align} $$

says that if these k predicates together include n objects, then at least one must include at least two objects. This schema is of course valid for every choice of k and $n>k$ .

We will see more examples of counting in the syntax with subsequent sections (see especially Remark 9.15 and Appendix E).

Remark 2.8. The fact that $\mathsf {FO}$ can only count in the syntax reverberates in interesting ways when we consider finite variable fragments of $\mathsf {FO}$ . While the two-variable fragment is known to have the (bounded) finite-model property [Reference Mortimer89], which in turn establishes its decidability, this fragment with counting quantifiers $\exists ^{\geq n}$ can easily enforce infinite models:

$$ \begin{align*}\forall x. \exists^{=1}y. R(x,y) \wedge \forall y .\exists^{\leq 1} x. R(x,y) \wedge \exists y. \forall x. \neg R(x,y) .\end{align*} $$

Such a language is in fact decidable [Reference Grädel, Otto and Rosen45]: like the two-variable fragment without counting, its satisfiability problem is NExpTime-complete [Reference Pratt-Hartmann103]. However, the complexity analysis of this system and its extensions [Reference Kieroński, Pratt-Hartmann and Tendera69] reveals arithmetical content that does not appear in analyses of the plain two-variable fragment, witness connections to integer programming (Section 3.2.1) and to semi-linear sets (Section 4.1).

2.3 Finite models

It is natural to consider a related system in the same language, but with interpretations restricted to finite models. Call such a system $\mathsf {FO}^\phi (\#)$ . As $\mathcal {L}_\#$ extends the language of first-order logic, Trakhtenbrot’s theorem tells us that the validities of $\mathsf {FO}^\phi (\#)$ are still not computably enumerable. Nonetheless, $\mathsf {FO}^\phi (\#)$ and variations on it have also been intensely studied in the literature on finite model theory. See, e.g., [Reference Otto98] or [Reference Schweikardt116] for summaries of relevant work.

As an example of distinctive issues that come up in the finitary setting, one might ask about the asymptotic probabilities of formulas in $\mathsf {FO}^\phi (\#)$ over finite structures. It was shown in [Reference Grumbach and Tollu48] that $\mathsf {FO}$ with the Härtig quantifier in fact possesses a zero–one law, just as pure $\mathsf {FO}$ does. As possession of a zero–one law is commonly interpreted as evidence that a logic cannot formalize any non-trivial counting, this can be taken as justification for our choice of comparison rather than equality as a primitive. Indeed, $\mathsf {FO}^\phi (\#)$ lacks a zero–one law; e.g., $\#_x P(x) \succsim \#_x \neg P(x)$ has asymptotic probability $1/2$ . It is conjectured in [Reference Grumbach and Tollu48] that (an extension of) $\mathsf {FO}^\phi (\#)$ nonetheless possesses a limit law, and that the limits are all rational numbers between $0$ and $1$ .

For many purposes in finite model theory (e.g., descriptive complexity) authors have been motivated to consider proper extensions of our language $\mathcal {L}_\#$ , a notable example being fixed point logic with counting [Reference Cai, Fürer and Immerman22]. Our purpose here is different: we aim to isolate weaker fragments of this language that might further reveal the subtle interplay between logic and counting, also pinpointing differences and commonalities between finitary and infinitary patterns in counting.

2.4 Fragments of $\mathcal {L}_\#$

While full first-order logic with counting may be a natural starting point for exploring our subject, the above observations invite the search for natural fragments and weaker variants of $\mathsf {FO}(\#)$ . It may be desirable, for example, to identify decidable fragments of $\mathcal {L}_\#$ . From this perspective it is noteworthy that some familiar ways of taming complexity are less effective here. For example, finite-variable fragments do not result in decidability: as shown by Grädel et al. [Reference Grädel, Otto and Rosen46], the two-variable fragment of $\mathsf {FO}(\#)$ is still undecidable ( $\Pi ^1_1$ -complete, so we do observe a reduction in complexity, compared to Theorem 2.4). The two-variable fragment of $\mathsf {FO}^\phi (\#)$ is also undecidable. Evidently, a significant source of the complexity is the potent combination of counting and arbitrary quantificational-relational reasoning, witness Lemma 2.2. The undecidability proof in [Reference Grädel, Otto and Rosen46] for the two-variable fragment crucially involves counting successors along binary relations.

A more dramatic route would be to move to a much tamer syllogistic or propositional fragment [Reference Ding, Harrison-Trainor and Holliday32, Reference Moss and Bimbó91]. For instance, if we let $\mathcal {L}_\#^0$ be the language of propositional logic with count comparisons, the resulting system $\mathsf {PL}(\#)$ is easily shown to be decidable (e.g., it will follow immediately from our results below). This route at once eliminates relational reasoning and first-order quantification.

An alternative route is to put relational reasoning to the side, but still retain first-order quantification. The monadic fragment of $\mathcal {L}_\#$ , which we will call $\mathcal {L}_\#^1$ , does not allow counting along relations, but it otherwise preserves the counting content of $\mathsf {FO}(\#)$ . Observe, for example, that our definition of the infinity quantifier in (2.1) and our reconstruction of logical connectives from count comparisons (Section 2.1) depend in no way on the arity of available predicates. We will thus use $\mathsf {MFO}(\#)$ , monadic first-order logic with counting, as a base system to explore richer combinations (Section 3). In this context we will consider adding second-order quantification (system $\mathsf {MSO}(\#)$ in Section 4), as well as the ability to count not just individuals but sequences of individuals (systems $\mathsf {MFO}(\sharp )$ and $\mathsf {MSO}(\sharp )$ in Section 5).

Of course, counting along relations is also common and natural. We therefore explore a tractable modal fragment of $\mathcal {L}_\#$ , which we call $\mathcal {L}_\#^{\mathsf {ml}}$ , as a way of taming the interaction among counting, quantification, and relational reasoning. A summary appears in Table 1.

Table 1 A hierarchy of counting languages and logics, covered in Sections 2-7. For each logical system $\mathsf {L}(\#)$ we also have a version $\mathsf {L}^\phi (\#)$ , where we restrict to finite models. In these systems terms can only denote natural numbers

Following this work we consider a different route altogether, namely changing the semantics of $\mathcal {L}_\#$ . Relaxing either the logical interpretation (relativizing to sets of ‘admissible’ variable assignments; cf. [Reference Németi, Marx, Masuch and Pólos96]) or the numerical content of the $\#$ terms again results in systems that retain much of the character of $\mathsf {FO}(\#)$ , while gaining in tractability.

3.1 Some core principles

Both systems, $\mathsf {MFO}^\phi (\#)$ and $\mathsf {MFO}(\#)$ , are evidently invariant under automorphisms. In the monadic setting automorphisms are precisely the maps that permute elements within a region: all the points that satisfy a given state-description are indistinguishable. This means that if a property holds for one point in a region, it holds for every point in that region. This theme of permutation invariance is characteristic of counting, and it will return when we discuss generalized quantifiers in Section 9.

As demonstrated above, use of individual variables essentially allows manipulating regions—removing or adding points. We can correspondingly state a more general invariance principle. Fix some variables $\mathbf {y}$ and a fixed (finite) set $\mathbf {P}$ of predicate letters, and let $\alpha ^{\mathbf {y}}(x)$ specify a state-description for x as well as which of the variables $\mathbf {y}$ are (un)equal to x. Then, for any formula $\varphi $ (in predicates $\mathbf {P}$ ), if there is at least one x satisfying $\alpha ^{\mathbf {y}}$ and $\varphi $ , then every x satisfying $\alpha ^{\mathbf {y}}$ also satisfies $\varphi $ . Codified in a general invariance principle:

(INV) $$\begin{align} \exists x.\big(\alpha^{\mathbf{y}}(x) \wedge \varphi(x)\big) \rightarrow \#_x\big(\alpha^{\mathbf{y}}(x) \wedge \varphi(x)\big) \approx \#_x\big(\alpha^{\mathbf{y}}(x)\big). \end{align} $$

Since either none of the $\alpha $ ’s satisfy $\varphi $ or all of them do, once we have specified $\alpha $ in a count formula, reference to $\varphi $ becomes redundant. In fact, ( INV ) follows from an even stronger statement (that is, stronger provided we admit infinite models):

(INV2) $$\begin{align} \#_x\big(\alpha^{\mathbf{y}}(x) \wedge \varphi(x)\big) \succ \mathsf{0} \rightarrow \#_x\big(\alpha^{\mathbf{y}}(x) \wedge \neg \varphi(x) \big) \approx \mathsf{0}. \end{align}$$

A related observation about terms $\#_x\varphi $ is that subformulas of $\varphi $ that do not involve x do not contribute any fine-grained information to the term’s denotation. If the free variables of $\psi $ are not among the bound variables of $\#_x\varphi $ , then the following is valid:

(SUB)

Here is the result of substituting $\beta $ for every occurrence of $\gamma $ in $\alpha $ .

3.2 Normal forms

The principles recorded in ( INV ) and ( SUB ), together with basic propositional reasoning and a few other elementary principles (see Section 3.4 for the others), allow the derivation of a normal form result, which works uniformly for $\mathsf {MFO}^\phi (\#)$ and $\mathsf {MFO}(\#)$ . As a first step, we can show that any formula is equivalent to one with no embedded $\#$ -terms or quantifiers within $\#$ -terms, as these terms can always be replaced by unembedded existential quantifiers. This is already a dramatic departure from full relational $\mathsf {FO}(\#)$ , where embedding is non-trivial. (Recall that $\mathsf {FO}(\#)$ with no embedded count comparisons was $\Pi ^1_1$ -complete, in stark contrast to Theorem 2.4.)

Define depth $\mathsf {d}(\varphi )$ by recursion, with $\mathsf {d}(\alpha ) = 0$ for $\alpha $ atomic, $\mathsf {d}(\varphi \wedge \psi ) = \mbox {max}(\mathsf {d}(\varphi ),\mathsf {d}(\psi ))$ , $\mathsf {d}(\neg \varphi ) = \mathsf {d}(\varphi )$ , while $\mathsf {d}(\#_x\varphi \succsim \#_y\psi ) = \mbox {max}(\mathsf {d}(\varphi ),\mathsf {d}(\psi ))+1$ and $\mathsf {d}(\exists x. \varphi ) =\mathsf {d}(\varphi )+1$ .

Generically, a monadic formula with free variables $\mathbf {y},x$ can be written in disjunctive normal form $\bigvee _i \big (\alpha _i(\mathbf {y}) \wedge \alpha ^{\mathbf {y}}_i(x) \wedge \varphi _i(\mathbf {y},x)\big )$ , where $\alpha _i(\mathbf {y})$ specifies state-descriptions for $\mathbf {y}$ and which of these variables are (un)equal, $\alpha ^{\mathbf {y}}_i(x)$ is as in the previous subsection, and $\varphi _i(\mathbf {y},x)$ is some other formula that may in general have positive depth. We want to show that any formula

$$ \begin{align*} \#_x\bigvee_{i\in I} \big(\alpha_i(\mathbf{y}) \wedge \alpha^{\mathbf{y}}_i(x) \wedge \varphi_i(\mathbf{y},x)\big)\succsim \#_x\bigvee_{j\in J} \big(\alpha_j(\mathbf{y}) \wedge \alpha^{\mathbf{y}}_j(x) \wedge \varphi_j(\mathbf{y},x)\big)\end{align*} $$

is equivalent to one with no embedded count comparisons or quantifiers. In other words this formula is equivalent to one of depth $1$ . First, by ( SUB ) we can take the subformulas $\alpha _i(\mathbf {y}),\alpha _j(\mathbf {y})$ outside the count comparisons, which leaves

$$ \begin{align*} \#_x\bigvee_{i\in I} \big(\alpha^{\mathbf{y}}_i(x) \wedge \varphi_i(\mathbf{y},x)\big) \succsim \#_x\bigvee_{j\in J} \big( \alpha_j^{\mathbf{y}}(x) \wedge \varphi_j(\mathbf{y},x)\big) \end{align*} $$

to analyze. Let $\kappa _k$ range over formulas $\exists x.\big (\alpha _k^{\mathbf {y}}(x) \wedge \varphi _k(\mathbf {y},x)\big )$ for $k \in I \cup J$ . Then by appeal to ( INV ), we have the equivalent formula:

$$ \begin{align*} \bigvee_{K \subseteq I \cup J}\big(\bigwedge_{k \in K}\kappa_k \wedge \bigwedge_{k \notin K} \neg \kappa_k \wedge \#_x\bigvee_{i\in I\cap K} \alpha^{\mathbf{y}}_i(x) \succsim \#_x\bigvee_{j\in J \cap K} \alpha_j^{\mathbf{y}}(x) \big) \end{align*} $$

Note that we have traded one level of $\#$ embedding for one existential quantifier. Since $\alpha _i^{\mathbf {y}},\alpha _j^{\mathbf {y}}$ are of depth $0$ , this concludes the argument for:

Using Lemma 3.1, the main result of this section is:

Proof We show more generally that a formula of depth $k+1$ over predicates $\mathbf {P}$ with free variables $\mathbf {y} = y_1,\dots ,y_n$ is equivalent to a disjunction

(3.6) $$ \begin{align} \bigvee\big(\alpha(\mathbf{y})\wedge(\sigma)_{\alpha(\mathbf{y})}\big), \end{align} $$

where $\alpha (\mathbf {y})$ ranges over possible descriptions of $\mathbf {y}$ , and $\sigma $ is a complete description of the regions over $\mathbf {P}$ , i.e., specifying $T_1 {\kern-1pt}={\kern-1pt} T_2 {\kern-1pt}+{\kern-1pt}m$ or $T_1{\kern-1pt}>{\kern-1pt} T_2+m$ for all $m\leq 2(n+k)$ . The notation $(\sigma )_{\alpha (\mathbf {y})}$ denotes a formula that specifies the description $\sigma $ on the assumption of $\alpha (\mathbf {y})$ . In other words, we claim that for each disjunct of (3.6), for all variable assignments s,

(3.7) $$ \begin{align} \mathcal{M},s \vDash \alpha(\mathbf{y}) \wedge (\sigma)_{\alpha(\mathbf{y})} \Rightarrow \mathcal{M}\mbox{ satisfies the }2(n+k)\mbox{ description }\sigma. \end{align} $$

The statement in the theorem will be the special case of (3.6) with no free variables ( $n=0$ ).

Example 3.3. For an example of such a disjunct over one predicate letter P, see the formula inside the existential quantifier in Figure 1. This formula has k free variables and depth $1$ . Here $\alpha (\mathbf {y})$ is the formula $\mathsf {diff}(\mathbf {y}) \wedge \bigwedge _{i \leq k} P(y_i)$ , while $(\sigma )_{\alpha (\mathbf {y})}$ is the count comparison. Note that $(\sigma )_{\alpha (\mathbf {y})}$ has free variables and it ‘means’ that $|P| = |\neg P| + 2k$ provided $\alpha (\mathbf {y})$ holds.

To show that depth $k+1$ formulas are always equivalent to formulas (3.6) satisfying (3.7), we proceed by inducting on k, starting with the case of depth $1$ formulas ( $k=0$ ) in free variables $\mathbf {y}=y_1,\dots , y_n$ . The critical case is a count comparison:

$$ \begin{align*}\#_x \bigvee \alpha(\mathbf{y},x) \succsim \#_x \bigvee \beta(\mathbf{y},x). \end{align*} $$

As before, by ( SUB ) we can separate out the descriptions of $\mathbf {y}$ to obtain a formula

(3.8) $$ \begin{align}\bigvee \big(\gamma(\mathbf{y}) \wedge \#_x\bigvee \alpha^{\mathbf{y}}(x) \succsim \#_x\bigvee\beta^{\mathbf{y}}(x) \big), \end{align} $$

where we have a $\gamma (\mathbf {y})$ disjunct exactly when $\gamma (\mathbf {y}) = \alpha (\mathbf {y}) = \beta (\mathbf {y})$ ; that is, all disjuncts inside the $\#$ terms must agree on the characterization of variables  $\mathbf {y}$ . It is then straightforward to check, by considering all cases, that the count comparison in each disjunct of (3.8), in context $\gamma (\mathbf {y})$ , asserts $T_1 = T_2 +m$ or $T_1> T_2+m$ for $m\leq 2n$ (or a disjunction of such comparisons). So this fits the form in (3.6), and (3.7) is satisfied.

In general, the normal forms (3.6) for a fixed k and n are closed under Boolean combinations, so we only need to consider the case of depth $k+1$ and n variables. By Lemma 3.1 we can assume all count comparison subformulas have depth $1$ , so it suffices to consider an existential quantification, which by induction we assume is

$$ \begin{align*} \exists z. \bigvee \big( \alpha(\mathbf{y},z) \wedge (\sigma)_{\alpha(\mathbf{y},z)}\big). \end{align*} $$

Such a formula will be equivalent to

$$ \begin{align*}\bigvee \exists z. \big(\alpha(\mathbf{y},z) \wedge (\sigma)_{\alpha(\mathbf{y},z)}\big)\end{align*} $$

and indeed to

(3.9) $$ \begin{align} \bigvee \Big(\alpha(\mathbf{y}) \wedge \exists z. \big(\alpha^{\mathbf{y}}(z) \wedge (\sigma)_{\alpha(\mathbf{y},z)}\big)\Big). \end{align} $$

It remains to be seen that (3.9) is of the form (3.6) with each disjunct satisfying (3.7). By the inductive assumption we know that for any s, if $\mathcal {M},s \vDash \alpha (\mathbf {y},z) \wedge (\sigma )_{\alpha (\mathbf {y},z)}$ , then $\mathcal {M}$ satisfies the $2(n+k)$ description $\sigma $ . But if $\mathcal {M},s \vDash \alpha (\mathbf {y}) \wedge \exists z. \big (\alpha ^{\mathbf {y}}(z) \wedge (\sigma )_{\alpha (\mathbf {y},z)}\big )$ , then there is a z-variant $s'$ of s such that $\mathcal {M},s' \vDash \alpha (\mathbf {y},z) \wedge (\sigma )_{\alpha (\mathbf {y},z)}$ , which establishes the result.

3.3 Questions of definability

Theorem 3.2 affords a refined understanding of the numerical relations that can be defined in $\mathsf {MFO}^\phi (\#)$ , as well as $\mathsf {MFO}(\#)$ . Where T is a set of state-descriptions, let $|T|_{\mathcal {M}}$ denote the sum of cardinalities of extensions in $\mathcal {M}$ of state-descriptions in T. We will say that $\mathcal {M} \sim _k \mathcal {M}'$ if for all $T_1,T_2$ and all $m \leq k$ ,

$$ \begin{align*} |T_1|_{\mathcal{M}} \geq |T_2|_{\mathcal{M}} + m \quad \mbox{iff}\quad |T_1|_{\mathcal{M}'} \geq |T_2|_{\mathcal{M}'} + m \end{align*} $$

Then, where $\mathcal {M} \equiv _k \mathcal {M}'$ signifies that $\mathcal {M}$ and $\mathcal {M}'$ agree on all sentences up to depth k, Theorem 3.2 immediately gives:

As an initial example, we can characterize precisely the binary logical quantifiers definable in $\mathsf {MFO}^\phi (\#)$ (see Section 9 for a proof, and for further discussion of generalized quantifiers):

This includes many of the standard logical quantifiers: ‘most’, ‘all’, ‘some’, ‘all but one’, ‘at least two’, etc. The following gives an example of a statement that cannot be expressed.

For a second example, consider a natural rendering of the natural language expression ‘many’, often taken to refer to a number above some contextual threshold. On a more sophisticated, but not uncommon, reading (cf. [Reference Rett111, Reference Westerståhl128]), ‘Many Qs are P’ amounts to a comparison between the proportion of Ps among the Qs and the proportion of Ps overall, which we might symbolize as

(3.10) $$ \begin{align} \frac{\#_x\big(P(x) \wedge Q(x)\big)}{\#_x Q(x)} \succ \frac{\#_x P(x)}{\#_x \top}. \end{align} $$

We will return to more analysis of natural language constructions in Section 9. Note that Corollary 3.4 can be used to derive undefinability results in $\mathsf {MFO}(\#)$ as well:

3.3.1 Interpolation failure

Another consequence of Theorem 3.2 is a particularly simple normal form result for the ‘letterless’ fragment of $\mathcal {L}_\#^1$ , that is, the fragment with no predicate symbols, built up from atomic formulas $\top $ and $\bot $ . In fact, the normal forms are identical to those for monadic first-order logic with the infinity quantifier [Reference Carreiro, Facchini, Venema and Zanasi24]:

Lemma 3.9. Every letterless sentence is equivalent in $\mathsf {MFO}(\#)$ to a disjunction of formulas having one of the following forms $\exists ^\infty x. \top $ , $\forall ^\infty x. \bot \wedge \exists ^{\geq k} \top $ , or $\exists ^{=k} x. \top $ .

For the restriction $\mathsf {MFO}^\phi (\#)$ to finite models, this simplifies even further to include only statements of the form $\exists ^{>k}.\top $ and $\exists ^{=k} x. \top $ . As a consequence we can show:

Proposition 3.10. Neither $\mathsf {MFO}^\phi (\#)$ nor $\mathsf {MFO}(\#)$ enjoys the interpolation property.

Proof Let $\varphi (P)$ be the formula:

$$ \begin{align*}\forall^\infty x. \bot \wedge \#_x(P(x)) \approx \#_x(\neg P(x)),\end{align*} $$

which is only true in finite models of even sizes. Let $\psi (Q)$ be the formula:

$$ \begin{align*}\exists x.\#_y( y \neq x \wedge Q(y) ) \approx \#_y( y \neq x \wedge \neg Q(y) ),\end{align*} $$

which in finite models requires the domain to be odd. Evidently $\varphi (P) \vDash \neg \psi (Q)$ . Let $\chi $ be a purported interpolant: $\varphi (P) \vDash \chi \vDash \neg \psi (Q)$ . As $\chi $ must be letterless, Lemma 3.9 implies that it must be a disjunction of sentences with one of the three specified forms. Furthermore, as it is entailed by $\varphi (P)$ we can assume that $\exists ^\infty x. \top $ is not a disjunct. A straightforward case analysis shows that $\chi $ must either be true only in models up to some fixed size—in which case it cannot be entailed by $\varphi (P)$ —or it is true in all finite models from some finite size onward—in which case it cannot entail $\neg \psi (Q)$ .

A familiar way of extending a language to guarantee interpolation is to allow second-order quantification. We will turn to such an extension below in Section 4. But first, we analyze the reasoning content of our normal form analysis a bit further.

3.4 Questions of axiomatization

What is the calculus of valid reasoning suggested by our current systems? For both of our basic monadic systems, $\mathsf {MFO}^\phi (\#)$ and $\mathsf {MFO}(\#)$ , we can locate a kind of separation between two components: (a) the general, more ‘logical’ principles that allow our normal form result (Theorem 3.2) and (b) more specific numerical reasoning for solving systems of inequalities. We discuss each component in turn for the system $\mathsf {MFO}^\phi (\#)$ which allows only finite domains. The general system $\mathsf {MFO}(\#)$ involves one more component for dealing with infinite sets that we will remark on at the end.

3.4.1 Step I

The normal form principles underlying our normal form result are as follows:

1. (a) general validities of propositional and first-order predicate logic,

2. (b) the two general principles ( INV ) and ( SUB ) highlighted earlier,

3. (c) the linear order properties of the relation $\succsim $ .

Here the linearity in Principle (c), used in our case distinctions, is worth high-lighting:

(COMP) $$\begin{align} \#_x\varphi \succsim \#_x\psi \vee \#_x\psi \succsim \#_x\varphi. \end{align}$$

The soundness of ( COMP ) in $\mathsf {MFO}(\#)$ depends on the axiom of choice. Indeed, ( COMP ) is equivalent to the axiom of choice [Reference Hartogs55]. Significantly, in the generalized semantics discussed in Section 8, Principles (a) and (b) will remain valid, while the strong reasoning principle (c) is naturally replaced by just the pre-order properties for $\succsim $ .

4.1 Finitary case

We saw above that normal forms in $\mathsf {MFO}^\phi (\#)$ correspond to (disjunctions of) sets of inequality constraints, a class whose solvability problem is already NP-complete. In the general setting of integer programming, there is a close correspondence between sets of linear inequalities and quantifier-free formulas of Presburger Arithmetic, that is, first-order logic with addition over the natural numbers (see, e.g., [Reference Oppen97]). The sets of solutions to such inequalities (or equivalently, assignments satisfying Presburger formulas with free variables) are exactly the semi-linear sets [Reference Ginsburg and Spanier44], a generalization of the ‘ultimately periodic’ sets of numbers:

Definition 4.2. A set $\mathcal {V}\subseteq \mathbb {N}^n$ of n-ary vectors is called linear if there is a system of equations over variables $\mathsf {v}_1,\dots ,\mathsf {v}_n,\mathsf {u}_1,\dots ,\mathsf {u}_m$ and constants $b_1,\dots ,b_n,a_{1,1},\dots ,a_{n,m}$ ,

(4.1) $$ \begin{align} \begin{pmatrix} \;\mathsf{v}_1\; \\ \vdots \\ \mathsf{v}_n \end{pmatrix} = \begin{pmatrix} b_1 + a_{1,1}\mathsf{u}_1 + & \dots & + a_{1,m}\mathsf{u}_m \\ \vdots & & \vdots \\ b_n + a_{n,1}\mathsf{u}_1 + & \dots & + a_{n,m}\mathsf{u}_m \end{pmatrix} \end{align} $$

such that $\mathbf {x} \in \mathcal {V}$ if and only if there exist values of $\mathsf {u}_1,\dots ,\mathsf {u}_m$ for which $\mathbf {v}=\mathbf {x}$ is a solution to (4.1). We say $\mathcal {V} \subseteq \mathbb {N}^n$ is semi-linear if it is a finite union of linear sets.

Definition 4.3. Suppose $S_1,\dots ,S_n$ are some state-descriptions over predicates $\mathbf {P}$ , and that $\varphi $ is an $\mathcal {L}_\#^2$ sentence in these same predicates $\mathbf {P}$ . We say that $\varphi $ defines a set $\mathcal {V} \subseteq \mathbb {N}^n$ just in case, for any model $\mathcal {M}$ , we have

(4.2) $$ \begin{align} \mathcal{M} \vDash \varphi \quad \mbox{iff}\quad [|S_1|_{\mathcal{M}},\dots,|S_n|_{\mathcal{M}}] \in \mathcal{V}. \end{align} $$

We now want to show the other direction, that all $\mathcal {L}_\#^2$ sentences in fact define semi-linear sets. Toward this result we first note that $\mathsf {MSO}(\#)$ possesses a prenex normal form.

By Theorem 3.2 we know that $\varphi (\mathbf {P},X_1,\dots ,X_n)$ has a normal form involving expressions $T_1=T_2+m$ and $T_1> T_2+m$ , where $T_1,T_2$ are cardinalities of state-descriptions over $\mathbf {P}$ and additional predicates $X_1,\dots ,X_n$ . Such formulas are thus easily seen to be semi-linear, indeed linear. As semi-linear sets are closed under Boolean combinations, and second-order quantifiers distribute over disjunction, the main goal is to show:

Proof As $\varphi (O_1,\dots ,O_n,X)$ is linear, we can assume it defines the solutions to

(4.3) $$ \begin{align} \begin{pmatrix} \;|S_1|\; \\ \vdots \\ |S_{2^{n+1}}| \end{pmatrix} = \begin{pmatrix} b_1 + a_{1,1}\mathsf{u}_1 + & \cdots & + a_{1,m}\mathsf{u}_m \\ \vdots & & \vdots \\ b_{2^{n+1}} + a_{2^{n+1},1}\mathsf{u}_1 + & \cdots & + a_{2^{n+1},m}\mathsf{u}_m \end{pmatrix}. \end{align} $$

To show that $\exists X. \varphi (O_1,\dots ,O_n,X)$ , too, is linear, we define another linear set of equations by ‘projecting out’ the variable X.

Specifically, note for each state-description $S_k'$ , both $S_k' \wedge X$ and $S_k' \wedge \neg X$ are (equivalent to) some state-descriptions, $S_i$ and $S_j$ , and in fact $S_k'$ is equivalent to $S_i \vee S_j$ . The new linear system in $2^n$ variables is then as follows for each $k\leq 2^n$ :

(4.4) $$ \begin{align} |S^{\prime}_k| = b_i + b_j + (a_{i,1}+a_{j,1})\mathsf{u}_1+ \dots + (a_{i,m} + a_{j,m})\mathsf{u}_m. \end{align} $$

It remains only to show that:

$$ \begin{align*} \mathcal {M} & \vDash \exists X. \varphi (O_1,\dots ,O_n,X)\\ &\Leftrightarrow [|S_1'|_{\mathcal {M}},\dots ,|S_{2^n}'|_{\mathcal {M}}] \mbox{ is a solution to Equation (20)}.\end{align*} $$

$(\Rightarrow )$ : If $\mathcal {M} \vDash \exists X. \varphi (O_1,\dots ,O_n,X)$ then for some subset A of the domain, we have $\mathcal {M},s^X_A \vDash \varphi (O_1,\dots ,O_n,X)$ . Treating X now as a predicate constant, we have a model $\mathcal {M}'$ for which $X^{\mathcal {M}'}=A$ , and by assumption this gives a solution $[|S_1|_{\mathcal {M}'},\dots ,|S_{2^{n+1}}|_{\mathcal {M}'}]$ to (4.3). But each state-description $S_k'$ is equivalent to a disjunction $S_i \vee S_j$ , whose cardinality is the sum $|S_i|+|S_j|$ . Therefore $\mathcal {M}'$ will satisfy each of the constraints in (4.4). As the state-descriptions $S_1',\dots ,S_{2^n}'$ are independent of X, this means $[|S_1'|_{\mathcal {M}},\dots ,|S_{2^n}'|_{\mathcal {M}}]$ also gives a solution to (4.4).

$(\Leftarrow )$ : Suppose $[|S_1'|_{\mathcal {M}},\dots ,|S_{2^n}'|_{\mathcal {M}}]$ gives a solution to (4.4) for some particular choices $\mathsf {u}_1,\dots ,\mathsf {u}_m$ . We need to find a set A such that $\mathcal {M},s^X_A \vDash \varphi (O_1,\dots ,O_n,X)$ . Since the extensions of $S_1',\dots ,S_{2^n}'$ are all disjoint, to define A it suffices to identify subsets of each ${[\![{ {S_k'} }]\!]}_{\mathcal {M}}$ . As above, suppose $S^{\prime }_k$ is equivalent to $S_i \vee S_j$ , so that $S_i$ is equivalent to $S^{\prime }_k \wedge X$ and $S_j$ is equivalent to $S_k' \wedge \neg X$ . Then let $B_k$ be any subset of ${[\![{ {S_k'} }]\!]}_{\mathcal {M}}$ of size $b_i + a_{i,1}\mathsf {u}_1 + \dots + a_{i,m}\mathsf {u}_m$ , such that the complement ${[\![{ {S^{\prime }_k} }]\!]}_{\mathcal {M}} - B_k$ has size $b_j + a_{j,1}\mathsf {u}_1 + \dots + a_{j,m}\mathsf {u}_m$ . This is always possible since $|S^{\prime }_k|$ is simply the sum of these two numbers. Finally let $A = \bigcup _{k\leq 2^n} B_k$ . Once again absorbing X into the language and defining $\mathcal {M}'$ to be just like $\mathcal {M}$ but with $X^{\mathcal {M}'} = A$ , the tuple $[|S_1|_{\mathcal {M}'},\dots ,|S_{2^{n+1}}|_{\mathcal {M}'}]$ gives a solution to (4.3) with the same choices $\mathsf {u}_1,\dots ,\mathsf {u}_m$ . Hence, $\mathcal {M}'\vDash \varphi (O_1,\dots ,O_n,X)$ , from which it easily follows that $\mathcal {M},s^X_A \vDash \varphi (O_1,\dots ,O_n,X)$ and finally $\mathcal {M} \vDash \exists X. \varphi (O_1,\dots ,O_n,X)$ .

The foregoing thus establishes:

As in the first-order case, numerous undefinable results again follow. For example:

Indeed, the theory of definability for Presburger Arithmetic carries over exactly to $\mathsf {MSO}^\phi (\#)$ , thanks to Theorem 4.7. Moreover, since there is an algorithmic means of putting a formula of $\mathsf {MSO}^\phi (\#)$ into normal form and finding a suitable semi-linear form, decidability follows from the decidability of Presburger Arithmetic.

4.2 Infinitary case

Allowing second-order quantification does increase the expressive power of our initial system $\mathsf {MFO}^\phi (\#)$ . While the latter essentially amounts to a proper fragment of Presburger Arithmetic, $\mathsf {MSO}^\phi (\#)$ gave us precisely Presburger Arithmetic. How does this look for the system $\mathsf {MSO}(\#)$ over models of arbitrary cardinality? One immediate difference is that, in contrast to $\mathsf {MFO}(\#)$ (Fact 3.8), the successor function on cardinal numbers can now be easily expressed:

$$ \begin{align*}\forall X.\big( \#_yP(y) \succ \#_y X(y) \rightarrow \#_y Q(y) \succsim \#_yX(y)\big).\end{align*} $$

This formula states that there is no cardinality strictly in between that of P and that of Q. How much more cardinal arithmetic does $\mathsf {MSO}(\#)$ encode?

As in the case of $\mathsf {MSO}^\phi (\#)$ , we can calibrate this by appeal to additive first-order (now cardinal) arithmetic. Consider the elementary theory of the structure $\langle C_{\aleph _\omega };+ \rangle $ , addition over the cardinals numbers less than $\aleph _\omega $ . This is the theory of cardinal numbers in a first-order language with one binary function symbol, namely addition. We show in Appendix C that this theory admits quantifier elimination provided we augment the language with constants for the (definable in $\mathsf {MSO}(\#)$ ) functions and relations:

• • $\{0\}$ and $\{\aleph _0\}$ ,

• • s — the successor function,

• • $>$ — the ‘greater than’ relation,

• • $\equiv _k$ — equivalence modulo k for each $k>1$ .

Furthermore, we can derive a normal form result for this language:

• • which (ordinary first-order) variables in the disjunct are finite or infinite ( $\delta $ ),

• • a description of a linear set for the finite variables ( $\phi $ ),

• • a description of a set of infinite cardinals using $0$ , s, and $>$ over $\aleph $ -number indices, for the infinite variables ( $\iota $ ).

This can be understood as a kind of separation result. The finitary part, Presburger Arithmetic, simply describes ordinary addition. As for the infinitary part, observe that there is an isomorphism from $\langle \mathbb {N};0,s,>\rangle $ onto $\langle \{\aleph _k\}_{k\in \mathbb {N}}; \aleph _0,s,> \rangle $ , sending k to $\aleph _k$ . In other words, the additive structure of cardinals less than $\aleph _\omega $ amounts to a ‘product’ of $\langle \mathbb {N};+ \rangle $ and $\langle \mathbb {N};> \rangle $ .Footnote ³

Our aim is to show that $\mathsf {MSO}(\#)$ possesses the same normal forms as in Proposition 4.11. To see that any statement of the form $\delta \wedge \iota \wedge \phi $ can be expressed, note that $\delta $ merely requires distinguishing finite and infinite sets (recall Equation (2.1)), while definability of any linear set (specified by $\phi $ ) was shown already in Lemma 4.4. Meanwhile, $\iota $ is a conjunction of formulas of types $\mathsf {v}=s^k(\mathsf {u})$ , $\mathsf {v}>s^k(\mathsf {u})$ , $\mathsf {v} = \aleph _k$ , and $\mathsf {v}>\aleph _k$ . We noted above that successor is expressible, and, for instance, we can assert that P has cardinality $\aleph _0$ simply by stating that P is infinite and there is no infinite set with smaller cardinality. Thus, any such statement is expressible.

To show that this exhausts what is definable in $\mathsf {MSO}(\#)$ , given Lemma 4.5, it remains to observe that the $\mathcal {L}_\#^2$ -definable sets are closed under ‘projection’ by existentially quantifying one of the variables. Thus, suppose we have an $\mathcal {L}_\#^2$ formula $\varphi (\mathbf {O},Y)$ with Y a predicate variable and $\mathbf {O}=O_1,\dots ,O_n$ all either predicate variables or letters. We will assume $\varphi (\mathbf {O},Y)$ has the form $\delta (\mathbf {O},Y) \wedge \iota (\mathbf {O},Y) \wedge \phi (\mathbf {O},Y)$ , analogously to the additive language: $\delta (\mathbf {O},Y)$ describes which state descriptions over variables $O_1,\dots ,O_n,Y$ are (in)finite, $\iota (\mathbf {O},Y)$ characterizes the infinite state descriptions, while $\phi (\mathbf {O},Y)$ describes a linear set. We need to analyze $\exists Y.\big (\delta (\mathbf {O},Y) \wedge \iota (\mathbf {O},Y) \wedge \phi (\mathbf {O},Y)\big )$ .

We can replace $\delta (\mathbf {O},Y)$ with a formula $\delta '(\mathbf {O})$ specifying that a state description S over $O_1,\dots ,O_n$ is finite iff $S \wedge Y$ and $S \wedge \neg Y$ were both finite according to $\delta (\mathbf {O},Y)$ . List the finite state descriptions according to $\delta (\mathbf {O},Y)$ as $S_1,\dots ,S_k$ . The subformula $\phi (\mathbf {O},Y)$ defines a linear set over the possible (finite) cardinalities:

(4.5) $$ \begin{align} \begin{pmatrix} \;|S_1|\; \\ \vdots \\ |S_{k}| \end{pmatrix} = \begin{pmatrix} b_1 + a_{1,1}\mathsf{u}_1 + & \cdots & + a_{1,m}\mathsf{u}_m \\ \vdots & & \vdots \\ b_{k} + a_{k,1}\mathsf{u}_1 + & \cdots & + a_{k,m}\mathsf{u}_m \end{pmatrix}. \end{align} $$

Suppose $S_i = S \wedge Y$ is finite but $S \wedge \neg Y$ is infinite. Then the constraint in (4.5) on $|S_i|$ is no constraint at all: since $|S|$ must be infinite, carving out a finite portion $S \wedge Y$ of any size will always be possible. So in this case we can simply drop the equation for $S_i$ . Otherwise, if $S_i = S\wedge Y$ and $S_j=S \wedge \neg Y$ are both finite, then we can repeat the argument from Section 4.1, again combining these two equations into a single equation for $|S|$ . The result is a set of equations in (cardinalities of) state descriptions over $\mathbf {O}$ , all asserted finite in $\delta '(\mathbf {O})$ .

The subformula $\iota (\mathbf {O},Y)$ represents constraints of the form $\mathsf {v}=\mathsf {w}$ and $\mathsf {v}>\mathsf {w}$ , where $\mathsf {v}$ and $\mathsf {w}$ are either ‘infinite’ state descriptions over $\mathbf {O},Y$ , k-fold successors of such state descriptions, or aleph-numbers. In view of the isomorphism between $\langle \mathbb {N};0,s,> \rangle $ and $\langle \{\aleph _k\}_{k \in \mathbb {N}};\aleph _0,s,>\rangle $ , we can construe these conjuncts as describing relations on natural numbers. As these relations are a special case of linear sets and can thus be encoded as in (4.5), we once again run the argument to ‘merge’ the equations for $S \wedge Y$ and $S \wedge \neg Y$ into a single equation for S, provided all of these are infinite. (If only one of $S \wedge Y$ and $S \wedge \neg Y$ is infinite, then that equation remains as before since S will have the same cardinality.) The resulting formula will in general involve addition. But as discussed further in Appendix C, since all variables are infinite we can eliminate all explicit sums, using equivalences such as $\mathsf {t} = \mathsf {v}+\mathsf {w} \Leftrightarrow (\mathsf {t}=\mathsf {v} \wedge \mathsf {v} \geq \mathsf {w})\vee (\mathsf {t}=\mathsf {w} \wedge \mathsf {w} \geq \mathsf {v}) $ .

In effect, we have shown how to reduce a sentence $\varphi (\mathbf {P})$ in $\mathcal {L}_\#^2$ to an additive first-order formula $\alpha (\mathbf {x})$ , with a variable $x_i$ in $\mathbf {x}$ corresponding to each state-description over $\mathbf {P}$ . Moreover, $\varphi (\mathbf {P})$ is satisfiable if and only if $\exists \mathbf {x}.\alpha (\mathbf {x})$ is true in $\langle C_{\aleph _\omega };+ \rangle $ . Thus, from decidability of the elementary theory of $\langle C_{\aleph _\omega };+ \rangle $ (see Theorem C.3 in Appendix C) we obtain:

5.1 Diophantine inequalities

To start our discussion, consider any polynomial inequality

(5.1) $$ \begin{align} m_1(\mathbf{v}) + \dots + m_k(\mathbf{v}) \geq m_1'(\mathbf{v}) + \dots + m_j'(\mathbf{v}), \end{align} $$

where $m_1,\dots ,m_k,m^{\prime }_1,\dots ,m^{\prime }_j$ are all monomials in variables $\mathbf {v} = \mathsf {v}_1,\dots ,\mathsf {v}_n$ . Each monomial $m(\mathbf {v})$ is of the form $a \mathsf {v}_1^{e_1}\dots \mathsf {v}_n^{e_n}$ , with $a,e_1,\dots ,e_n$ all natural numbers and $a>0$ . We would like to show that sentences in $\mathsf {MFO}^{\phi }(\sharp )$ express all the Diophantine inequalities of type (5.1). The first result generalizes the observations above:

Proof Let $a^*$ be the sum of all the coefficients of $m_1,\dots ,m_k,m_1',\dots ,m_j'$ , and let $e^*$ be the maximum over all the sums $\sum _{i \leq n} e_i$ . Then our sentence will take the form:

(5.2) $$ \begin{align} \exists \mathbf{z}.\Big(\mathsf{diff}(\mathbf{z}) \wedge \sharp_{\mathbf{x}} \bigvee_{1\leq i \leq k} \alpha_i \succsim \sharp_{\mathbf{x}} \bigvee_{1 \leq i \leq j} \beta_i\Big), \end{align} $$

with $\mathbf {z} = z_1,\dots ,z_{a^*}$ and $\mathbf {x} = x_0,x_1,\dots ,x_{e^*}$ . We need to ensure that each tuple of values for $\mathbf {x}$ satisfies at most one of the $\alpha _i$ formulas (and the same for the $\beta _i$ formulas), and that each $\alpha _i$ contributes exactly $a \times |S_1|^{e_1}\times \dots \times |S_n|^{e_n}$ to the overall sum, when $m_i(\mathbf {v}) = a \mathsf {v}_1^{e_1}\dots \mathsf {v}_n^{e_n}$ . To that end let $\alpha _i$ be the conjunction of the following formulas:

1. (i) $S_1(x_1) \wedge \cdots \wedge S_1(x_{e_1})$ , with a similar conjunct for each of $S_2,\dots ,S_n$ , predicating $e_2,\dots ,e_n$ variables, respectively.

2. (ii) For any remaining x up to $x_{e^*}$ , include a conjunct $x= x_1$ .

3. (iii) As a final conjunct in the formula $(x_0 = z_{i_1} \vee \dots \vee x_0 = z_{i_a})$ , for a variables $z_{i_1},\dots ,z_{i_a}$ from among $z_1,\dots ,z_{a^*}$ , guaranteed unique to this disjunct $\alpha _i$ .

The last conjunct 5.1 ensures that each $\alpha _i$ contributes a multiplied by the number of tuples satisfying $|S_1|^{e_1}\times \dots \times |S_n|^{e_n}$ , since each such tuple appears with exactly a (unique) values of $x_0$ . Defining the $\beta _i$ s analogously produces a formula whose models capture precisely the same solutions as (5.1), provided the sum of these numbers is at least $a^*$ . There may of course be solutions that together add up to less than $a^*$ , in which case (5.2) will fail; however, there will be at most finitely many. For each such solution $b_1,\dots ,b_n$ we can simply disjoin (5.2) with the statement $|S_1|=b_1 \wedge \dots \wedge |S_n|=b_n$ , the latter being easily definable (even in $\mathsf {MFO}^\phi (\#)$ ).

Conjunctions of inequalities in (5.1) give us the well-studied class of Diophantine equations. The Matiyasevich–Robinson–Davis–Putnam (MRDP) theorem shows that there can be no decision procedure to determine whether a given Diophantine equation has a solution. So:

Moreover, while it is possible to enumerate the satisfiable formulas in an effective way, the valid sentences of $\mathsf {MFO}^{\phi }(\sharp )$ —those whose negations define equations with no solutions—are not computably enumerable. Therefore:

5.2 Normal forms

In the direction of a normal form for $\mathsf {MFO}^{\phi }(\sharp )$ , a first observation is that a version of the invariance principle ( INV ) from Section 3.2 holds in the present setting as well:

$$ \begin{align*} \exists \mathbf{x} \big(\alpha^{\mathbf{y}}(\mathbf{x}) \wedge \varphi(\mathbf{x})\big) \rightarrow \sharp_{\mathbf{x}} \big( \alpha^{\mathbf{y}}(\mathbf{x}) \wedge \varphi(\mathbf{x})\big) \approx \sharp_{\mathbf{x}} \alpha^{\mathbf{y}}(\mathbf{x}), \end{align*} $$

where now $\alpha ^{\mathbf {y}}(\mathbf {x})$ is a complete description of the list $\mathbf {x}$ of variables (relative to $\mathbf {y}$ ). By an analogous argument we can then show that every formula in $\mathcal {L}^1_{\sharp }$ is equivalent to one with no embedded $\sharp $ comparisons. More generally, as in Theorem 3.2, we have:

Proof Sketch

We want to show more generally that every formula of $\mathcal {L}^1_{\sharp }$ in free variables $\mathbf {y}$ is equivalent to a disjunction

(5.3) $$ \begin{align} \bigvee \big(\alpha(\mathbf{y}) \wedge (\sigma)_{\alpha(\mathbf{y})}\big), \end{align} $$

where $\alpha (\mathbf {y})$ ranges over possible descriptions of $\mathbf {y}$ , and $\sigma $ is a conjunction of (strict and weak) Diophantine inequalities (5.1). Specifically, each disjunct is such that, for all s:

(5.4) $$ \begin{align} \mathcal{M},s \vDash \alpha(\mathbf{y}) \wedge (\sigma)_{\alpha(\mathbf{y})} \Rightarrow & \mathcal{M}\mbox{ satisfies the description }\sigma. \end{align} $$

As in the proof of Theorem 3.2, we show that every formula is equivalent to one of the form (5.3) satisfying (5.4) by induction on the quantifier depth of formulas. In the base case, with no quantifiers and just a single $\sharp $ -comparison, our normal forms will be disjunctions of conjunctions $\alpha (\mathbf {y}) \wedge (\sigma )_{\alpha (\mathbf {y})}$ where $(\sigma )_{\alpha (\mathbf {y})}$ takes the form:

$$\begin{align*} \bigwedge \Big( \sharp_{\mathbf{x}} \bigvee \alpha_i^{\mathbf{y}}(\mathbf{x}) \succsim \sharp_{\mathbf{x}} \bigvee \alpha_j^{\mathbf{y}}(\mathbf{x}) \Big). \end{align*}$$

It is straightforward to check that each such disjunct corresponds to a set of Diophantine inequality constraints satisfying (5.4). The inductive case is just as in the proof of Theorem 3.2, reducing to the claim that normal forms in (5.3) are closed under existential quantification.

5.3 Second-order extensions

The jump from $\mathsf {MFO}^\phi (\#)$ to $\mathsf {MSO}^\phi (\#)$ , incorporating second-order quantification, was relatively minor. Arithmetically speaking, it simply allowed ‘filling out’ the class of linear inequalities we were able to encode. Given that $\mathsf {MFO}^{\phi }(\sharp )$ already defines quantifier-free first-order arithmetic (Theorem 5.7), we might expect a more dramatic increase in expressive power when moving to the second-order version $\mathsf {MSO}^{\phi }(\sharp )$ .

The proof of Lemma 5.4 was given for state-descriptions corresponding to the variables in (5.1). Suppose, however, that we replace some of these state-descriptions with second-order variables. It then becomes clear that we can consider arbitrary quantificational statements involving Diophantine inequalities. Here is an illustration, revisiting Example 5.3:

Example 5.8. We can encode the purely arithmetical statement $\forall n \exists m.( m\times 2 = n^3 + 2)$ :

$$ \begin{gather*} \forall X. \exists Y. \exists x,y.\Big(\neg (X(x) \vee X(y)) \wedge x \neq y \wedge \sharp_{u,v}\big( Y(u) \wedge (v=x \vee v=y) \big)\approx \\ \sharp_{z,u,v} \big((X(z) \wedge X(u) \wedge X(v)) \vee z=u=v=x \vee z=u=v=y \big) \Big). \end{gather*} $$

This is the same expression as in Example 5.3, except that we quantify out the predicates P and Q. Given the quantification, this statement is of course unsatisfiable. Were the initial universal quantifier instead existential, this would be a valid statement.

More systematically, we can derive a normal form result in this language, such that every sentence is equivalent to a Boolean combination of arithmetical statements (involving arbitrary quantification over natural numbers), from which we obtain:

It of course follows that the set of validities in $\mathsf {MSO}^{\phi }(\sharp )$ is non-arithmetical.

5.4 Infinitary counting

For both systems, $\mathsf {MFO}^\phi (\sharp )$ and $\mathsf {MSO}^\phi (\sharp )$ , we can consider their more general versions, $\mathsf {MFO}(\sharp )$ and $\mathsf {MSO}(\sharp )$ , where we allow infinite models. It is shown in Appendix C that, similar to the purely additive case, cardinal arithmetic (say, up to $\aleph _{\omega }$ ) with addition and multiplication separates cleanly into the finitary and infinitary components, with the infinitary component effectively reducing to the first-order theory of $\langle \mathbb {N};> \rangle $ . A similar (but in fact simpler) analysis to that given for $\mathsf {MSO}(\#)$ shows that $\mathsf {MFO}(\sharp )$ defines exactly the quantifier-free definable relations on cardinals less than $\aleph _{\omega }$ , while $\mathsf {MSO}(\sharp )$ coincides with full first-order cardinal arithmetic (with addition and multiplication).

6.1 Addition

Let $\mathsf {MFO}(\#,+)$ be the system that results by allowing arbitrary finite sums of basic $\#$ terms. In other words we allow terms of the form $\#_{x_1}\varphi _1 + \dots + \#_{x_n}\varphi _n$ . We already know that $\mathsf {MSO}(\#)$ can express all such inequalities. Conversely, the normal form result for $\mathsf {MSO}(\#)$ by means of linear inequalities shows that this system and $\mathsf {MFO}(\#,+)$ are in fact equally expressive when it comes to defining relations on cardinal numbers.

Note also that the numerical reasoning involved in Fourier–Motzkin (Remark 3.11) can be transcribed into this language without any further ado. For instance, we can encode the crucial step (iii) by a simple scheme:

$$ \begin{align*}\big(|S_1| \succsim |S_2| + |S_3| \wedge |S_4|+|S_3| \succsim |S_2|\big) \rightarrow |S_1|+|S_4| \succsim |S_2|+|S_2|.\end{align*} $$

Thus, similar to analogous work on (rational) linear programming [Reference Fagin, Halpern and Megiddo37], we could codify the steps of the algorithm into axioms of a formal system.

6.2 Multiplication

From an arithmetical point of view, it is natural to allow arbitrary finite products of basic $\#$ -terms as well. How would such a system relate to our systems for counting sequences, such as $\mathsf {MFO}^\phi (\sharp )$ or $\mathsf {MSO}^\phi (\sharp )$ ? Needless to say, if we had explicit multiplication and addition we would be able to encode all arithmetical relations, which would give the same expressive power as $\mathsf {MSO}^\phi (\sharp )$ (thanks to Theorem 5.9).

Similar to the case of $\mathsf {MSO}^\phi (\#)$ , even without explicit addition we can simulate addition if we avail ourselves of second-order quantification. Indeed, let $\mathsf {MSO}^\phi (\#,\times )$ be the second-order monadic fragment with products of $\#$ -terms (in fact, binary products suffice). Echoing observations dating back to Skølem [Reference Skølem119], we can thereby encode arbitrary Diophantine inequalities. Indeed, consider any such

(6.1) $$ \begin{align} m_1(\mathbf{v}) + \dots + m_k(\mathbf{v}) \geq m_1'(\mathbf{v}) + \dots + m_j'(\mathbf{v}), \end{align} $$

over variables $\mathbf {v}$ corresponding to state-descriptions over $\mathbf {P}$ . To express (6.1) in $\mathsf {MSO}^\phi (\#,\times )$ we introduce $k+j$ predicate variables $X_1,\dots ,X_{k+j}$ and consider the statement that all $X_i$ are disjoint but that $\#(X_1 \vee \dots \vee X_k) \succsim \#(X_{k+1} \vee \dots \vee X_{k+j})$ . Each monomial $m_i(\mathbf {v})$ can clearly be expressed as a product of $\#$ -terms (possibly using first-order quantification) in the original variables $\mathbf {P}$ , so we set each of these equal to the corresponding term $\# X_i$ . To define the same set of solutions as (6.1) (in the sense of Definition 4.3, so that the formula includes no free predicate variables), we existentially quantify all the variables $X_1,\dots ,X_{k+j}$ .

Given second-order quantification we can repeat the same analysis as with $\mathsf {MSO}^\phi (\sharp )$ to obtain not just the Diophantine sets, but again all arithmetical sets: the state-descriptions over $\mathbf {P}$ can themselves be quantified arbitrarily. Hence, this system $\mathsf {MSO}^\phi (\#,\times )$ is precisely equivalent to $\mathsf {MSO}^\phi (\sharp )$ . Analogously to $\mathsf {MSO}^\phi (\#,\times )$ , restricting to vectors of length $2$ suffices. We leave more fine-grained analysis of fragments of these systems (e.g., the purely first-order fragment) for future explorations.

6.3 Other arithmetical operations

Aside from addition and multiplication, we could naturally consider a host of other common arithmetical functions and relations. As an example, unlike addition and multiplication, exponentiation does not trivialize in the infinitary setting. Indeed, whereas in the finitary setting exponentiation is definable from addition and multiplication (e.g., by Gödel’s famous $\beta $ function), the Generalized Continuum Hypothesis can already be stated succinctly in $\mathsf {MSO}(\#)$ with exponentiation:

$$ \begin{align*}\forall X,Y,Z.\big( |X|\approx \mathbf{2}^{|Y|} \wedge |Y|\succsim \aleph_0 \wedge |Z|\succ |Y| \rightarrow |Z| \succsim |X|\big),\end{align*} $$

where $\mathbf {2}$ abbreviates a set with cardinality two. It could be illuminating to study the properties of such a system across different models of set theory.

Another natural example is the relation of divisibility, which also arises in the study of natural language quantifiers and automata hierarchies (see Section 9.5 and in particular Proposition 9.17 (b)). A non-trivial observation in the finite case (due to Julia Robinson) is that first-order logic with divisibility and the successor function already provide the full suite of arithmetically definable relations [Reference Robinson112]. At the same time, the existential fragment of Presburger Arithmetic with divisibility is known to be decidable [Reference Lipshitz84], which leaves open the possibility that some of our systems may too remain relatively well-behaved (recall Remark 4.8). We defer these and further explicit arithmetical excursions for another occasion.

6.4 Interim summary

Table 2 lists the logical systems we have studied so far. In this monadic setting, we assess each system’s ability to reason about counting by analyzing the arithmetical content of its family of definable relations. All of these systems speak about unary predicates and their Boolean combinations, but we have been most interested in the abstract relations over cardinal numbers that sentences in these systems can define, essentially taking cardinalities of state-descriptions (or more generally, non-overlapping predicates) as numerical variables. We have seen that the landscape here is quite rich, naturally calibrated by familiar first-order arithmetical languages. With this grasp of the pure monadic fragment, we now move on to consider well-behaved fragments employing relational reasoning.

Table 2 A hierarchy of monadic counting logics, covered in Sections 2–6. Where $\mathfrak {M}$ is a structure, $\mathcal {D}(\mathfrak {M})$ are the first-order definable relations over the domain of $\mathfrak {M}$ , while $\mathcal {D}_{\mathsf {qf}}(\mathfrak {M})$ are the relations definable by quantifier-free formulas

7.1 Language and semantics

The language of propositional modal logic with counting, $\mathcal {L}_\#^{\mathsf {ml}}$ , has a syntax defined inductively as follows:

$$ \begin{align*}\varphi \quad := \quad p \;\; \mid \;\; \neg \varphi \;\; \mid \;\; \varphi \wedge \psi \;\;\mid \;\; \#\varphi \succsim \#\psi \;.\end{align*} $$

The depth of formulas is defined recursively as for our earlier logics, with standard clauses for atoms p and Booleans, while $\mathsf {d}(\#\varphi \succsim \#\psi ) = \mbox {max}(\mathsf {d}(\varphi ), \mathsf {d}(\psi )) + 1$ .

The semantics of this language uses standard modal relational models $\mathfrak {M} = (W, R, V)$ . At points in these models, we define truth of formulas, and term values in a mutual recursion. For a point s we write $R_s = \{t: Rst\}$ for its R-successors. Here are the two key clauses:

• • ${[\![{ {\#\varphi } }]\!]}^{\mathfrak {M}, s} = | R_s \cap {[\![{ {\varphi } }]\!]}^{\mathfrak {M}} |$ ,

• • $\mathfrak {M}$ , $s \models \#\varphi \succsim \#\psi $ iff ${[\![{ {\#\varphi } }]\!]}^{\mathfrak {M}, s} \geq {[\![{ {\#\psi } }]\!]}^{\mathfrak {M}, s}$ .

Given this, we define an existential modality $\Diamond \varphi $ as $\#\varphi \succ \#\bot $ , and using negation we can then also define its universal dual $\Box \varphi $ . There is also some definability for the Booleans, as we saw with $\mathsf {MFO(\#)}$ , but we will let this rest here. Call the resulting system $\mathsf {ML}(\#)$ . As before, we denote the logic interpreted over finite models by $\mathsf {ML}^\phi (\#)$ .

As for expressive power, iterated counting in this simple modal language can produce non-trivial assertions. The reader might consider the formula $\#(\#\neg p \succ \# p) \succ \#(\#p \succsim \#\neg p)$ , and determine what this says numerically, for instance, on finite trees. An example model is depicted in Figure 3. One can also enforce infinity of some sets of successors. E.g., the modal formula $\Diamond q \wedge \#(p \wedge \neg q) \approx \#(p \vee q)$ requires an infinity of successors satisfying p.

Figure 3 An example model in which $\#(\#\neg p \succ \# p) \succ \#(\#p \succsim \#\neg p)$ holds at the root point. The points where p holds are shaded. The number of successors with more non-p successors than p successors is greater than the number of successors with at least as many p successors as non-p successors.

7.2 Some basic model theory

Here are some invariance properties of our modal counting language that are useful for studying its expressive power.

A generated submodel of a modal model is a submodel that is closed under taking R-successors (see, e.g., [Reference Blackburn, de Rijke and Venema17]). Given the ‘forward-looking’ nature of the modal counting language along the order R, the following is a counterpart of the analogous invariance property for the basic modal language.

The Finite Depth Property of modal logic also goes through, where ‘finite depth’ refers to the following cut-off versions of our models: $\mathfrak {M}|_n, s$ is the submodel of $\mathfrak {M}$ consisting of only those points that can be reached from s in at most n relational steps.

The following invariance property refers to the standard tree unraveling of arbitrary relational models yielding tree-like models in basic modal logic [Reference Blackburn, de Rijke and Venema17].

Finally define duplication of a tree as making copies of all immediate successors of the root: each successor t splits into $t_1, t_2$ each heading a disjoint copy of the original subtree at t. This construction can also be defined for models in general, and it can also be iterated going down the tree [Reference van Benthem13], but we will not use this generality here.

These invariance properties put limits on expressive power. For instance, our counting logic $\mathsf {ML(\#)}$ does not contain the well-known system of graded modal logic that describes specific finite numbers of successors [Reference Fine41].

In fact, $\mathsf {ML(\#)}$ and graded modal logic are incomparable in expressive power; see [Reference Demri and Lugiez30] for a more powerful system that subsumes both.

7.3 Bisimulation

Behind the above preservation facts lies a general notion of bisimulation for $\mathcal {L}_\#^{\mathsf {ml}}$ . For convenience, we define this to be a standard modal bisimulation [Reference Blackburn, de Rijke and Venema17] satisfying a further requirement of cardinality comparison between sets satisfying a structural property matching modal definability.

See Figure 4. Note: in Clause (a), we mean that the sets $X, Y$ are $\sim _Z$ -closed with respect to successors of s, not necessarily in the whole model $\mathfrak {M}$ , and likewise in Clause (b).

Figure 4 An ordinary modal bisimulation Z between $\mathfrak {M}$ and $\mathfrak {N}$ is depicted by the dotted lines. In both of these models the root point has four $\sim _Z$ -closed sets of successors: the empty set, the whole set, and the two encircled sets. To be a $\#$ -bisimulation (Definition 7.8), the same ordering of these sets by cardinality must hold in each, as it does here.

To understand what the map $Z[X] \cap R_t$ does, note that $R_t - Z[X]$ = $Z[R_s -X]$ , given the $\sim _Z$ -closedness of X and the fact that Z is a modal bisimulation.

Bisimulation invariance can be used to show that certain notions are not definable.

As in general modal logic, converse results require additional conditions. We formulate two versions, starting with a Hennessy–Milner result for ‘image-finite’ models where each point has only finitely many relational successors.

Still, the common assumption of image-finiteness runs counter to the fact that $\mathsf {ML}(\#)$ can also compare infinite cardinalities among successors. To reach a perfect correspondence we can employ another device, passing to an infinitary modal language, allowing conjunctions and disjunctions of arbitrary sets of formulas. Call this language $\mathcal {L}_\#^{\infty \mathsf {ml}}$ .

For a first study of standard modal themes like bisimulation and frame correspondence for $\mathsf {ML}(\#)$ and its extensions, see [Reference Fu and Zhao42].

7.4 Normal forms for $\mathsf {ML}(\#)$

The modal counting language admits syntactic normal forms that combine standard normal forms for modal logic with the numerical equational normal forms that we found for $\mathsf {MFO(\#)}$ . The idea is to start with the earlier state descriptions, and then describe inductively, for successors at increasing distance, which types occur with which multiplicity. In what follows, we fix a finite vocabulary of proposition letters.

The inductive step in this definition makes sense because it is easy to show inductively that the set of n-types is finite for each n. To understand this definition, note that modal types record inductively which types of lower rank are present and absent on successors of given points. $\mathsf {ML}(\#)$ merely enriches this to more precise numerical information.

Here are two points of comparison with the earlier normal forms for monadic counting logic. First, we cannot compress our modal normal forms further to depth 1 as we did for $\mathsf {ML}(\#)$ in Section 3. Their simplicity is rather in that each level of counting refers to points farther away in the modal accessibility structure, so, intuitively, nested count information refers to different positions. Next, normal forms for the monadic counting language are ‘loose’ in that they do not necessarily contain complete information about all regions in the model. The difference is slight, since, by the linearity of the cardinality order, loose forms can be expanded to disjunctions of complete forms. (We implicitly invoked this fact already when stating Corollary 3.4 in Section 3.) In the modal case, we could also allow loose forms, but we chose the complete version because of the following point.

Normal forms are related to Scott sentences in infinitary languages, describing, up to suitable ordinal depths, what syntactic types in the language are realized in a given model [Reference Scott, Addition, Henkin and Tarski117]. Modal Scott sentences in $\mathcal {L}_\#^{\infty \mathsf {ml}}$ also include information on numbers of occurrences of types, and can define given pointed models up to bisimulation.

7.5 Language extensions

Our modal language is still quite weak in some respects. For instance, unlike the system $\mathsf {MFO}(\#)$ , it cannot talk about specific finite numbers of relevant objects: in our case, successors of the current point. In addition, we still lack the resources to express further features of the earlier-mentioned Pigeonhole Principle

(7.1) $$ \begin{align} \#_x\exists y. R(y,x) \succ \#_x\exists y. R(x,y) \rightarrow \exists x. \exists^{\geq 2} y. R(y,x). \end{align} $$

A modal rendering of the $\mathsf {FO}(\#)$ -style syntax with explicit variables in this principle requires (a) numerical graded modalities, (b) both forward $\Diamond ^{\rightarrow }$ and backward $\Diamond ^{\leftarrow }$ modalities along the ordering R, and also, (c) the notion of counting involved is not local to some current point, but involves a global operator $\#_g$ , referring to the whole domain. With these modal devices, the Pigeonhole Principle will come to look like this:

(7.2) $$ \begin{align} \#_g \Diamond^{\rightarrow}\top \succ \#_g \Diamond^{\leftarrow}\top \rightarrow E \Diamond^{\leftarrow, \geq 2} \top, \end{align} $$

where the ‘existential modality’ E is defined as having global count greater than 0.

We briefly discuss these extensions in turn. Adding graded modalities to $\mathsf {ML}(\#)$ seems natural, so as to give the system the same expressive power as $\mathsf {MFO}(\#)$ over sets of successors. In fact, Demri and Lugiez [Reference Demri and Lugiez30] present a generalized graded modal logic with Presburger-like constraints on types of successors which extends our system $\mathsf {ML}(\#)$ . Given our analysis of additive arithmetic in terms of second-order counting logics, there may be connections here with the second-order version of $\mathsf {ML}(\#)$ mentioned below in Example 9.9.

Next, adding backward modalities for the converse of the accessibility relation leads to a tense-logical version of $\mathsf {ML}(\#)$ . While such an extension seems straightforward, several earlier notions would need non-trivial adaptation. Moreover, the typical valid tense-logical principles $ \varphi \rightarrow \Box ^{\rightarrow }\Diamond ^{\leftarrow }\varphi ,\varphi \rightarrow \Box ^{\leftarrow }\Diamond ^{\rightarrow }\varphi $ relating the two directions of R suggest a more systematic analysis of the connections between counting in the forward and backward directions.

Also of interest is adding global counting operators, which, as noted above, can define the usual global existential modality over the whole domain. Extending the well-known fact that standard modal $\mathsf {S5}$ provides an alternative notation for monadic first-order logic without identity, we could also consider global counting as a device by itself, yielding another presumably simple modal counterpart to the system $\mathsf {MFO}(\#)$ .

Of course, beyond $\mathsf {MFO}(\#)$ , the other systems considered in earlier sections, too, suggest modal extensions. For instance, an analogue to the notion of multiple counting in $\mathsf {MFO}(\sharp )$ might involve ‘multi-dimensional’ modal counting logics [Reference Marx and Venema85]. Perhaps more importantly in representing natural patterns of reasoning, one can add second-order quantifiers over sets, on the analogy of the earlier system $\mathsf {MSO}(\#)$ . This would result in a second-order version of $\mathsf {ML}(\#)$ comparable to basic modal logic with quantifiers over propositions [Reference Fine40]. In fact, if we add quantification over proposition letters to $\mathsf {ML}(\#)$ with global counting, then this gives us an alternative, modal notation for sentences of $\mathsf {MSO}(\#)$ , thanks to Theorem 3.2 and Lemma 4.5.Footnote ⁵ By the same argument as in Section 4.2, such a system will be decidable (Corollary 4.13). One concrete use for it will be found in Section 9.2, when discussing quantifier constructions in natural language.

8.1 Beyond counting

We can break our interpretation of count terms $\#_x\varphi $ into two steps. In a model $\mathcal {M}$ with domain D and variable assignment s, we first consider the set ${[\![{ {\varphi } }]\!]}^{\mathcal {M},s}_x =\{d \in D: \mathcal {M}, s^x_d \models \varphi \}$ . In the second step we map subsets $S \subseteq D$ of the domain to numbers. Thus we have a map $f:\wp {(D)} \rightarrow \{\kappa : |D| \geq \kappa \}$ , with $S \mapsto |S|$ . Ultimately we set

(8.1) $$ \begin{align} {[\![{ {\#_x\varphi} }]\!]}^{\mathcal{M},s} = f({[\![{ {\varphi} }]\!]}^{\mathcal{M},s}_x). \end{align} $$

We now want to consider generalizing Equation (8.1) by allowing a broader class of functions $f:\wp {(D)} \rightarrow \mathbb {P}$ , where $\mathbb {P} = (P;\geq )$ may be some other poset than a set of cardinal numbers.

8.2 Probability and proportionality

As a first example, let $\mathbb {P} = ([0,1];\geq )$ be the real unit interval. (The rational interval $([0,1]\cap \mathbb {Q};\geq )$ would also suffice for much of what we will say.) Over finite models a natural map to consider is the function $f:\wp {(D)} \rightarrow [0,1]$ sending S to the ratio $|S|/|D|$ . It is straightforward to verify that the valid reasoning principles in the systems $\mathsf {MFO}^\phi (\#)$ and $\mathsf {MSO}^\phi (\#)$ will remain unchanged. The basic propositional and modal systems, $\mathsf {PL}^\phi (\#)$ and $\mathsf {ML}^{\phi }(\#)$ , can also be given such a proportionality interpretation whereby ${[\![{ {\#\varphi } }]\!]}^{\mathfrak {M},s}$ is the proportion of (successor) points where $\varphi $ holds.

On this interpretation, terms $\#_x\varphi $ (or $\#\varphi $ ) can be construed as specifying the probability that $\varphi $ is satisfied, a connection between elementary logics of counting and probability made explicit in [Reference van der Hoek59]. The probability measures obtained in this way are all regular in that they assign every non-empty set non-zero probability (cf. [Reference Ding, Holliday and Icard33]).

What happens when we move to polyadic systems $\mathsf {MFO}(\sharp )$ and $\mathsf {MSO}(\sharp )$ ? Some of our work has natural analogues here. For instance, recall again our analysis of ‘Many Qs are P’ (Equation (3.10)). Interpreted as a probabilistic statement about a measure $\mu $ , this says, $\mu (P\mid Q)> \mu (P)$ , i.e., that Q ‘confirms’ P [Reference Reichenbach108]. However, the two interpretations—counting and proportion—no longer agree on general logical principles when we allow poladicity:

Example 8.1. Consider the formula

$$ \begin{align*}\exists y,z.\big(y \neq z \wedge \sharp_x(x= y \vee x = z) \approx \sharp_{x,w}(P(x) \wedge P(w))\big).\end{align*} $$

This is not satisfiable under our counting interpretation since it would require $|P| = \sqrt {2}$ . By contrast, on the proportionality interpretation: it merely requires that $2 \times |D| = |P|^2$ .

This echoes a broader theme that reasoning about conditional probabilities already amounts to general reasoning about real fields [Reference Ibeling, Icard, Mierzewski and Mossé63, Reference Mossé, Ibeling and Icard93].

8.3 Mass, weight, and abstract values

Probability and proportionality are still clear quantitative numerical measures of sizes and ratios. However, generalizing beyond these, our logics also support more qualitative interpretations as calculi of ‘weight’ or ‘mass’ [Reference Link83]. In the above two-step setup, we can think of terms $\#_x\varphi $ as denoting a collective entity in some intuitive sense, say, like in the semantics of plural expressions and mass terms in natural language. The values assigned to these might lie in some qualitative mereological algebra. The minimum needed for interpreting our $\#$ -languages is then some pre-order on this mereological algebra, while further structure may come in the form of, not addition or multiplication, but fusion, and perhaps other mereological primitives [Reference Leśniewski79].

We will not pursue this more general perspective here, which deserves a separate development of its own. Instead, we only note two changes from our earlier logical analysis.

8.4 Non-classical logics

Recall that in Section 2.1, we pointed at different logics, classical or non-classical, to come out of the counting component of our systems. In the current generalized setting, ways of inducing logical operations multiply. For instance, as long as $f(D) \geq f(\varnothing )$ and $f(\varnothing ) \ngeq f(D)$ , we will recover at least the classical Booleans in the same way as before via (2.3) and (2.4). However, if we merely drop the requirement that $f(D) \geq f(\varnothing )$ , we can already invalidate ‘paradoxes of material implication’ such as $\varphi \rightarrow (\psi \rightarrow \varphi )$ , while still validating some principles typical of relevant logics (see [Reference Restall110]), such as $\neg \neg \varphi \leftrightarrow \varphi $ . We leave further exploration of this way of inducing logical systems to future work.

8.5 Embedding into multisorted $\mathsf {FO}$

Our second logical observation is more technical. With a generalized semantics, some of our earlier conclusions about system behavior and complexity need to be reconsidered. Provided we only stipulate first-order conditions on the partial order $\mathbb {P}$ and on the map $f:\wp {(D)} \rightarrow \mathbb {P}$ —both natural requirements in abstract mereological semantics—we can show that the set of valid principles for $\mathsf {FO}(\#)$ becomes computably enumerable. The same style of analysis also applies to the extended system $\mathsf {FO}(\sharp )$ which allows counting tuples.

Proof Sketch

The idea here is as follows. The above generalized semantics works on three-sorted structures with a domain D of objects, a domain P of collectives or ‘predicates’ for the denotations of $\#$ -terms, and a value domain V, with a binary relation E between objects and predicates, a function $f:P\rightarrow V$ sending predicates to values, and a binary relation $\geq $ on the value domain. We can state what is needed for this to work in first-order terms, on the analogy of Henkin models for second-order logic: (a) an Extensionality principle stating that predicates standing in the E relation to the same objects are the same, and (b) a set of Comprehension principles making sure that the domain of predicates is closed under definitions in our language with finitely many parameters.

With this in place, we can translate our $\#$ -languages into this three-sorted first-order language. In particular, the $\mathsf {Tr}$ -translation of an expression $\#_x \varphi \succsim \#_x \psi $ will read

$$ \begin{align*}\exists p, q.\, \forall x \big(E(x,p) \leftrightarrow \mathsf{Tr}(\varphi)(x)\big) &\land \forall x. \big(E(x,q) \leftrightarrow \mathsf{Tr}(\psi)(x)\big) \\ & \land f(p) \geq f(q).\end{align*} $$

This translation is easily extended to multiple count operators, where the domain of available predicates now includes predicates of arbitrary finite arities, whose natural closure properties can still be described in first-order style.

Now it is straightforward to show that a formula $\varphi $ of our $\#$ -language is satisfiable in abstract value semantics iff its translation $\mathsf {Tr}(\varphi )$ is satisfiable in a three-sorted model for the above effectively axiomatized first-order theory consisting of Extensionality and Comprehension.

Incidentally, the same strategy can also bring down the complexity of second-order versions of our $\#$ -languages, as we let second-order quantifiers range, Henkin-style, over the special set of available predicates in the above three-sorted models.

The shift to a first-order perspective has noteworthy repercussions for the meta-properties of $\#$ -logics. Consider the failure of Compactness observed earlier (Proposition 2.1): this property will hold now, because of the first-order reduction outlined above.

8.6 Generalized dependence semantics

There is also a more logic-oriented approach to lowering the complexity of our initial system $\mathsf {FO}(\#)$ . In so-called generalized assignment semantics for first-order logic, models come with a range of admissible or available assignments, where gaps in the full space of all functions from variables to objects encode dependencies or correlations between variables [Reference Baltag and van Benthem5, Reference Németi, Marx, Masuch and Pólos96]. The main truth condition is now that $\mathcal {M}, s \models \exists x \varphi $ iff there exists some admissible assignment t in the model which is equal to s except for the value of x, and such that $\mathcal {M}, t \models \varphi $ .

It is known that the set of validities on generalized assignment models is decidable [Reference Németi, Marx, Masuch and Pólos96], while additional first-order principles impose further existential closure conditions on the admissible assignments, such as Church–Rosser style confluence properties that support the encoding of undecidable tiling problems, thus elucidating the assumptions underlying the undecidability of $\mathsf {FO}$ on standard models. Moreover, generalized assignment models support various decidable language extensions, such as polyadic tuple quantifiers [Reference van Benthem14], and explicit atoms expressing functional dependence of variables y on sets of variables X [Reference Baltag and van Benthem5].

To extend the semantics of $\mathsf {FO}(\#)$ to generalized assignment models, we need a stipulation as to how we are going to count in this setting. Various options may be considered given the richer environment of available vs. arbitrary assignments, but here is one that seems natural. At an assignment s in a model $\mathcal {M}$ ,

• $\#^{X}_Y \varphi $ denotes the cardinality of the set of all tuples of values taken by the set Y in those assignments in $\mathcal {M}$ that (a) agree with s on their X-values, and (b) make $\varphi $ true.

This counts ranges of values for some variables conditional on the current values of other fixed variables, leaving open the status of yet other variables occurring in the formula $\varphi $ .

In terms of this count notion, for instance, the existential quantifier (and the dependence modalities of Baltag and van Benthem [Reference Baltag and van Benthem5]) can easily be defined in the style that was introduced in Section 2.1. Moreover, functional dependence of y on X can be written as $\#^{X}_y \top (y) \approx \#^{\{x\}}_x \top (x)$ . But we can also express other notions of correlation, up to forms of independence. For instance, $\#^{X}_y \top (y) \approx \#^{\emptyset }_y \top (y)$ says that the local values of X leave a value range for y whose cardinality is equal to the total value range for y in the model.

We submit that this combination of generalized assignment semantics and count terms is interesting, but exploring its natural open problems is beyond the scope of this paper.

9.1 Quantifier expressions in logical semantics

There is a wide range of quantifier words and quantificational constructions in natural language. The quantifier vocabulary includes first-order expressions such as ‘all’, ‘some’, ‘no’, but also numerals like ‘one’, ‘two’, or combinations like ‘all except two’. But there are also higher-order expressions such as ‘most’, and expressions whose meaning is highly context-dependent such as ‘many’, ‘enough’, and so on. Moreover, the quantifier vocabulary includes comparative expressions such as ‘More A than B are C’ or ‘As many A as B are C’, or even ‘Twice as many A as B are C’.

For a basic pattern, one usually takes the binary format $Q AB$ of $\langle 1,1 \rangle $ quantifiers, with Q a quantifier expression and $A, B$ unary predicates denoting sets of objects. It is generally assumed that quantifiers in natural languages satisfy some universal constraints, such as,

• Conservativity $Q AB$ holds iff $Q A(A\cap B)$ holds.

In what follows, in line with the literature, we will assume Conservativity throughout, though most of our results could be given more general formulations. Other widely assumed constraints hold in many cases. An important one is Extension saying that the relation $Q AB$ does not depend on the total universe of objects inside which the sets $A, B$ are located. Finally, true quantifier expressions are purely numerical in the sense of satisfying the following constraint, which also played a key role in Sections 3–5:

• Permutation Invariance $Q AB$ holds iff $Q \pi [A]\pi [B]$ for any permutation $\pi :D\rightarrow D$ .

  

  Figure 5 (a) Assuming Conservativity, Extension, and Invariance, we need only be concerned with $a=A-B$ and $b=A\cap B$ . (b) The tree of numbers consists of all pairs $(a,b)$ . Highlighted are pairs in the quantifier ‘all’. (c) Examples of quantifiers and their arithmetic expressions. Note that, in addition to requiring multiplication, the quantifier ‘many’ violates Extension.

The total effect of these three conditions ties quantifiers closely to counting. To specify the meaning of a quantifier expression Q, it suffices to list its acceptance behavior on all pairs of numbers $(a, b)$ where $a = |A - B|, b = |A \cap B |$ for some $A, B$ such that $Q AB$ holds (see Figure 5a). Accordingly, Generalized Quantifier Theory studies quantifiers equally well in numerical terms as in logical ones. A typical tool in Generalized Quantifier Theory for visualizing this double perspective is the so-called tree of numbers for representing quantifiers graphically in terms of the pairs $(a,b)$ representing cardinalities $(|A-B|, |A\cap B|)$ (Figure 5b). Here a quantifier can be seen as a subset of the tree. Further special properties of quantifiers then show up as geometrical patterns in the tree. For instance, if Q is upward monotonic in its right-hand argument, Q will be closed when moving upward along an upward diagonal line from any point where it holds. Upward monotonicity in the left-hand argument shows as acceptance of the sub-quadrant generated by points $(a, b)$ where Q holds. These geometric descriptions lead to simple characterizations of all possible monotonic quantifiers, or all first-order definable quantifiers [Reference van Benthem11].

9.2 Linguistic vocabulary and $\#$ -logics

For a start, the logical system $\mathsf {MFO}(\#)$ shows various analogies with the preceding style of analysis. First in terms of general constraints, it enjoys the following well-known logical property.

This property allows us to explore valid reasoning principles in $\mathsf {MFO}(\#)$ that assume Conservativity and Extension, which did not yet come to the fore in our earlier analysis in Section 3. An illustration is the following principle of Quantity:

$$ \begin{align*}\big((\varphi)^A(B) \wedge \#(A-B) \approx \#(C-D) \wedge \#(A \cap B) \approx \#(C \cap D)\big) \rightarrow (\varphi)^C(D).\end{align*} $$

Here $(\varphi )^{A}(B)$ makes a pure cardinality statement about B inside the set A (a strong form of Conservativity) and the conclusion is that this statement would hold for any set C with the same numerical behavior with respect to D. This expresses a form of Permutation Invariance in terms of validities in $\mathsf {MFO}(\#)$ .

As for inference patterns for specific quantifiers, our Introduction highlighted numerical syllogisms with first-order quantifiers, numerals, exceptive quantifiers ‘all except at most k’, and comparative quantifiers such as ‘most’ or ‘more…than…’. Numerical syllogisms are often analyzed in practice using Venn Diagrams with number information written into the zones, as in Figure 5a. This representation was the intuitive basis for the normal forms for the system $\mathsf {MFO(\#)}$ (recall Figure 1) which encodes all of the above reasoning.

These informal comparisons can be made precise by means of definability results. Here is an illustration using the model-theoretic definability analysis presented in Section 3.3.

Thus, the first-order quantifiers of natural language are definable. But of course $\mathsf {MFO}(\#)$ can define non-first-order quantifiers too, such as ‘Most A are B’. The normal form format of Section 3 cuts across standard first-order/second-order boundaries.