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

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

Определения

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

Связанные свойства

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

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

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

Результаты

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

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

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

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

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

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

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

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

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

Поэтому, если

${\displaystyle A\vee B}$является теоремой , так же как и . ${\displaystyle T}$ ${\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}$

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

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

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

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

История

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

Смотрите также

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

Ссылки

• Питер Дж. Фрейд и Андре Сцедров, 1990, Категории, Аллегории . Северная Голландия.
• Харви Фридман , 1975, Свойство дизъюнкции влечет численное свойство существования , Государственный университет Нью-Йорка в Буффало.
• Герхард Генцен , 1934, «Untersuruchungen über das logische Schließen. I», Mathematische Zeitschrift v. 39 n. 2, стр. 176–210.
• Герхард Генцен , 1935, "Untersuchungen über das logische Schließen. II", Mathematische Zeitschrift v. 39 n. 3, стр. 405–431.
• Курт Гёдель , 1932, «Zum intuitionistischen Aussagenkalkül», Anzeiger der Akademie der Wissenschaftischen в Вене , т. 69, стр. 65–66.
• Стивен Коул Клини, 1945, «Об интерпретации интуиционистской теории чисел», Журнал символической логики , т. 10, стр. 109–124.
• Ульрих Коленбах , 2008, Прикладная теория доказательств , Springer.
• Джон Майхилл , 1973, «Некоторые свойства интуиционистской теории множеств Цермело-Френкеля», в книге А. Матиаса и Х. Роджерса, Кембриджская летняя школа по математической логике , заметки о лекциях по математике, т. 337, стр. 206–231, Springer.
• Майкл Ратьен, 2005, «Дизъюнкция и связанные с ней свойства для конструктивной теории множеств Цермело-Френкеля», Журнал символической логики , т. 70, № 4, стр. 1233–1254.
• Энн С. Троелстра , ред. (1973), Метаматематическое исследование интуиционистской арифметики и анализа , Springer.

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

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