Ограниченный квантор

При изучении формальных теорий логики математической ограниченные кванторы (также известные как ограниченные кванторы ) часто включаются в формальный язык в дополнение к стандартным кванторам «∀» и «∃». Ограниченные кванторы отличаются от «∀» и «∃» тем, что ограниченные кванторы ограничивают диапазон кванторной переменной. Изучение ограниченных кванторов мотивировано тем фактом, что определить, истинно ли предложение только с ограниченными кванторами, часто не так сложно, как определить, истинно ли произвольное предложение.

Примеры

Примеры ограниченных кванторов в контексте реального анализа включают:

$\forall x>0$ - для всех x , где x больше 0
$\exists y<0$ - существует y , где y меньше 0
$\forall x\in \mathbb {R}$ - для всех x, где x - действительное число
$\forall x>0\quad \exists y<0\quad (x=y^{2})$ - каждое положительное число является квадратом отрицательного числа

Ограниченные кванторы в арифметике

Предположим, что L — язык арифметики Пеано (подойдет также язык арифметики второго порядка или арифметики всех конечных типов). Существует два типа ограниченных кванторов: $\forall n<t$ и $\exists n<t$ .Эти кванторы связывают числовую переменную n с помощью числового термина t, не содержащего n, но который может иметь другие свободные переменные. («Числовые термины» здесь означают такие термины, как «1+1», «2», «2×3», « m +3» и т.д.)

Эти кванторы определяются следующими правилами ( $\phi$ обозначает формулы):

\exists n<t\,\phi \Leftrightarrow \exists n(n<t\land \phi )

\forall n<t\,\phi \Leftrightarrow \forall n(n<t\rightarrow \phi )

Есть несколько мотивов для этих кванторов.

В приложениях языка к теории рекурсии , таких как арифметическая иерархия , ограниченные кванторы не добавляют сложности. Если $\phi$ является разрешимым предикатом, тогда $\exists n<t\,\phi$ и $\forall n<t\,\phi$ также разрешимы.
В приложениях к изучению арифметики Пеано тот факт, что конкретный набор может быть определен только с помощью ограниченных кванторов, может иметь последствия для вычислимости набора. Например, существует определение простоты с использованием только ограниченных кванторов: число n является простым тогда и только тогда, когда не существует двух чисел строго меньших, чем n , произведение которых равно n . В языке не существует бескванторного определения простоты. $\langle 0,1,+,\times ,<,=\rangle$ , однако. Тот факт, что существует ограниченная кванторная формула, определяющая простоту, показывает, что простоту каждого числа можно определить вычислимым путем.

В общем, отношение натуральных чисел можно определить с помощью ограниченной формулы тогда и только тогда, когда оно вычислимо в иерархии линейного времени, которая определяется аналогично полиномиальной иерархии , но с линейными временными границами вместо полиномиальных. Следовательно, все предикаты, определяемые ограниченной формулой, являются элементарными , контекстно-зависимыми и примитивно-рекурсивными .

В арифметической иерархии арифметическая формула, содержащая только ограниченные кванторы, называется $\Sigma _{0}^{0}$ , $\Delta _{0}^{0}$ , и $\Pi _{0}^{0}$ . Верхний индекс 0 иногда опускается.

Ограниченные кванторы в теории множеств

Предположим, что L — язык $\langle \in ,\ldots ,=\rangle$ теории множеств Цермело -Френкеля , где многоточие может быть заменено операциями формирования терминов, такими как символ для операции над набором степеней . Есть два ограниченных квантора: $\forall x\in t$ и $\exists x\in t$ . Эти кванторы связывают заданную переменную x и содержат термин t , который может не упоминать x , но может иметь другие свободные переменные.

Семантика этих кванторов определяется следующими правилами:

\exists x\in t\ (\phi )\Leftrightarrow \exists x(x\in t\land \phi )

\forall x\in t\ (\phi )\Leftrightarrow \forall x(x\in t\rightarrow \phi )

Формула ZF, содержащая только ограниченные кванторы, называется $\Sigma _{0}$ , $\Delta _{0}$ , и $\Pi _{0}$ . Это составляет основу иерархии Леви , которая определяется аналогично арифметической иерархии.

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

См. также

Подтипирование - ограниченная количественная оценка в теории типов
Система F _<: — полиморфное типизированное лямбда-исчисление с ограниченной количественной оценкой.

Ссылки

Хинман, П. (2005). Основы математической логики . АК Петерс. ISBN 1-56881-262-0 .
Кунен, К. (1980). Теория множеств: введение в доказательства независимости . Эльзевир. ISBN 0-444-86839-9 .