В конструктивной математике , тезис Чёрча ( КТ ) является аксиомой о том , что все общие функции вычислимой . Аксиома берет свое название от тезиса Черча – Тьюринга , [ цитата необходима ], который утверждает, что каждая эффективно вычислимая функция является вычислимой функцией , но конструктивистская версия намного сильнее, утверждая, что каждая функция вычислима.
Аксиома CT несовместима с классической логикой в достаточно сильных системах. Например, арифметика Гейтинга (HA) с CT в качестве аксиомы сложения способна опровергнуть некоторые примеры закона исключенного третьего . Однако гейтингова арифметика equiconsistent с арифметикой Пеано (ПА), а также с арифметикой Гейтинга плюс церковь диссертации. То есть добавление закона исключенного третьего или тезиса Чёрча не делает арифметику Гейтинга противоречивой, а добавление обоих делает.
Официальное заявление
В теориях первого порядка, таких как HA, которые не могут дать количественную оценку функций напрямую, CT формулируется как схема аксиом, говорящая, что любая определяемая функция вычислима, с использованием предиката T Клини для определения вычислимости. Для каждой формулы φ ( x , y ) двух переменных схема включает аксиому
Эта аксиома утверждает, что если для каждого x существует y, удовлетворяющий φ, то на самом деле существует e, которое является числом Гёделя общей рекурсивной функции, которая для каждого x будет производить такое y, удовлетворяющее формуле, с некоторым u число Гёделя, кодирующее проверяемое вычисление , свидетельствующее о том, что y на самом деле является значением этой функции в x .
В системах более высокого порядка, которые могут определять количество функций напрямую, CT можно сформулировать как единую аксиому, утверждающую, что каждая функция от натуральных чисел до натуральных чисел вычислима.
Отношение к классической логике
Показанная выше схематическая форма CT при добавлении к конструктивным системам, таким как HA, подразумевает отрицание закона исключенного третьего. Например, классическая тавтология гласит, что каждая машина Тьюринга либо останавливается, либо не останавливается на заданном входе. Предполагая эту тавтологию, в достаточно сильных системах, таких как HA, можно сформировать функцию h, которая принимает код для машины Тьюринга и возвращает 1, если машина останавливается, и 0, если она не останавливается. Тогда из тезиса Чёрча можно было бы заключить, что эта функция вычислима, но это, как известно, неверно, потому что проблема остановки вычислимо не разрешима. Таким образом, HA и CT опровергают некоторые следствия закона исключенного третьего.
Упомянутая выше форма "единой аксиомы" СТ,
определяет количество функций и говорит, что каждая функция f вычислима (с индексом e ). Эта аксиома согласуется с некоторыми слабыми классическими системами, которые не имеют силы формировать функции, такие как функция f из предыдущего абзаца. Например, слабая классическая система согласуется с этой единственной аксиомой, потому что имеет модель, в которой каждая функция вычислима. Однако форма с единственной аксиомой становится несовместимой с законом исключенного третьего в любой системе, которая имеет достаточно аксиом для построения таких функций, как функция h из предыдущего абзаца.
Расширенная диссертация Черча
Расширенный тезис Чёрча (ECT) расширяет притязания на функции, которые полностью определены в определенном типе области. Его использует школа конструктивной математики, основанная Андреем Марковым-младшим . Формально это можно выразить схемой:
В приведенном выше описании ограничен быть почти отрицательным . Для арифметики первого порядка (где обозначена схема), это означает не может содержать дизъюнкции , а кванторы существования могут появляться только перед (разрешимые) формулы.
Этот тезис можно охарактеризовать как утверждение, что предложение истинно тогда и только тогда, когда оно вычислимо реализуемо . Фактически это фиксируется следующими метатеоретическими эквивалентностями: [1]
Здесь, означает "". Итак, это доказуемо в с участием что предложение истинно, если оно реализуемо. Но также, доказуемо верно в с участием если только доказуемо осуществимо в без .
Вторая эквивалентность может быть расширена с помощью принципа Маркова (M) следующим образом:
Так, доказуемо верно в с участием а также если существует число n, которое доказуемо реализует в . Квантор существования должен быть снаружи.в данном случае, потому что PA неконструктивен и не обладает свойством существования .
Рекомендации
- ^ Troelstra, AS Метаматематическое исследование интуиционистской арифметики и анализа . Том 344 конспектов лекций по математике; Спрингер, 1973 г.
- Эллиотт Мендельсон (1990) «Размышления о тезисе Черча и математических доказательствах», Journal of Philosophy 87 (5): 225–233.