Свойства дизъюнкции и существования

В математической логике свойства дизъюнкции и существования являются «отличительными чертами» конструктивных теорий, таких как арифметика Хейтинга и теории конструктивных множеств (Rathjen 2005).

Определения

• , свойству дизъюнкции Теория удовлетворяет если всякий раз, когда предложение A ∨ B является теоремой , то либо A является теоремой, либо B является теоремой.
• Свойство существования или свойство свидетеля удовлетворяется теорией, если всякий раз, когда предложение (∃ x ) A ( x ) является теоремой, где A ( x ) не имеет других свободных переменных, тогда существует некоторый член t такой, что теория доказывает В ) ​ . ​

Связанные объекты

Ратьен (2005) перечисляет пять свойств, которыми может обладать теория. К ним относятся свойство дизъюнкции ( DP ), свойство существования ( EP ) и три дополнительных свойства:

• Свойство численного существования (NEP) гласит, что если теория доказывает $(\exists x\in \mathbb {N} )\varphi (x)$, где φ не имеет других свободных переменных, то теория доказывает $\varphi ({\bar {n}})$ для некоторых $n\in \mathbb {N} {\text{.}}$ Здесь ${\bar {n}}$ это термин в $T$ представляющий число n .
• Правило Чёрча (CR) гласит, что если теория доказывает $(\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)$ тогда существует натуральное число e такое, что, полагая $f_{e}$ — вычислимая функция с индексом e , теория доказывает $(\forall x)\varphi (x,f_{e}(x))$.
• Вариант правила Чёрча, CR ₁ , гласит, что если теория доказывает $(\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)$ тогда существует натуральное число e такое, что теория доказывает $f_{e}$ тотален и доказывает $\psi (f_{e})$.

Эти свойства могут быть непосредственно выражены только для теорий, которые способны давать количественную оценку натуральным числам, а в случае CR ₁ — количественную оценку функций из $\mathbb {N}$ к $\mathbb {N}$. На практике можно сказать, что теория обладает одним из этих свойств, если дефиниционное расширение теории обладает указанным выше свойством (Rathjen 2005).

Результаты

Непримеры и примеры

Почти по определению теория, допускающая исключенное третье при наличии независимых утверждений, не обладает свойством дизъюнкции. Таким образом, все классические теории, выражающие арифметику Робинсона , не имеют ее. Большинство классических теорий, таких как арифметика Пеано и ZFC , в свою очередь, также не подтверждают свойство существования, например, потому, что они подтверждают утверждение о существовании принципа наименьшего числа . Но некоторые классические теории, такие как ZFC плюс аксиома конструктивности , имеют более слабую форму свойства существования (Rathjen 2005).

Арифметика Хейтинга хорошо известна тем, что обладает свойством дизъюнкции и свойством (числового) существования.

Хотя самые ранние результаты касались конструктивных теорий арифметики, многие результаты также известны и для конструктивных теорий множеств (Rathjen 2005). Джон Майхилл (1973) показал, что IZF с устранением аксиомы замены в пользу аксиомы коллекции обладает свойством дизъюнкции, свойством числового существования и свойством существования. Майкл Ратьен (2005) доказал, что CZF обладает свойством дизъюнкции и свойством числового существования.

Фрейд и Скедров (1990) заметили, что свойство дизъюнкции справедливо в свободных алгебрах Гейтинга и свободных топосах . В категориальных терминах , в свободном топосе , это соответствует тому факту, что терминальный объект , $\mathbf {1}$, не является объединением двух собственных подобъектов. Вместе со свойством существования это приводит к утверждению, что $\mathbf {1}$ является неразложимым проективным объектом — функтор, который он представляет (функтор глобального сечения), сохраняет эпиморфизмы и копроизведения .

Связь между свойствами

Между пятью свойствами, обсуждавшимися выше, существует несколько взаимосвязей.

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

$A\vee B\equiv (\exists n)[(n=0\to A)\wedge (n\neq 0\to B)]$.

Следовательно, если

$A\vee B$ представляет собой теорему $T$, так и есть $\exists n\colon (n=0\to A)\wedge (n\neq 0\to B)$.

Таким образом, предполагая свойство численного существования, существует некоторое $s$ такой, что

$({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)$

это теорема. С ${\bar {s}}$ является числом, можно конкретно проверить значение $s$: если $s=0$ затем $A$ является теоремой, и если $s\neq 0$ затем $B$ это теорема.

Харви Фридман (1974) доказал, что в любом рекурсивно перечислимом расширении интуиционистской арифметики свойство дизъюнкции подразумевает свойство числового существования. В доказательстве используются самореферентные предложения, аналогично доказательству теорем Гёделя о неполноте . Ключевым шагом является нахождение границы квантора существования в формуле (∃ x )A( x ), что дает ограниченную формулу существования. (∃ Икс < п )А( Икс ). Тогда ограниченную формулу можно записать в виде конечной дизъюнкции A(1)∨A(2)∨...∨A(n). Наконец, устранение дизъюнкта можно использовать, чтобы показать, что одно из дизъюнктов доказуемо.

История

Курт Гёдель (1932) без доказательства заявил, что интуиционистская логика высказываний (без дополнительных аксиом) обладает свойством дизъюнкции; этот результат был доказан и распространен на интуиционистскую логику предикатов Герхардом Генценом (1934, 1935). Стивен Коул Клини (1945) доказал, что арифметика Гейтинга обладает свойством дизъюнкции и свойством существования. Метод Клини представил технику реализуемости , которая сейчас является одним из основных методов исследования конструктивных теорий (Kohlenbach 2008; Troelstra 1973).

См. также

• Конструктивная теория множеств
• Хейтинговая арифметика
• Закон исключенного третьего
• Реализуемость
• Экзистенциальный квантор

Ссылки

• Питер Дж. Фрейд и Андре Щедров, 1990, Категории, Аллегории . Северная Голландия.
• Харви Фридман , 1975, Свойство дизъюнкции подразумевает свойство числового существования , Государственный университет Нью-Йорка в Буффало.
• Герхард Генцен , 1934, «Исследования по логическим рассуждениям. I», Mathematical Journal v. 39 н. 2, стр. 176–210.
• Герхард Генцен , 1935, «Исследования по логическим рассуждениям. II», Mathematical Journal v. 39 н. 3, стр. 405–431.
• Курт Гёдель , 1932, «Об интуиционистском исчислении высказываний», вестник Академии наук в Вене , т. 69, стр. 65–66.
• Стивен Коул Клини, 1945, «Об интерпретации интуиционистской теории чисел», Журнал символической логики , т. 10, стр. 109–124.
• Ульрих Коленбах , 2008, Прикладная теория доказательств , Springer.
• Джон Майхилл , 1973, «Некоторые свойства интуиционистской теории множеств Цермело-Френкеля», в книге А. Матиаса и Х. Роджерса, Кембриджская летняя школа по математической логике , Конспекты лекций по математике, т. 337, стр. 206–231, Springer.
• Майкл Ратьен, 2005, « Дизъюнкция и связанные с ней свойства конструктивной теории множеств Цермело-Френкеля », Журнал символической логики , т. 70 н. 4, стр. 1233–1254.
• Энн С. Трулстра , изд. (1973), Метаматематическое исследование интуиционистской арифметики и анализа , Спрингер.

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

• Мошовакис, Джоан (16 декабря 2022 г.). «Интуиционистская логика» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .