cuantificación de recuento

Un cuantificador de conteo es un término matemático para un cuantificador de la forma "existen al menos k elementos que satisfacen la propiedad X ". En la lógica de primer orden con igualdad, los cuantificadores de conteo se pueden definir en términos de cuantificadores ordinarios, por lo que en este contexto son una notación abreviada. Sin embargo, resultan interesantes en el contexto de lógicas como la lógica de dos variables con conteo , que restringe el número de variables en las fórmulas. Además, los cuantificadores de conteo generalizados que afirman "existen infinitos" no se pueden expresar mediante un número finito de fórmulas en la lógica de primer orden.

Los cuantificadores de conteo pueden definirse recursivamente en términos de cuantificadores ordinarios.

Dejar${\displaystyle \exists _{=k}}$denotan "existen exactamente${\displaystyle k}$". Entonces

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

Dejar${\displaystyle \exists _{\geq k}}$denotan "existen al menos${\displaystyle k}$". Entonces

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

• Cuantificación de la singularidad
• cuantificador de Lindström
• Espectro de una oración

• Erich Graedel, Martin Otto y Eric Rosen. «La lógica de dos variables con conteo es decidible». En Actas del 12.º Simposio IEEE sobre Lógica en Ciencias de la Computación LICS '97 , Varsovia, 1997. Archivo Postscript OCLC 282402933 .