Räknekvantifiering

En räknekvantifierare är en matematisk term för en kvantifierare av formen "det finns minst k element som uppfyller egenskapen X ". I första ordningens logik med likhet kan räknekvantifierare definieras i termer av vanliga kvantifierare, så i detta sammanhang är de en notationsstenografi. De är dock intressanta i sammanhanget med logik som tvåvariabellogik med räkning som begränsar antalet variabler i formler. Dessutom är generaliserade räknekvantifierare som säger "det finns oändligt många" inte uttryckbara med ett ändligt antal formler i första ordningens logik.

Definition i termer av vanliga kvantifierare

Räknekvantifierare kan definieras rekursivt i termer av vanliga kvantifierare.

Låt $\exists ^{=k}$ beteckna "det finns exakt $k$ ". Sedan

{\begin{aligned}\exists ^{=0}xPx&\leftrightarrow \neg \exists xPx\\\exists ^{=k+1}xPx&\leftrightarrow \exists x(Px\land \exists ^{=k}y(y\neq x\land Py ))\end{aligned}}

Låt $\exists ^{\geq k}$ beteckna "det finns minst $k$ ". Sedan

{\begin{aligned}\geqexists ^{ 0}xPx&\leftrightarrow \top \\\exists ^{\geq k+1}xPx&\leftrightarrow \exists x(Px\land \exists ^{\geq k}y(y\neq x\land Py))\end {Justerat}}

Se även

Erich Graedel, Martin Otto och Eric Rosen. "Tvåvariabel logik med räkning kan avgöras." In Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97, Warschau. 1997. Postscript-fil OCLC 282402933