Liczenie ilościowe

Kwantyfikator zliczający to termin matematyczny określający kwantyfikator w postaci „istnieje co najmniej k elementów spełniających właściwość X ”. W logice pierwszego rzędu z równością kwantyfikatory liczące można zdefiniować za pomocą zwykłych kwantyfikatorów, więc w tym kontekście są one skrótem notacyjnym. Są jednak interesujące w kontekście logiki, takiej jak logika dwóch zmiennych z liczeniem , które ograniczają liczbę zmiennych we wzorach. Ponadto uogólnione kwantyfikatory liczące, które mówią „istnieje nieskończenie wiele”, nie są wyrażalne przy użyciu skończonej liczby formuł w logice pierwszego rzędu.

Definicja w kategoriach zwykłych kwantyfikatorów

Kwantyfikatory liczące można definiować rekurencyjnie w kategoriach zwykłych kwantyfikatorów.

Niech ${\ displaystyle \ istnieje ^ {= k}}$ oznacza „istnieje dokładnie ${\ displaystyle k}$ ”. Następnie

${\ Displaystyle {\ rozpocząć {wyrównane} \ istnieje ^{=0}xPx&\leftrightarrow \neg \exists xPx\\\exists ^{=k+1}xPx&\leftrightarrow \exists x(Px\land \exists ^{=k}y(y\neq x\land Py ))\koniec {wyrównane}}}$

Niech oznacza „istnieje co najmniej $k}$$displaystyle$ . Następnie

${\ Displaystyle {\ rozpocząć {wyrównane} \ istnieje ^ {\ geq 0}xPx&\leftrightarrow \top \\\exists ^{\geq k+1}xPx&\leftrightarrow \exists x(Px\land \exists ^{\geq k}y(y\neq x\land Py))\end {wyrównany}}}$

Zobacz też

• Kwantyfikacja wyjątkowości
• Kwantyfikator Lindströma

•   Ericha Graedela, Martina Otto i Erica Rosena. „Logika dwóch zmiennych z liczeniem jest rozstrzygalna”. W Proceedings of 12th IEEE Symposium on Logic in Computer Science LICS `97 , Warschau. 1997. Plik postscriptowy OCLC 282402933