Квантор ветвления

В логике квантор ветвления ​ также называемый квантором Хенкина , конечным частично упорядоченным квантором или даже нелинейным квантором , представляет собой квантор частичного порядка.

$\langle Qx_{1}\dots Qx_{n}\rangle$

кванторов ∈ {∀ , для Q ∃}. Это частный случай обобщенного квантора . В классической логике префиксы кванторов линейно упорядочены так, что значение переменной ym _, связанной квантором Qm _, зависит от значения переменных

y ₁ , ..., y _{м −1}

связанный кванторами

Qy ₁ , ..., Qy _{м −1}

предшествующий Q _м . В логике с (конечной) частично упорядоченной количественной оценкой это вообще не так.

Количественная оценка ветвления впервые появилась в докладе Леона Хенкина на конференции в 1959 году . Системы частично упорядоченной количественной оценки занимают промежуточное положение по силе между логикой первого порядка и логикой второго порядка . Они используются в качестве основы для Хинтикки и Габриэля Санду логики поддержки независимости .

Определение и свойства

Простейший квантор Хенкина $Q_{H}$ является

$(Q_{H}x_{1},x_{2},y_{1},y_{2})\varphi (x_{1},x_{2},y_{1},y_{2})\equiv {\begin{pmatrix}\forall x_{1}\,\exists y_{1}\\\forall x_{2}\,\exists y_{2}\end{pmatrix}}\varphi (x_{1},x_{2},y_{1},y_{2}).$

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

$\exists f\,\exists g\,\forall x_{1}\forall x_{2}\,\varphi (x_{1},x_{2},f(x_{1}),g(x_{2})).$

Он также достаточно мощный, чтобы определить квантификатор $Q_{\geq \mathbb {N} }$ (т.е. «их бесконечно много») определяется как

$(Q_{\geq \mathbb {N} }x)\varphi (x)\equiv (\exists a)(Q_{H}x_{1},x_{2},y_{1},y_{2})[\varphi (a)\land (x_{1}=x_{2}\leftrightarrow y_{1}=y_{2})\land (\varphi (x_{1})\rightarrow (\varphi (y_{1})\land y_{1}\neq a))].$

Из этого следует несколько вещей, в том числе неаксиоматизируемость логики первого порядка с $Q_{H}$ (впервые наблюдавшийся Эренфойхтом ) и его эквивалентность $\Sigma _{1}^{1}$-фрагмент логики второго порядка ( экзистенциальная логика второго порядка ) — последний результат опубликован независимо в 1970 году Гербертом Эндертоном. и В. Уолко.

Следующие кванторы также можно определить как $Q_{H}$.

• Решер: «Число φ s меньше или равно числу ψ s»

$(Q_{L}x)(\varphi x,\psi x)\equiv \operatorname {Card} (\{x\colon \varphi x\})\leq \operatorname {Card} (\{x\colon \psi x\})\equiv (Q_{H}x_{1}x_{2}y_{1}y_{2})[(x_{1}=x_{2}\leftrightarrow y_{1}=y_{2})\land (\varphi x_{1}\rightarrow \psi y_{1})]$

• Хертиг: « φ s равнозначны ψ s»

$(Q_{I}x)(\varphi x,\psi x)\equiv (Q_{L}x)(\varphi x,\psi x)\land (Q_{L}x)(\psi x,\varphi x)$

• Чанг: «Число φs равно области определения модели»

$(Q_{C}x)(\varphi x)\equiv (Q_{L}x)(x=x,\varphi x)$

Квантор Хенкина $Q_{H}$ типа (4) сам по себе может быть выражен как квантор Линдстрема .

Отношение к естественным языкам

Хинтикка в статье 1973 года выдвинул гипотезу о том, что некоторые предложения на естественных языках лучше всего понимать с точки зрения кванторов ветвления, например: «Некоторые родственники каждого жителя деревни и некоторые родственники каждого горожанина ненавидят друг друга» должны интерпретироваться, согласно Хинтикке, как:

${\begin{pmatrix}\forall x_{1}\,\exists y_{1}\\\forall x_{2}\,\exists y_{2}\end{pmatrix}}[(V(x_{1})\wedge T(x_{2}))\rightarrow (R(x_{1},y_{1})\wedge R(x_{2},y_{2})\wedge H(y_{1},y_{2})\wedge H(y_{2},y_{1}))].$

которое, как известно, не имеет логического эквивалента первого порядка.

Идея ветвления не обязательно ограничивается использованием классических кванторов в качестве листьев. В статье 1979 года Джон Барвайз предложил варианты предложений Хинтикка (как иногда называют приведенное выше), в которых внутренние кванторы сами по себе являются обобщенными кванторами , например: «Большинство жителей деревни и большинство горожан ненавидят друг друга». Наблюдая за этим $\Sigma _{1}^{1}$ не замкнут при отрицании, Барвайз также предложил практический тест, чтобы определить, действительно ли предложения естественного языка включают в себя кванторы ветвления, а именно, чтобы проверить, включает ли их отрицание на естественном языке квантификацию универсальности над заданной переменной ( $\Pi _{1}^{1}$ предложение).

Предложение Хинтикки было встречено со скептицизмом рядом логиков, поскольку некоторые предложения первого порядка, подобные приведенному ниже, по-видимому, достаточно хорошо отражают предложение Хинтикка на естественном языке.

$[\forall x_{1}\,\exists y_{1}\,\forall x_{2}\,\exists y_{2}\,\varphi (x_{1},x_{2},y_{1},y_{2})]\wedge [\forall x_{2}\,\exists y_{2}\,\forall x_{1}\,\exists y_{1}\,\varphi (x_{1},x_{2},y_{1},y_{2})]$

где

$\varphi (x_{1},x_{2},y_{1},y_{2})$

обозначает

$(V(x_{1})\wedge T(x_{2}))\rightarrow (R(x_{1},y_{1})\wedge R(x_{2},y_{2})\wedge H(y_{1},y_{2})\wedge H(y_{2},y_{1}))$

Хотя за этим последовало много чисто теоретических дебатов, только в 2009 году некоторые эмпирические тесты со студентами, обученными логике, показали, что они с большей вероятностью назначат модели, соответствующие «двунаправленному» предложению первого порядка, а не предложению с квантором ветвления нескольким естественным языковые конструкции, производные от предложения Хинтикка. Например, студентам показывали неориентированные двудольные графы (с квадратами и кругами в качестве вершин) и просили сказать, правильно ли описывают диаграммы такие предложения, как «более 3 кругов и более 3 квадратов, соединенных линиями».

См. также

• Семантика игры
• Логика зависимости
• Логика, дружественная к независимости (логика ЕСЛИ)
• Квантор Мостовского
• Квантор Линдстрема
• Непервая упорядочиваемость

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

• Теоретико-игровой квантификатор в PlanetMath.