WikiDer > Квантор ранг

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

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

Определение

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

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

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

Замечания

• Мы пишем FO [n] для множества всех Первый заказ формулы φ с ${ Displaystyle qr ( varphi) Leq п}$.
• Реляционный FO [n] (без функциональных символов) всегда имеет конечный размер, т.е. содержит конечное число формул.
• Обратите внимание, что в Prenex нормальная форма кванторный ранг φ - это в точности количество кванторов, входящих в φ.

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

• Для Логика фиксированной точки, с оператором наименьшей фиксированной точки LFP:

qr ([LFP_φ] y) = 1 + qr (φ)

...

Примеры

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

${ Displaystyle forall x существует yR (x, y)}$

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

${ Displaystyle forall xR (y, x) клин существует xR (x, y)}$

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

${ Displaystyle R (х, y) клин х neq y}$

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

${ Displaystyle forall x существует y существует z ((x neq y wedge xRy) wedge (x neq z wedge zRx))}$

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

${ Displaystyle forall x ( существует y (x neq y wedge xRy)) клин существует z (x neq z wedge zRx))}$

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

• Prenex нормальная форма
• Игра Эренфойхта
• Квантификатор

использованная литература

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

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

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