%\documentstyle[11pt]{article} \documentstyle{jancl} \pagestyle{empty} \newtheorem{myth}{Theorem} \newtheorem{mylem}{Lemma} \newtheorem{mycol}[myth]{Corollary} \title{Computational semantics for monadic quantifiers\thanks{The research reported here has been supported by the research grant of Polish National Commitee of Scientific Research (KBN) 433/H01/95/08.}} \author{Marcin Mostowski\\ 02--372 Warszawa \\ Opaczewska 25 m. 6 \\ Poland\\ e-mail:{\tt marcinmo@plearn.bitnet}} \begin{document} \maketitle \thispagestyle{empty} \begin{abstract} The paper gives a survey of known results related to computational devices (finite and push--down automata) recognizing monadic generalized quantifiers in finite models. Some of these results are simple reinterpretations of descriptive---feasible correspondence theorems from finite--model theory. Additionally a new result characterizing monadic quantifiers recognized by push down automata is proven. \end{abstract} The aim of the work is presentation of the state of knowledge and main research problems in computational approach to finite interpretations of monadic generalized quantifiers. We will concentrate on purely logical approach -- that is we will consider mainly structures without standard linear orderings. However proper results for linearly ordered structures will be mentioned when relevant. Let us observe that monadic quantifiers -- being the first natural class of quantifiers investigated from computational point of view -- are not systematically treated in logical literature. In the first attempt \cite{MakPnu93} of surveying the subject of generalized quantifiers from computational point of view, monadic quantifiers are only shortly mentioned. \section{Generalities} By monadic generalized quantifiers we mean Lindstr{\"o}m's quantifiers (see \cite{Lind66}) of types of the form $(1,1, \ldots , 1)$; if the number of ones in the type signature is $n$ then we say that the corresponding quantifier is a monadic $n$-ary quantifier. Syntactically it binds one variable in $n$ formulae. More precisely for each $n$--ary monadic quantifier $Q$ we define the logic $L(Q)$ as an extension of elementary (first order) logic. The set of $L(Q)$--formulae is obtained by adding to the standard construction rules the following: if $x$ is a variable and $\varphi_1, \ldots, \varphi_n$ are formulae then also $Q x (\varphi_1, \ldots, \varphi_n)$ is a formula. Semantically $n$-ary monadic quantifier $Q$ can be represented by closed on isomorphisms class $K_Q$ of structures of the form $(U, R_1, \ldots , R_n)$, where $U \neq \emptyset$ and $R_i \subseteq U$, for $i = 1, 2, \ldots , n$. The definition of the satisaction relation is extended by the following: \noindent for any model $M$, and a valuation ${\bf a}$ in $M$: \noindent $M \models Q x (\varphi_1, \ldots, \varphi_n) [{\bf a}]$ if and only if $(|M|, \varphi_1^{M,x,{\bf a}}, \ldots, \varphi_n^{M,x,{\bf a}}) \in K_Q$, \noindent where $|M|$ is the universe of $M$, and $\varphi^{M,x,{\bf a}}$ is the set defined by $\varphi$ in $M$ with respect to the variable $x$, under the valuation ${\bf a}$ -- free in $\varphi$ variables different than $x$ are interpreted according to the valuation ${\bf a}$.\footnote{For the discussion of the general definition of Lindstr{\"o}m quantifiers see e.~g. \cite{Lind66} or \cite{KM95}.} %\pagebreak The class $K_Q$ can be represented by the set of nonempty words $F_Q$ over the alphabet $A = \{ a_0, a_1, \ldots , a_{2^n-1} \}$ such that \\ {\em $\alpha \in F_Q$ if and only if there is $(U, R_1 , \ldots , R_n) \in K_Q$ and a linear ordering $U = \{ b_1 , \ldots , b_k \}$ such that $lh(\alpha) = k$, and $i$-th character of $\alpha$ is $a_j$ exactly when $b_i \in S_1 \cap \ldots \cap S_n$, where} \[ S_l = \left\{ \begin{array}{ll} R_l & \mbox{if integer part of $j / 2^{(l-1)}$ is odd} \\ U - R_l & \mbox{otherwise} \end{array} \right. \] So defined intersections $S_1 \cap \ldots \cap S_n$ are called constituents of the proper model -- the above defined constituent is also called $j$-th constituent. Then we can think of characters $a_0, \ldots, a_{2^n - 1}$ as names of constituents. In other words our definition says that $i$--th character is $a_j$ exactly when $b_i$ belongs to $j$--th constituent. For identifying a constituent we should know which relation is taken positively and which is taken negatively. This can be calculated by writing down $j$ in binary notation, and checking whether $l$--th digit from the rigth is $1$ (positive) or $0$ (negative). For $n = 3$ this idea is ilustrated by the following picture: \begin{picture}(300,200)(10,10) \put(85,185){\makebox(0,0){$ b_1$}} \put(125,185){\makebox(0,0){$ b_2$}} \put(165,185){\makebox(0,0){$ b_3$}} \put(205,185){\makebox(0,0){$ b_4$}} \put(245,185){\makebox(0,0){$ b_5$}} \put(285,185){\makebox(0,0){$ b_6$}} \newsavebox{\I} \newsavebox{\OO} \savebox{\I}(30,30){${\bf 1}$} \savebox{\OO}(30,30){${\bf 0}$} \put(25,165){\makebox(0,0){$ R_3:$}} \put(65,145){\frame{\usebox{\I}}} \put(105,145){\frame{\usebox{\I}}} \put(145,145){\frame{\usebox{\I}}} \put(185,145){\frame{\usebox{\OO}}} \put(225,145){\frame{\usebox{\I}}} \put(265,145){\frame{\usebox{\OO}}} \put(25,125){\makebox(0,0){$ R_2:$}} \put(65,105){\frame{\usebox{\I}}} \put(105,105){\frame{\usebox{\OO}}} \put(145,105){\frame{\usebox{\I}}} \put(185,105){\frame{\usebox{\I}}} \put(225,105){\frame{\usebox{\I}}} \put(265,105){\frame{\usebox{\I}}} \put(25,85){\makebox(0,0){$ R_1:$}} \put(65,65){\frame{\usebox{\OO}}} \put(105,65){\frame{\usebox{\I}}} \put(145,65){\frame{\usebox{\I}}} \put(185,65){\frame{\usebox{\I}}} \put(225,65){\frame{\usebox{\I}}} \put(265,65){\frame{\usebox{\OO}}} \put(25,25){\makebox(0,0){$ \alpha:$}} \put(85,25){\makebox(0,0){$ a_6$}} \put(125,25){\makebox(0,0){$ a_5$}} \put(165,25){\makebox(0,0){$ a_7$}} \put(205,25){\makebox(0,0){$ a_3$}} \put(245,25){\makebox(0,0){$ a_7$}} \put(285,25){\makebox(0,0){$ a_2$}} \put(180,5){\framebox(40,190){}} \sbox{\I}{} \sbox{\OO}{} \end{picture} \vspace{20pt} Particularly, when $b_4 \not \in R_1$ and $b_4 \in R_2 \cap R_3$, then the fourth character of the word $\alpha$ is $a_3$. \\ Let ${\cal C}$ be a class of recognizing devices, and ${\cal Q}$ be a class of monadic quantifiers. We say that {\em ${\cal C}$ accepts ${\cal Q}$ if and only if for each $n > 0$ and each $n$--ary monadic quantifier $Q$ $( Q \in {\cal Q} \Leftrightarrow \exists M \in {\cal C} ( M$ accepts $ F_Q )$.} \\ %\pagebreak Originally these concepts were introduced by B{\"u}chi (see \cite{Ladner77}), who investigated models with fixed linear orderings. Of course when no ordering is fixed then classes $F_Q$ are closed on permutations in the sense that if $\alpha \in F_Q$ and $\alpha'$ is obtained from $\alpha$ by arbitrary shuffling characters then $\alpha' \in F_Q$. Interpretations of monadic quantifiers in this spirit were first investigated in \cite{Benth86} and \cite{Benth87}. we have the following straightforward: \begin{mylem} For each monadic quantifiers $Q_1, Q_2$ of the same type there are quantifiers being their intersection, union, and the complement of $Q_1$, defined by sets of words $F_{Q_1} \cap F_{Q_2}$, $F_{Q_1} \cup F_{Q_2}$, and $A^* - F_{Q_1} - \{ \varepsilon \}$ respectively. \end{mylem} If the class of quantifiers is closed on all the above operations then we will say that it is closed on boolean combinations. Considering monadic quantifiers in presence of linear ordering can be understood as follows: Instead of a monadic quantifier $Q$ of type $(1,1, \ldots, 1)$, we consider a generalized quantifier $Q'$ of type $(2,1,1, \ldots, 1)$ (with the same number of ones), and we assume that in our language we have one binary predicate symbol $<$, which is always interpreted as a linear ordering --- what is equivalent to saying that we consider only models for the theory of linear ordering in terms of $<$. Then we interpret formulae of the form $$Q x (\varphi_1, \ldots, \varphi_m)$$ as $$Q' x y ( x < y, \varphi_1, \ldots, \varphi_m).$$ A similar remark apply to the Ramsey quantifier ${\sf Q}^2$, introduced by Macintyre (see \cite{KM95}). \section{First Characterizations} The first characterization of quantifiers in finite models from computational point of view has been given by van Benthem.\footnote{Other older results mentioned in this paper are essentially reinterpretations of theorems about descriptive---feasible correspondences, originally formulated in terms of classes of models.} \begin{myth} {\bf (straightforward generalization of \cite{Benth87})}% \label{th:benth:e} Finite automata with only 1--loops accept the class of all monadic elementary definable quantifiers. \end{myth} Because of the following \begin{myth} {\bf (see \cite{MM93c}\footnote{This theorem follows also from the last theorem in \cite{vaa}, which says, among others, that monadic second--order logic in monadic vocabulary is semantically equivalent to elementary logic.})} Monadic quantifiers definable in monadic second order logic are elementary definable. \end{myth} we have also \begin{mycol} Finite automata with only 1--loops accept the class of all monadic quantifiers definable in monadic second order logic. \end{mycol} These results can be contrasted with the following: \begin{myth} {\bf (B{\"u}chi, Ladner, see \cite{Ladner77}\footnote{ This theorem follows from works of B{\"u}chi. However Ladner gave its reinterpretation in the spirit of finite--model theory.})} \begin{enumerate} \item In presence of linear ordering star--free finite automata accept elementary definable monadic quantifiers. \item In presence of linear ordering finite automata accept monadic quantifiers definable in monadic second order logic. \end{enumerate} \end{myth} The above theorem is essentially reinterpretation of Ladner's formulation, which was not given in terms of quantifiers, but definable classes of models. Reinterpretation of other results from finite--model theory in terms of quantifiers has been done in the first general survey devoted to generalized quantifiers in finite models by Makowsky and Pnueli \cite{MakPnu93}.\footnote{As far as I know the first paper dvoted to generalized quantifiers in finite models is \cite{vaa}.} In their paper they give also some new results, particularly, related to mutual interpretations of languages with generalized quantifiers in finite models. %\pagebreak \section{Divisibility Quantifiers and Finite Automata} For $n \geq 2$ by divisibility quantifier ${\sf D}_n$ we mean the quantifier of type $(1)$ such that \\ ${\sf D}_n x \varphi$ if and only if the number of $x$ satisfying $\varphi$ is divisible by $n$. \\ Divisibility logic $L({\sf D}_{\omega})$ is elementary logic enriched by all quantifiers ${\sf D}_n$, for $n \geq 2$. Divisibility logic is equivalent to the logic with quantifiers {\em counting modulo} (see e.~g. \cite{STT88}). \begin{myth}[\cite{MM93b}] Finite automata accept the class of all monadic quantifiers definable in $L({\sf D}_{\omega})$. \end{myth} %\pagebreak {\bf Proof.} We will discuss here only the simplest case of unary monadic quantifier $Q$ such that $F_Q$ is regular. Our alphabet $A$ is $\{ 0, 1 \}$. Following \cite{MM93b} we will describe the automaton recognizing $F_Q$. We define the standard equivalence relation $\approx $ as follows $\alpha \approx \beta $ iff for every $\gamma \in \{0,1\}^{*} (\alpha \gamma \in F_Q$ iff $\beta \gamma \in F_Q)$. Let $k$ be the smallest number such that $0^{k} \approx 0^{i}$, for some $i > k$, and $n$ be the smallest such that $0^{k} \approx 0^{n}$ and $n > k$. Numbers $p$ and $m$ are defined in the same way taking 1 in the place of 0. %\pagebreak Let us consider the following automaton ${\cal A} = (S,\{0,1\},\delta ,s_{00},F)$ %%%%%%%%%%%%%%%%%%%%% % \newcommand{\state}[4]{\put(#1,#2){\makebox(0,0){$\bullet$}} \put(#1,#2){\makebox(48,15)[l]{$\ \ s_{#3,#4}$}}} % \newcommand{\arrow}[5]{\put(#1,#2){\vector(#3,#4){#5}}} % \newcommand{\ArrL}[2]{\arrow{#1}{#2}{-1}{0}{90}} % \newcommand{\ArrU}[2]{\arrow{#1}{#2}{0}{1}{90}} % \newcommand{\arrD}[2]{\arrow{#1}{#2}{0}{-1}{22}} % \newcommand{\arrR}[2]{\arrow{#1}{#2}{1}{0}{22}} % \begin{picture}(250,250) % \thicklines % \state{10}{210}{0}{0} \state{10}{110}{k}{0} \state{10}{10}{n-1}{0} \state{110}{210}{0}{p} \state{110}{110}{k}{p} \state{110}{10}{n-1}{p} \state{210}{210}{0}{m-1} \state{210}{110}{k}{m-1} \state{210}{10}{n-1}{m-1} % \arrD{10}{205} \arrD{10}{140} \arrD{10}{105} \arrD{10}{40} % \arrD{110}{205} \arrD{110}{140} \arrD{110}{105} \arrD{110}{40} % \arrD{210}{205} \arrD{210}{140} \arrD{210}{105} \arrD{210}{40} % \arrR{15}{210} \arrR{80}{210} \arrR{115}{210} \arrR{180}{210} % \arrR{15}{110} \arrR{80}{110} \arrR{115}{110} \arrR{180}{110} % \arrR{15}{10} \arrR{80}{10} \arrR{115}{10} \arrR{180}{10} % \ArrL{205}{5} \ArrL{205}{105} \ArrL{205}{205} % \ArrU{15}{15} \ArrU{115}{15} \ArrU{215}{15} \end{picture} % \thinlines %%%%%%%%%%%%%%%%%%%%% %\vspace{20pt} where all horizontal arrows are labeled by 1, and all vertical arrows are labeled by 0. We will call this automaton: $(n,m,k,p)$-automaton. A priori we cannot expect that ${\cal A}$ will be identical with the syntactic automaton ${\cal A}'$ defined by $\approx$. However we can define proper set $F$ of accepting states in ${\cal A}$ by constructing a suitable homomorphism $f : {\cal A} \rightarrow {\cal A}'$, and defining $F$ as $f^{-1}(F')$, where $F'$ is the set of accepting states of ${\cal A}'$. So we obtain that ${\cal A}$ accepts $F_Q$. %\pagebreak %Let $ \varphi (x)$ be a %given formula of the logic $L({\sf D}_{\omega })$, % we have to find a formula $\psi$ of %$L({\sf D}_{\omega })$ equivalent to $Qx \varphi (x)$. For every state $s_{ij}\in F$ we define the formula $\psi_{ij}$ such that $\psi_{ij}$ expresses that: \\ ``{\em there are exactly $j$ $x$ such that $\varphi(x)$ and exactly $i$ $x$ such that $\neg \varphi (x)$}'', if $i < k$ and $j < p$, \\ ``{\em the number of $x$ such that $\varphi(x)$ minus $p$ is equivalent to $j - p$ modulo $m - p$ and there are exactly $i$ $x$ such that $\neg \varphi (x)$}'', if $i < k$ and $j \ge p$, \\ ``{\em there are exactly $j$ $x$ such that $\varphi(x)$ and the number of $x$ such that $\neg \varphi(x)$ minus $k$ is equivalent to $i - k$ modulo $n - k$}''\footnote{We assume here that for each $n, m$, $n \equiv m ($mod $1)$.}, if $i \ge k$ and $j < p$, \\ ``{\em the number of $x$ such that $\varphi(x)$ minus $p$ is equivalent to $j - p$ modulo $m - p$ and the number of $x$ such that $\neg \varphi(x)$ minus $k$ is equivalent to $i - k$ modulo $n - k$}'', if $i \ge k$ and $j \ge p$. \\ That ``{\em there are exactly $j$ $x$ such that $\varphi(x)$}'' is expressible in $L({\sf D}_{\omega })$ follows from that it is expressible in elementary logic. That ``{\em the number of $x$ such that $\varphi (x)$ is equivalent to $j$ modulo $s$}'' can be expressed in $L({\sf D}_{\omega })$ by the following formula: $\exists x_{1}\ldots \exists x_{j}(\varphi (x_{1}) \wedge \ldots \wedge \varphi(x_{j}) \wedge \bigwedge_{1\le a 1$ cannot be recognized by PDA. In this section we will consider also quantifiers of type $(1)$ accepted by deterministic PDA. However firstly we will recall some basic concepts related to Push--Down Automata (PDA). A push--down automaton is of the form ${\cal A} = (A, \Sigma, S, s_0, F, \delta)$, where $A$ is an input alphabet, $\Sigma$ -- stack alphabet, $S$ -- a set of internal states, $s_0 \in S$ is an initial state, $F \subseteq S$ is a set of accepting states, and finally $$\delta : (A \cup \{ \varepsilon \}) \times S \times \Sigma \longrightarrow P(S \times \Sigma^{*})$$ is a transition function. The function $\delta$ describes the behaviour of ${\cal A}$ in the following sense: When reading a word the automaton ${\cal A}$ pops an element $\sigma$ from the top of the stack, reads a character $a \in A$ (or nothing in a case of so called $\varepsilon$--moves), and is in a state $s \in S$, then it chooses $(s',\sigma') \in \delta(a,s,\sigma)$, and changes its internal state to $s'$, it shifts the head into the next character, and pushes the word $\sigma'$ into the top of the stack. If $\delta(\varepsilon,s,\sigma) = \emptyset$, for each $s \in S, \sigma \in \Sigma$ (there are no $\varepsilon$--moves), and $\delta(a,s,\sigma)$ always contains not more then one element, then we say that ${\cal A}$ is deterministic push down automaton, or shortly deterministic PDA, otherwise it is called nondeterministic PDA. When ${\cal A}$ is deterministic PDA then the transition function $\delta$ can be described as a partial function $$\delta : A \times S \times \Sigma \longrightarrow S \times \Sigma^{*}$$ An input word $\alpha \in A^{*}$ is accepted by ${\cal A}$ if and only if starting its work with its head on the first character of $\alpha$, being in the iternal state $s_0$, and having the stack empty, the automaton ${\cal A}$ ends reading $\alpha$ in a state belonging to $F$. If additionally the stack is empty at the end, then we say that ${\cal A}$ accepts $\alpha$ by empty stack. A set $X \subseteq A^{*}$ is recognized by ${\cal A}$ if for each $\alpha \in A^{*}$: \begin{center} $\alpha \in X$ if and only if ${\cal A}$ accepts $\alpha$. \end{center} Deterministic PDA--s recognize by arbitrary stack larger class of sets then the class recognized by empty stack, e.~g. let $L = \{ 0^n 1^k : k \leq n, k, n \in \omega \}$. $L$ is acceptable deterministically, but not by empty stack. The reason is that each PDA after reading many symbols $0$ and making the stack empty cannot memorize how many symbols $1$ can be still accepted. Let us observe that all the above concepts are defined in such the way that forgeting about stacks and stack alphabets we obtain adequate definitions of corresponding concepts related to finite automata. Let $a, b, c, d \in \omega$, by $(a,b,c,d)$--linear quantifier ${\sf Lin}_{(a,b,c,d)}$ we mean the quantifier of type $(1)$ such that ${\sf Lin}_{(a,b,c,d)} = Q_R$, where $$(*) \ \ \ \ R = \{ (x,y) \in \omega^2 : \exists z \in \omega \ \ (x,y) = (c,d)+z(a,b) \}$$ We say that a quantifier $Q$ of type $(1)$ is {\em almost linear} iff for some \\ \noindent $a, b, c_1, \ldots, c_k, d_1, \ldots, d_k \in \omega$ and some finite relation $R_0 \subseteq \omega^2$: $$Q = Q_{R_0} \cup {\sf Lin}_{(a,b,c_1,d_1)} \cup \ldots \cup {\sf Lin}_{(a,b,c_k,d_k)}.$$ In other words almost linear quantifiers are those semilinear quantifiers, which have at most one nontrivial vector $(a,b)$ in its defining relation. The ratio $a/b$ will be called the ratio of the corresponding almost linear relation. For geometrical illustration of what does it mean {\em almost linear}, let us consider a relation $S \subseteq \omega^2$ being a finite union of relations of the form $(*)$ with the same ratio $a/b$. Allowing $z$ to vary over the set of reals we can think of $S$ as a set of points on the euclidean plane. Then almost linear relation $S$ can be defined (modulo a finite set) as a finite union of straight lines $R_1, \ldots, R_m$ parallel each to other. \begin{picture}(300,200)(10,10) \put(20,20){\vector(1,0){270}} \put(292,23){$x$} \put(20,20){\vector(0,1){170}} \put(23,192){$y$} \put(30,10){\line(2,3){110}} \put(33,10){$R_1$} \put(37,21){\line(1,0){30}} \put(51,23){$a$} \put(67,21){\line(0,1){45}} \put(69,43){$b$} \put(80,10){\line(2,3){110}} \put(83,10){$R_2$} %\put(90,10){\line(2,3){180}} %\put(92,10){$R_3$} \put(160,70){${\bf \cdots}$} \put(170,10){\line(2,3){110}} \put(173,10){$R_{m}$} %\put(150,10){\line(2,3){180}} %\put(152,10){$R_m$} \end{picture} \vspace{20pt} The above picture suggests that complements of almost linear relations are never almost linear, their finite unions are almost linear only if they have the same ratio, and their intersections are either almost linear or finite. Of course deterministic PDA--s recognize by empty stack all regular quantifiers, but what more? We will show that they recognize also almost linear quantifiers. However the intersection of a regular set and a set recognized by deterministic PDA (by empty stack) is still recognized by deterministic PDA (by empty stack). We claim that nothing more (between permutation closed sets) is recognized by deterministic PDA--s by empty stack. %\pagebreak \begin{myth} The class of all quantifiers recognized by deterministic PDA--s by empty stack is the union of the following: \begin{enumerate} \item regular quantifiers, \item intersections of regular and almost linear quantifiers. \end{enumerate} \end{myth} {\bf Proof} Firstly we will show that almost linear quantifiers are recognized by deterministic PDA--s. We start with the simplest linear case without exceptions. Let $R$ be defined as above for some fixed $a, b, c, d \in \omega$. Let $Q$ be $Q_R$. Now we will describe the deterministic PDA recognizing $F_Q$. We define the stack alphabet $S$ as $\{ <$0--mile$> , <$1--mile$> \}$. \\ $<$0--mile$>$ contains $a$ steps, and $<$1--mile$>$ contains $b$ steps. \\ The behaviour of our PDA can be described by the following picture: %%%%%%%%%%%%%%%%%%%%% % \begin{picture}(250,250) % \thicklines % \put(10,210){\makebox(0,0){$\bullet$}} % \put(10,210){\line(1,0){200}} % \put(10,210){\line(0,-1){200}} % \put(10,210){\line(1,-1){200}} % \put(55,100){\makebox(0,0){$<$0--mile$>$}} % \put(20,120){\vector(0,-1){30}} % \put(100,235){\makebox(0,0){$<$1--mile$>$}} % \put(80,220){\vector(1,0){30}} % \put(120,120){\makebox(0,0){$F$}} % \end{picture} % \thinlines %%%%%%%%%%%%%%%%%%%%% %\vspace{20pt} Reading a word $\alpha$ we go to right -- when $1$ is read $b$ times, and down -- when $0$ is read $a$ times. We count miles poping and pushing them as follows: \begin{itemize} \item when we have passed one mile and the stack is empty then we push it, \item when we have passed one mile and the stack contains a mile of the same kind then we push it, \item when we have passed one mile and the stack contains a mile of another kind then we pop the mile from the stack. \end{itemize} 0--miles can be counted after reading 0 $c$--times, 1--miles can be counted after reading 1 $d$--times. The word $\alpha$ is accepted if after reading it we are staying at the line $F$ --- it means that the stack is empty. The general case allowing exceptions can be obtained by enriching our construction by some states and instructions not modifying the stack. \\ {\bf Remark} Let us observe that a similar picture can be used to justify Van Benthem's theorem \ref{th:benth:a}. \\ Let $Q' = Q_{R'}$ be defined by a semilinear $R'$, that is being a finite union of linear relations $S$ such that for some $a_1 , b_1 , \ldots , a_k $, $b_k , c , d \in \omega$ \\ $S = \{ (x,y) \in \omega^2 : \exists z_1 , \ldots , z_k (x,y) = (c,d) + z_1(a_1,b_1) + \ldots + z_k(a_k,b_k) \}$. \\ In this case for recognizing $Q_S$ we can use the same idea constructing nondeterministic PDA with $k$ kinds of $0$--miles, and $k$ kinds of $1$--miles. Our PDA will choose nondeterminstically what kind of miles have to be used for measuring distances. Therefore $F_{Q'}$ as being a finite union of context free sets is itself context free. {\bf end of Remark} \\ %\pagebreak Now let us assume that $Q$ is accepted by some deterministic push down automaton ${\cal A}$. By Parikh's theorem there is a semilinear $R'$, as described in the above remark, such that $Q = Q_{R'}$. \\ Firstly we assume that modulo finite number of exceptions $R'$ is linear, that is $R' = S \cup R_0$, where $R_0$ is finite, and for some $a_1 , b_1 , \ldots , a_k $, $b_k , c , d \in \omega$ \\ $S = \{ (x,y) \in \omega^2 : \exists z_1 , \ldots , z_k (x,y) = (c,d) + z_1(a_1,b_1) + \ldots + z_k(a_k,b_k) \}$. \\ Then we obtain two possible cases: \begin{enumerate} \item \label{caseI} for some $i = 1 , \ldots , k$ either $a_i = 0$ and $b_i \neq 0$ or $b_i = 0$ and $a_i \neq 0$, in this case $Q$ is definable by divisibility quantifiers; \item \label{caseII} all $a_1 , \ldots , a_k , b_1 , \ldots , b_k$ are different than $0$, in this case we show that $Q$ is almost linear. \end{enumerate} Let us consider in details only the case \ref{caseII}. The case \ref{caseI} is simpler, and it can be analyzed similarly. We consider the simplest case when the set $S$ is defined by three vectors: \\ $S = \{ (x,y) \in \omega^2 : \exists z_1, z_2 (x,y) = (c,d) + z_1(a_1,b_1) + z_k(a_2,b_2) \}$, \\ \noindent and no one parameter is equal to $0$. The general argument differs only by straightforward technicalities. Let us consider words: $$\alpha_x = 0^c 1^d 0^{(x a_1) a_2} 1^{(x a_1) b_2}$$ $$\beta_x = 0^c 1^d 0^{(x a_2) a_1} 1^{(x a_2) b_1}$$ Now we will show that $a_1 b_2 = a_2 b_1$. Let us assume that $a_1 b_2 < a_2 b_1$. Then for arbitrary large $n$ we can chose $x$ such that $$k = x (a_2 b_1 - a_1 b_2) > n.$$ Then $\beta_x = \alpha_x 1^k$. The automaton ${\cal A}$ after reading $\alpha_x$ is in accepting state with empty stack. It means that it cannot memorize $x$, and from this moment, not reading any zeros, it behaves like finite automaton (without stack). Chosing sufficiently large $x$ we obtain the contradiction. Therefore in the case \ref{caseII} we prove that there are natural numbers $i , j > 0$ such that for some $x_1 , \ldots , x_k$: \\ \begin{center} $(a_1 , b_1) = x_1 (i , j)$ $\vdots$ $(a_k , b_k) = x_k (i , j)$ \end{center} Moreover we can choose $x_1 , \ldots , x_k$ being relatively prime and $i , j$ being greatest possible. Then we take $a = y i$, $b = y j$, and $c' = c + i x$, $d' = d + j x$, for some suficiently large $x$, e. g. $x = x_1 \ldots x_k z$, where $y$ is the least multiplier of $(i,j)$ greater than all exceptions and $z$ is used to make $c'$ and $d'$ greater than all exceptions. For differentiating between particular $(a_i,b_i)$, for $i = 1, \ldots, k$, we need only counting modulo $y$, what can be done without using the stack. Therefore $Q$ is ${\sf Lin}_{(a,b,c',d')} \cap Q'$ modulo some finite number of exceptions, for some regular $Q'$. The general case can be obtained by a similar argument. {\bf This ends the proof.} \\ As the result we obtain the following: \begin{mycol} The complement of a quantifier $Q$ recognized by a deterministic PDA by empty stack is also recognized by deterministic PDA by empty stack if and only if $Q$ is regular. \end{mycol} Of course, by a trivial argument, the complement of a quantifier recognized by a deterministic PDA is also recognized by a deterministic PDA by arbitrary stack. \begin{mycol} The class of quantifiers recognized by deterministic PDA--s by empty stack is closed on intersections. \end{mycol} Let us observe that the assumption that accepting is by empty stack is essential here, because the class of quantifiers described above is not closed on complements. Additionally the union of an almost linear and a regular quantifier can be still recognized by a deterministic PDA but not by empty stack. Similarly as in the case of nondeterministic PDA--s no natural descriptive class of all monadic quantifiers recognized by deterministic PDA--s is not known. \\ Finally let us mention another open problem. In the paper \cite{MM91c} it was observed that in the theory of $(\omega , + )$ divisibility quantifiers are eliminable. We do not know any other monadic quantifiers being eliminable in arithmetic of addition, which are not definable in divisibility logic. Are there any such quantifiers? %\pagebreak \section{Examples} >From our work and known proprieties of finite and push--down automata we obtain the following facts: \begin{enumerate} \item {\bf Definable in $L({\sf D}_{\omega})$, regular quantifiers:} \begin{itemize} \item {\bf even}, {\bf odd}; \item counting modulo $\exists^{pq}$, for $q < p$, where $\exists^{p,q} x \varphi$ iff $ \# \{ x : \varphi \} \equiv q (mod \ p)$;\footnote{For a set $A$ by $\# A$ we denote the cardinal number of $A$.} \item $Q x ( \varphi , \psi )$ iff $ \# \{ x : \varphi \} \equiv \# \{ x : \psi \} (mod \ p)$. \end{itemize} \item {\bf Recognized by deterministic PDA--s by empty stack, but not regular quantifiers:} \begin{itemize} \item {\bf Half}, {\bf every other}, where ${\bf Half} x \varphi$ iff $ \# \{ x : \varphi \} = \# \{ x : \neg \varphi \}$; \item {\bf every third}, {\bf every fourth}, $\ldots$ , {\bf every $n$--th}, where {\bf every $n$--th} $x \varphi$ iff $n \cdot \# \{ x : \varphi \} = \# \{ x : x = x \}$; \item H{\"a}rtig quantifier, $Q_H x ( \varphi , \psi )$ iff $ \# \{ x : \varphi \} = \# \{ x : \psi \} \end{itemize} \item {\bf Recognized by deterministic PDA--s by arbitrary stack, but not by deterministic PDA--s by empty stack:} \begin{itemize} \item {\bf majority}, where {\bf majority} $x \varphi$ iff $ \# \{ x : \varphi \} > \# \{ x : \neg \varphi \}$. \end{itemize} \item {\bf Recognized by non deterministic PDA--s, but not by deterministic PDA--s:} \begin{itemize} \item {\bf two or three times more}, where the quantifier $Q$ is definned by disjunction of ${\sf Lin}_{(1,2,0,0)}$ and ${\sf Lin}_{(1,3,0,0)}$, \\ $Qx \varphi$ iff $ \# \{ x : \varphi \} = 2 \cdot \# \{ x : \neg \varphi \}$ or $ \# \{ x : \varphi \} = 3 \cdot \# \{ x : \neg \varphi \}$. \end{itemize} \item {\bf Semilinear, but not recognized by PDA--s:} \begin{itemize} \item $Qx (\varphi , \psi)$ iff $ \# \{ x : \varphi \wedge \neg \psi \} = \# \{ x : \varphi \wedge \psi \} = \# \{ x : \neg \varphi \wedge \psi \}$. \end{itemize} \end{enumerate} %\pagebreak \begin{thebibliography}{99} \bibitem{Benth86} {\sc J. van Benthem}, {\bf Essays in Logical Semantics}, D. Reidel Publishing Company 1986. \bibitem{Benth87} {\sc J. van Benthem}, {\em Towards a Computational Semantics}, in {\sc P. Gardenf{\"{o}}rs} (ed.), {\bf Generalized Quantifiers}, D. Reidel Publishing Company 1987, pp. 31--71. \bibitem{KM95} {\sc M. Krynicki} and {\sc M. Mostowski} {\em Quantifiers, Some Problems and Ideas}, in {\sc M. Krynicki}, {\sc M. Mostowski}, and {\sc L.W. Szczerba} (eds.) {\bf Quantifiers: Logics, Models and Computation} Volume I, Kluwer Academic Publishers, 1995, pp. 1--19. \bibitem{Ladner77} {\sc R. E. Ladner}, {\em Application of Model Theoretic Games to Discrete Linear Orders and Finite Automata}, {\bf Information and Control} 33 (1977), pp. 281--303. \bibitem{Lind66} {\sc P. Lindstr{\"{o}}m}, {\em First order predicate logic with generalized quantifiers}, {\bf Theoria} 32 (1966), pp. 186--195. \bibitem{MakPnu93} {\sc J. A. Makowsky} and {\sc Y. B. Pnueli} {\em Computable quantifiers and logics over finite structures}, in {\sc M. Krynicki}, {\sc M. Mostowski}, and {\sc L.W. Szczerba} (eds.) {\bf Quantifiers: Logics, Models and Computation} Volume I, Kluwer Academic Publishers, 1995, pp. 313--357. \bibitem{MM91c} {\sc M. Mostowski}, {\em Divisibility quantifiers}, in {\bf Bulletin of the Section of Logic} 20, no. 2 (1991), pp. 67--70. \bibitem{MM93b} {\sc M. Mostowski}, {\em The Logic of Divisibility}, to appear in {\bf The Journal of Symbolic Logic}. \bibitem{MM93c} {\sc M. Mostowski}, {\em Kwantyfikatory rozga{\l}{\c{e}}zione a problem formy logicznej}, (in Polish, Branched Quantifiers and the Problem of Logical Forms) in {\bf Nauka i j{\c{e}}zyk}, Wydzia{\l} Filozofii i Socjologii Uniwersytetu Warszawskiego, Warszawa 1994, pp. 201 -- 241. \bibitem{vaa} {\sc J. V{\"a}{\"a}n{\"a}nen}, {\em Remarks on generalized quantifiers and second--order logic}, in {\bf Set Theory and Hierarchy Theory}, {\sc J. Waszkiewicz}, {\sc A. Wojciechowska}, and {\sc A. Zarach} (eds.), Prace Naukowe Instytutu Matematyki Politechniki Wroc{\l}awskiej, Wroc{\l}aw 1977, pp. 117--123. \bibitem{STT88} {\sc H. Straubing, D. Th{\'{e}}rien, W. Thomas}, {\em Regular Languages Defined with Generalized Quantifiers}, {\bf Proc. 15th ICALP 88}, {\sc T. Lepist{\"{o}}} and {\sc A. Salomaa} (eds.) Lec. Notes in Comput. Sci. 317, Springer-Verlag, Berlin 1988, pp. 561--575. \end{thebibliography} \end{document}