Подсчет количественной оценки

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

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

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

Позволять $\exists ^{=k}$ обозначают «существуют ровно $k$". Затем

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

Позволять $\exists ^{\geq k}$ обозначают «существует по крайней мере $k$". Затем

${\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. Постскриптум . ОСЛК   282402933