Cтраница 1
Устранимость их была доказана Гильбертом и Бернайсом [ 1934, стр. Эти доказательства устанавливают устранимость tw как формального оператора, присоединение которого к данному формализму делает возможным введение сразу всех описательных определений. [1]
Теорема об устранимости характеристик доказана в гл. [2]
Предлагаемое ниже доказательство устранимости сечения, конечно, неэлементарно, что и невозможно в силу упомянутого результата Такеути, но все же не использует закона исключенного третьего и протекает в рамках интуиционистской непредикативной теории видов. Можно показать, что доказательство устранимости сечения из выводов ограниченной сложности само формализуется в интуиционистской простой теории типов с аксиомой бесконечности. [3]
Но это доказательство устранимости i-правила распространяется только на такие формализмы, которые получаются из исчисления предикатов с i-правилом путем добавления каких-либо собственных аксиом и, может быть, аксиомы равенства ( J2), в то время как прежняя теорема была доказана с включением аксиомы полной продукции. [4]
В тех случаях, когда устранимость i-правила может быть выведена из второй е-теоремы, конечно, можно иметь дело прямо с е-символом и е-формулой, а не с i-правилом. В качестве примера мы рассмотрим вопрос о замене функциональных знаков предикатными символами. Идущее далее рассуждение имеет менее общий характер, поскольку оно не охватывает полной индукции; но, с другой стороны, нынешний результат, в отличие от прежнего, будет относиться не только к таким формализмам, которые включают в себя аксиомы равенства. [5]
Отметим, что вопрос об устранимости обнаруженного несоответствия в общем случае не может быть решен, так как решение данного вопроса требует знания моделью всех причинно-следственных связей, существующих в предметной области, и умения делать выводы ( умозаключения) любой сложности. Следует иметь в виду, что способы устранения несоответствий являются весьма разнообразными, начиная от вычислении и кончая запросами к пользователю. [6]
Как известно, обычные методы доказательства устранимости сечения ( см., например, [ 14, с. Причиной является непредикативный характер таких логик, в которых вместо параметров формул в определенных случаях разрешается подставлять термы, более сложные, чем сами исходные формулы. Из-за этого основная индукция по логической сложности главной формулы сечения разрушается, и доказательство не проходит. Такеути [15] показал, что это обстоятельство не случайно: доказав устранимость сечения в простой теории типов, можно уже элементарно доказать непротиворечивость простой теории типов с аксиомой бесконечности. Простая теория типов с аксиомой бесконечности - очень обширная теория, естественно формализующая практически всю работающую математику. Таким образом, в силу известной теоремы Геделя само доказательство устранимости сечения не может быть элементарным; более того, оно не может быть даже проведено средствами такой сильной теории, как простая теория типов с аксиомой бесконечности. С точки зрения оснований математики поэтому принципиальный интерес приобретает анализ формы доказательства устранимости сечения в простой теории типов. [7]
Как известно, обычные методы доказательства устранимости сечения, например, типа, приведенного нами в первой части, оказываются непригодными для логик высокого порядка. Причиной является непредикативный характер таких исчислений, в которых вместо параметров формул в определенных случаях разрешается подставлять термы, более сложные, чем сами исходные формулы. Из-за этого основная индукция по логической сложности главной формулы сечения разрушается и доказательство не проходит. Та-кеути [1] показал, что это обстоятельство не случайно: доказав устранимость сечения в простой теории типов, можно уже элементарно доказать непротиворечивость простой теории типов с аксиомой бесконечности. Простая теория типов с аксиомой бесконечности - очень обширная теория, естественно формализующая практически все разделы работающей классической математики. Таким образом, в силу известной теоремы Геделя, само доказательство устранимости сечения не может быть элементарным, - более того, оно не может быть даже проведено средствами такой сильной теории, как простая теория типов с аксиомой бесконечности. Доказательство устранимости сечения представляет поэтому замечательный пример весьма неэлементарного доказательства просто формулируемого синтаксического утверждения, представляющего несомненный интерес. С точки зрения оснований математики принципиальный интерес приобретает анализ формы этого доказательства. [8]
Ясно, что QC-устранимость включает 5ЛС - устранимость. [9]
Точнее, можно показать, что доказательство устранимости сечения из выводов ограниченной сложности само формализуется в интуиционистской простой теории типов с аксиомой бесконечности. Мы проводим доказательство в стиле Жирара-Мартин - Лефа-Правица для обычного исчисления секвенций, а не для натурального вывода или систем типа секвенциальной системы Шютте ( см., например, Освальд [2], Буххольц [1]), метод доказательства распространен на теорию с правилом объемности и, наконец, наше доказательство имеет специальную алгебраическую форму. В действительности строится конкретная модель для рассматриваемого исчисления такая, что из истинности секвенции в этой модели следует ее выводимость без сечений. Логика модели образует алгебру с пополнением, так что модель является примером применения алгебр с пополнением в конкретных исследованиях по теории интуиционистского вывода. [10]
В пятом параграфе мы приводим детальное доказательство устранимости сечения в интуиционистской простой теории типов с правилом объемности ( экстенсиональности), заданной в форме исчисления секвенций. Наше доказательство, хотя и не элементарно, основано на интуиционистской теории видов и, в частности, не использует закона исключенного третьего. Описывается конкретная модель простой теории типов в форме некоторой алгебры с пополнением, такая, что из истинности секвенции в этой модели следует ее выводимость без сечений. [11]
Это геометрическое условие лежит в основе алгебраических условий устранимости высших членов. [12]
Существенным признаком этого вида хрупкости является ее обратимость или устранимость. Развивающаяся хрупкость в процессе медленного охлаждения может быть устранена быстрым охлаждением при повторном отпуске и снова получена новым нагревом с медленным охлаждением. [13]
С точки зрения управления важное значение имеет масштабность, значимость и степень устранимости отклонений. [14]
Такая возможность исключения связанных переменных имеется только у очень специальных систем, в то время как устранимость связанных переменных из вывода любой формулы, не содержащей связанных переменных, согласно нашей е-теореме, имеет место для всякой формализованной средствами исчисления предикатов системы, содержащей только собственные аксиомы без связанных переменных. [15]