Кванторный ранг

В математической логике кванторный ранг формулы — это глубина вложенности ее кванторов . Он играет существенную роль в теории моделей .

Обратите внимание, что ранг квантора является свойством самой формулы (т. е. выражения на языке). Таким образом, две логически эквивалентные формулы могут иметь разные кванторные ранги, когда они выражают одно и то же разными способами.

Определение

Кванторный ранг формулы на языке первого порядка (FO)

Пусть φ — формула ФО. Кванторный ранг φ, обозначаемый qr(φ), определяется как

• $qr(\varphi )=0$, если φ атомарна.
• $qr(\varphi _{1}\land \varphi _{2})=qr(\varphi _{1}\lor \varphi _{2})=max(qr(\varphi _{1}),qr(\varphi _{2}))$.
• $qr(\lnot \varphi )=qr(\varphi )$.
• $qr(\exists _{x}\varphi )=qr(\varphi )+1$.
• $qr(\forall _{x}\varphi )=qr(\varphi )+1$.

Примечания

• Обозначим FO[n] множество всех формул первого порядка φ с $qr(\varphi )\leq n$.
• Реляционный FO[n] (без функциональных символов) всегда имеет конечный размер, т.е. содержит конечное число формул
• Обратите внимание, что в нормальной форме Prenex ранг квантора φ равен точно количеству кванторов, появляющихся в φ.

Квантификатор ранга формулы более высокого порядка

• Для логики фиксированной точки с оператором наименьшей фиксированной точки LFP: $qr([LFP_{\phi }]y)=1+qr(\phi )$

Примеры

• Предложение кванторного ранга 2:

$\forall x\exists yR(x,y)$

• Формула кванторного ранга 1:

$\forall xR(y,x)\wedge \exists xR(x,y)$

• Формула кванторного ранга 0:

$R(x,y)\wedge x\neq y$

• Предложение в пренексной нормальной форме кванторного ранга 3:

$\forall x\exists y\exists z((x\neq y\wedge xRy)\wedge (x\neq z\wedge zRx))$

• Предложение, эквивалентное предыдущему, но кванторного ранга 2:

$\forall x(\exists y(x\neq y\wedge xRy))\wedge \exists z(x\neq z\wedge zRx))$

См. также

• Пренекс нормальная форма
• Эренфойхт-Фрэссе_game
• Квантор

Ссылки

• Эббингауз, Хайнц-Дитер ; Флум, Йорг (1995), Теория конечных моделей , Springer , ISBN  978-3-540-60149-4 .
• Гредель, Эрих; Колайтис, Фокион Г.; Либкин Леонид ; Мартен, Маркс; Спенсер, Джоэл ; Варди, Моше Ю .; Венема, Иде; Вайнштейн, Скотт (2007), Теория конечных моделей и ее приложения , Тексты по теоретической информатике. Серия EATCS, Берлин: Springer-Verlag , стр. 133, ISBN  978-3-540-00428-8 , Збл   1133.03001 .

Внешние ссылки

• Кванторный ранговый спектр диссертации бакалавра L-бесконечности-омеги, 2000 г.