title: Counting quantifier
text: # Counting quantifier
  
  Un counting quantifier è un quantificatore della forma "esistono almeno k elementi che soddisfano la proprietà X ". Nella logica del primo ordine possono essere definiti mediante i quantificatori ordinari, quindi si tratta di una notazione più compatta.
  
  Tuttavia, sono interessanti nel contesto della logica a due variabili che limita il numero di variabili nelle formule. Inoltre, i counting quantifier generalizzati , in quanto si riferiscono a un numero infinito di elementi, non sono esprimibili mediante un numero finito di formule della logica del primo ordine.
  
  ## Definizione rispetto ai quantificatori ordinari
  
  I counting quantifier possono essere definiti in modo ricorsivo in termini di quantificatori ordinari.
  
  * Sia $\exists ^{=k}$ e si legga "esistono esattamente $k$ elementi". Allora:
  
      ${\begin{aligned}\exists ^{=0}xF(x)&\leftrightarrow \neg \exists xF(x)\\\exists ^{=k+1}xF(x)&\leftrightarrow \exists x(F(x)\land \exists ^{=k}y(y\neq x\land F(y)))\end{aligned}}$
  * Sia $\exists ^{\geq k}$ e si legga "esistono almeno $k$ elementi". Allora:
  
      ${\begin{aligned}\exists ^{\geq 0}xF(x)&\leftrightarrow \top \\\exists ^{\geq k+1}xF(x)&\leftrightarrow \exists x(F(x)\land \exists ^{\geq k}y(y\neq x\land F(y)))\end{aligned}}$
  