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 ${\mathrm{\exists }}^{=k}$ e si legga "esistono esattamente $k$ elementi". Allora:

$\begin{array}{cc}{\mathrm{\exists }}^{=0}xF(x)& \leftrightarrow \mathrm{\neg }\mathrm{\exists }xF(x)\\ {\mathrm{\exists }}^{=k+1}xF(x)& \leftrightarrow \mathrm{\exists }x(F(x)\wedge {\mathrm{\exists }}^{=k}y(y\ne x\wedge F(y)))\end{array}$

• Sia ${\mathrm{\exists }}^{\ge k}$ e si legga "esistono almeno $k$ elementi". Allora:

$\begin{array}{cc}{\mathrm{\exists }}^{\ge 0}xF(x)& \leftrightarrow \mathrm{\top }\\ {\mathrm{\exists }}^{\ge k+1}xF(x)& \leftrightarrow \mathrm{\exists }x(F(x)\wedge {\mathrm{\exists }}^{\ge k}y(y\ne x\wedge F(y)))\end{array}$

Bibliografia

• Erich Graedel, Martin Otto, and Eric Rosen. "Two-Variable Logic with Counting is Decidable." In Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau. 1997. file Postscript Template:Oclc

Voci correlate

• Unicità

Template:Controllo di autorità Template:Portale