Q0 (математическая логика)

Q ₀ — это Питера Эндрюса формулировка просто типизированного лямбда-исчисления ,и обеспечивает основу для математики, сравнимую с логикой первого порядка плюс теорией множеств.Это форма логики высшего порядка , тесно связанная с логикой Семейство средств доказательства теорем HOL .

Системы доказательства теорем TPS и ETPS основаны на Q ₀ . В августе 2009 года TPS выиграла первый в истории конкурс.среди систем доказательства теорем высшего порядка. ^[1]

Аксиомы Q ₀

Система имеет всего пять аксиом, которые можно сформулировать как:

$(1)$ $g_{oo}T\land g_{oo}F=\forall x_{o}[g_{oo}x_{o}]$

$(2^{\alpha })$ $[x_{\alpha }=y_{\alpha }]\supset [h_{o\alpha }x_{\alpha }=h_{o\alpha }y_{\alpha }]$

$(3^{\alpha \beta })$ $f_{\alpha \beta }=g_{\alpha \beta }=\forall x_{\beta }[f_{\alpha \beta }x_{\beta }=g_{\alpha \beta }x_{\beta }]$

$(4)$ $[\lambda \mathbf {x_{\alpha }} \mathbf {B} _{\beta }]\mathbf {A} _{\alpha }=\mathbf {S} _{A_{\alpha }}^{\mathbf {x} _{\alpha }}\mathbf {B} _{\beta }$

$(5)$ ℩ $_{i(oi)}[{\text{Q}}_{oii}y_{i}]=y_{i}\,$

(Аксиомы 2, 3 и 4 представляют собой схемы аксиом — семейства схожих аксиом. Экземпляры аксиом 2 иАксиома 3 различается только типами переменных и констант, но экземпляры Аксиомы 4 могут иметьлюбое выражение, заменяющее A и B. )

Подстрочный индекс " o " является символом типа для логических значений, а нижний индекс « i » — это символ типа для отдельных (не логических) значений. Последовательности этих представляют типы функций и могут включать круглые скобки, чтобы различать разные функции.типы. Греческие буквы с индексами, такие как α и β, являются синтаксическими переменными для типа.символы. Жирные заглавные буквы, такие как $A$ , $B$ и $C.$ являются синтаксическими переменными для WFF, а жирные строчные буквы, такие как $x$ , $y$ — синтаксические переменные для переменных. $S$ указывает на синтаксическую замену во всех свободных вхождениях.

Единственными примитивными константами являются $Q ((oα)α)$ , обозначающие равенствочленов каждого типа α и $℩ (i(oi))$ , обозначаяоператор описания индивидуумов, уникальный элемент множества, содержащего ровно одного индивидуума.Символы λ и скобки («[» и «]») представляют собой синтаксис языка.Все остальные символы являются аббревиатурами содержащих их терминов, включая кванторы ∀ и ∃.

В аксиоме 4 $x$ должен быть свободен для $A$ в $B$ ,означает, что замена не вызывает каких-либо явлений свободные переменные $A$ становятся связанными в результате подстановки.

Об аксиомах

Аксиома 1 выражает идею о том, что $T$ и $F$ являются единственными логическими значениями.
Схемы аксиом 2 ^а и 3 ^аб выражать фундаментальные свойства функций.
Схема аксиом 4 определяет природу обозначения λ.
Аксиома 5 гласит, что оператор выбора является обратным функции равенства индивидов. (При наличии одного аргумента $Q$ содержащий индивидуума. В Q ₀ отображает этого индивидуума в множество/предикат , $x = y$ является сокращением от $Qxy$ , которое является сокращением от $(Qx)y$ .) Этот оператор также известен как определенный оператор описания .

В Эндрюсе 2002 Аксиома 4 разбита на пять подразделов, которые разбивают процесс замены. Приведенная здесь аксиома обсуждается как альтернатива и доказывается из подразделов.

Расширения логического ядра

Эндрюс расширяет эту логику определениями операторов выбора. для коллекций всех типов, так что

$(5a)$ ℩ $_{\alpha (o\alpha )}[{\text{Q}}_{o\alpha \alpha }y_{i}]=y_{i}\,$

— теорема (номер 5309). Другими словами, все типы имеют определенный оператор описания.Это консервативное расширение , поэтому расширенная система непротиворечива, еслиядро единообразно.

Он также представляет дополнительную аксиому 6 , которая гласит:что существует бесконечно много индивидуумов вместе с эквивалентными альтернативамиаксиомы бесконечности.

В отличие от многих других формулировок теории типов и помощников по доказательству, основанных натеория типов, Q ₀ не предусматривает базовых типов, отличных от o и i ,так, например, конечные кардинальные числа строятся как совокупность отдельных лиц.подчиняющийся обычным постулатам Пеано, а не типу в смысле простоготеория типов.

Вывод в вопросе ₀

Q ₀ имеет единственное правило вывода.

Правило R. Из $С$ и $А α = Б α$ сделать вывод о результате замены одного появление $A α$ в $C$ в результате появления $Б α$ ,при условии, что появление $A α$ в $C$ не (вхождение переменной) непосредственно предшествует $λ$ .

Производное правило вывода R' позволяет рассуждать на основе набора H. гипотез

Правило Р'. Если $ЧАС ⊦ А α знак равно B α$ ,и $H ⊦ C$ , а $D$ получается из $C$ заменив одно вхождение $A α$ вхождениемB $, α$ то $H ⊦ D$ , при условии, что:

Появление $A α$ в $C$ не является появлением переменной, которой непосредственно предшествует $λ$ , и
ни одна переменная не свободна в $A α = B α$ и член $H$ связан в $C$ при замененном вхождении $A α$ .

Примечание. Ограничение на замену $A α$ на $B α$ в $C$ гарантирует, что любая переменнаясвободен как в гипотезе, так и в $A α = B α$ продолжает иметь одно и то же значение в обоих случаях после заменысделано.

Теорема о дедукции для Q ₀ показывает, что доказательства гипотез с использованием правила R′могут быть преобразованы в доказательства без гипотез и с использованием правила R.

В отличие от некоторых подобных систем, вывод в Q ₀ заменяет подвыражение на любой глубине.внутри WFF с равным выражением. Например, данные аксиомы:

1. $\existsx Px$
2. $Px \supset Qx$

и тот факт, что $A \supset B \equiv (A \equiv A \land B)$ , мы можем действовать, не удаляя квантор:

3. $Px \equiv (Px \land Qx)$ для A и B.
4. $\existsx (Px \land Qx)$ правило R, подставляя в строку 1 строку 3.

Примечания

^ Соревнования по системе CADE-22 ATP (CASC-22)

Ссылки

Эндрюс, Питер Б. (2002). Введение в математическую логику и теорию типов: к истине через доказательство (2-е изд.). Дордрехт, Нидерланды: Kluwer Academic Publishers . ISBN 1-4020-0763-9 . См. также [1]
Черч, Алонсо (1940). «Формулировка простой теории типов» (PDF) . Журнал символической логики . 5 (2): 56–58. дои : 10.2307/2266170 . JSTOR 2266170 . S2CID 15889861 . Архивировано из оригинала (PDF) 12 января 2019 г.

Дальнейшее чтение

описание Q ₀Более подробное ; часть статьи о теории типов Чёрча в Стэнфордской энциклопедии философии .
Обзор математической логики (включая различных преемников Q ₀ ): Основы математики. Генеалогия и обзор doi: 10.4444/100.111 .

[1] Соревнования по системе CADE-22 ATP (CASC-22)

[1]

Аксиомы Q 0