Подсчет количественных показателей

Математический логический термин

Квантор подсчета — это математический термин для квантификатора вида «существует по крайней мере k элементов, удовлетворяющих свойству X ». В логике первого порядка с равенством квантификаторы подсчета можно определить в терминах обычных квантификаторов, поэтому в этом контексте они являются сокращенной записью. Однако они интересны в контексте логик, таких как двухпеременная логика с подсчетом , которая ограничивает количество переменных в формулах. Кроме того, обобщенные квантификаторы подсчета, которые говорят «существует бесконечно много», не могут быть выражены с использованием конечного числа формул в логике первого порядка.

Определение в терминах обычных квантификаторов

Квантификаторы подсчета можно определить рекурсивно в терминах обычных квантификаторов.

Пусть обозначает «существует ровно ». Тогда ${\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}}}$

Пусть обозначает «существует по крайней мере ». Тогда ${\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}}}$

Смотрите также

• Количественная оценка уникальности
• Квантификатор Линдстрема

Ссылки

• Эрих Грэдель, Мартин Отто и Эрик Розен. «Двухпараметрическая логика с подсчетом разрешима». В трудах 12-го симпозиума IEEE по логике в компьютерных науках LICS `97 , Варшава. 1997. Файл постскриптума OCLC  282402933