Свойства дизъюнкции и существования - Disjunction and existence properties

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

Свойство дизъюнкции

Свойство дизъюнкции удовлетворяется теорией, если всякий раз, когда предложение A ∨ B является теоремой , либо A - теорема, либо B - теорема.

Свойство существования

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

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

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

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

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

Предпосылки и история

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

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

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

В топоях

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

Отношения

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

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

{\ Displaystyle А \ Ви В \ эквив (\ существует п) [(п = 0 \ к А) \ клин (п \ neq 0 \ к В)]}

.

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

{\ displaystyle A \ vee B}

это теорема , так и есть .

{\ displaystyle T}

{\ Displaystyle \ существует п \ двоеточие (п = 0 \ к А) \ клин (п \ neq 0 \ к В)}

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

{\ displaystyle ({\ bar {s}} = 0 \ к A) \ клин ({\ bar {s}} \ neq 0 \ to B)}

это теорема. Так как является числительным, можно конкретно проверить значение : if then - теорема и if then - теорема. ${\ 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). Наконец, исключение дизъюнкции может использоваться, чтобы показать, что один из дизъюнктов доказуем.

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

Ссылки

Питер Дж. Фрейд и Андре Щедров, 1990, Категории, Аллегории . Северная Голландия.
Харви Фридман , 1975, Свойство дизъюнкции подразумевает свойство численного существования , Государственный университет Нью-Йорка в Буффало.
Герхард Генцен , 1934, "Untersuchungen ü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, «Некоторые свойства интуиционистской теории множеств Цермело-Френкеля», в A. Mathias и H. Rogers, Cambridge Summer School in Mathematical Logic , Lectures Notes in Mathematics v. 337, pp. 206–231, Springer.
Майкл Ратиен, 2005, " Дизъюнкция и связанные свойства для конструктивной теории множеств Цермело-Френкеля ", Журнал символической логики , т. 70, с. 4. С. 1233–1254.
Энн С. Трельстра , изд. (1973), Метаматематические исследования интуиционистской арифметики и анализа , Springer.

внешняя ссылка

Интуиционистская логика Джоан Московакис, Стэнфордская энциклопедия философии

Languages

In other projects