Что выражает порядок вложенных кванторов в логике предикатов?

Один из способов интерпретировать порядок вложенных кванторов - это выражение отношений зависимости между выборами объектов, выбранных для удовлетворения формуле квантификации. Фридман в «Теории геометрии» Канта объясняет, как невозможность выразить такие зависимости в силлогистике (например, для определения пределов нужны три вложенных квантора) заставила ранние исчисления и анализ полагаться на интуитивные идеи о движении, а не на формальные конструкции. И, в свою очередь, это привело Канта к его синтетической априорной теории математического рассуждения.

Например, ∀x∃yL(x,y) означает, что существует y для каждого x, т.е. мы должны выбирать y в зависимости от x или y=f(x). Деквантованная формула — это L(x,f(x)) и x может быть выбрана свободно, тогда функция f будет обеспечивать выполнение предиката. В этом примере f является функцией поиска любви, для каждого x она находит y, которого x любит. Но ∃y∀xL(x,y) другое, означает, что есть универсальный y для всех x, константа y=c, всеми любимый, как Санта. Таким образом, формула сводится к L(x,c), другому шаблону зависимости.

Описанная процедура называется сколемизацией, и любая квантифицированная формула может быть преобразована в деквантифицированную форму с помощью функций и констант Скулема , которые явно выявляют зависимости. Универсально квантифицируемые переменные выбираются свободно, а экзистенциально квантифицируемые переменные должны выбираться в зависимости от всех универсально квантифицируемых переменных, у которых ∀ предшествует их ∃. Например, ∀x∃y∀z∃tL(x,y,z,t) означает, что x и z выбираются свободно, выбор y снова зависит только от x, поэтому y=f(x), но выбор t зависит как от x, так и от z, поэтому t=g(x,z). Сколемизированная формула — это L(x,f(x),z,g(x,z)). Перемещая квантификаторы и сколемизируя, вы увидите, как меняются зависимости удовлетворенности. Это то, что эквивалентно описывает синтаксический анализ деревьев в ответе Килана.

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

Вы можете увидеть разницу, когда создадите дерево синтаксического анализа для этих выражений:

    ∀                 ∃
   / \               / \
  x   ∃             y   ∀
     / \               / \
    y   L             x   L
       / \               / \
      x   y             x   y

 ∀x∃y L(x,y)       ∃y∀x L(x,y)

_{Примечание: создание дерева синтаксического анализа аналогично размещению неявных скобок: ∀x(∃y(L(x,y))) и ∃y(∀x(L(x,y))).}

Первый означает:

• Для всех x выполняется следующее:
  • Существует некоторый y, такой что:
    • х любит у.

Или «все кого-то любят».

Второе означает:

• Существует ay такое, что:
  • Для всех х:
    • х любит у.

Или «есть тот, кто любит всех».