Cuantificación de conteo

Término lógico matemático

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 abreviatura de notación. Sin embargo, son interesantes en el contexto de lógicas como la lógica de dos variables con conteo que restringen el número de variables en las fórmulas. Además, los cuantificadores de conteo generalizados que dicen "existen infinitos" no se pueden expresar utilizando un número finito de fórmulas en la lógica de primer orden.

Definición en términos de cuantificadores ordinarios

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

Sea "existen exactamente ". Entonces ${\displaystyle \exists ^{=k}}$ ${\displaystyle k}$

${\displaystyle {\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}}}$

Sea "existen al menos ". Entonces ${\displaystyle \exists ^{\geq k}}$ ${\displaystyle k}$

${\displaystyle {\begin{aligned}\exists ^{\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{aligned}}}$

Véase también

• Cuantificación de unicidad
• Cuantificador de Lindström

Referencias

• 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 informática LICS '97 , Varsovia, 1997. Archivo Postscript OCLC  282402933