![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
fregimus
1
2
3
4
5
6
7
I. Введение
Часто приходится слышать, будто бы некая «теорема Геделя» якобы доказывает, что процессы в сознании вообще и мышление в частности не могут быть алгоритмизированы и смоделированы на вычислительной машине. Многие пускаются в весьма пространные рассуждения, будто бы доказывающие это. Во всех этих рассуждениях непременно обнаруживается логический изъян. Несмотря на обилие таких рассуждений, безупречного доказательства того, что вычислительные формализмы не способны охватить когнитивные процессы, не существует. Не существует, однако, и доказательства обратного — что сознание описуемо формальной системой; к этому мы обратимся в самом конце.
Нам следует разобрать несколько «опровержений» вычислимости сознания и найти в них логические ошибки. Чтобы понять их, однако, вначале нам потребуется разобраться, что же такое теоремы Геделя, о чем говорят эта теоремы, и о том, насколько применим их объект к понятиям о реальном сознании.
Тема эта достаточно обширна, так что нам стоит разбить ее на цикл из нескольких статей, где бы мы могли остановиться на ключевых моментах подробнее. Надеюсь, что этот рассказ будет понятен всем, даже тем, кто далек от математики и когнитивистики. Мы не будем заниматься математикой, мы будем играть в кубики, и еще просто рассуждать. Мы же все умеем это с детства, так что даже ничего нового нам делать не придется. Если по ходу изложения у вас появятся вопросы или сомнения, понимаете ли вы предмет верно, обязательно спрашивайте; буду очень рад ответить возможно подробнее.
II. Библиография
Предмет, о котором мы будем говорить, много лучше и подробнее освещается в книгах; если вы хотите вникнуть в тему глубже, чем позволит короткая статья здесь, лучше обратиться к следующим работам. Вероятно, читать их имеет смысл именно в этом порядке, хотя многое зависит от подготовки и специальных знаний читателя.
1. Хофштадтер Д. Гедель, Эшер, Бах. Самара : Бахрах-М, 2001. Книга эта подобна фуге, где параллельные голоса создают гармонию смыслов. Одна из тем — рассказ о теоремах Геделя и неразрешимости.
2. Подниекс К. М. Вокруг теоремы Геделя. Рига : Зинатне, 1981. Это замечательное математическое введение в теоремы Геделя; там же вы найдете их доказательство, которое мы здесь разбирать не будем. О применимости их к сознанию, однако, в книге не говорится.
3. Franzén T. Gödel's Theorem: An Incomplete Guide to its Use and Abuse. Wellesley, Mass. : AK Peters, 2005 (спасибо![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
alexey_rom за ссылку). Книга написана несколько менее популярно, чем [1], и требует определенных математических знаний, но в ней разбираются и те вопросы, что мы разбираем сейчас.
III. Смертен ли Сократ?
Теоремой или теоремами Геделя обычно называют совокупность утверждений о неполноте арифметик, начало которым было положено Куртом Геделем в работе, опубликованной в 1931 г., а затем значительно усиленных другими математиками; в частности, более сильное утверждение, которое чаще всего сегодня и называют теоремой Геделя (в единственном числе) доказано Баркли Россером, учеником Алонцо Черча, в 1936 г.
Чтобы понять теорему Геделя, сначала следует разобраться в предмете, котором она говорит, а говорит она о формальных системах (ФС). ФС, как следует из их названия, имеют дело с формой. Понятие формы, отдельно рассматриваемой от сущности предмета, восходит к философии Аристотеля; он же и изобрел формализмы — силлогизмы:
Каждый человек смертен.
Сократ — человек.
Следовательно, Сократ смертен.
Силлогизм задает правила для операции над верными утверждениями для получения верных же утверждений. Правило построения силлогизма — формальное, лишенное содержания, в которое можно подставить любые, внешние по отношению к силлогизму утверждения:
Все P есть Q.
R есть P.
Следовательно, R есть Q.
Мотив разделения формы и смысла будет центральным в нашем повествовании. Обратите внимание еще раз: сам по себе формальный силлогизм никакого смысла не имеет: вывод «следовательно, R есть Q» совершенно бессмыслен, покуда R и Q не заменены на определенные высказывания. В то же время, смысл возникает при интерпретации формализма, но не в самом формализме. Мы, снаружи формализма, придаем высказываниям смысл. Мы говорим, что все люди смертны, и что Сократ есть человек. После этого мы берем Аристотелев формализм — как инструмент — и подставляем в него эти утверждения, и получаем вывод: Сократ смертен. Где возникает этот вывод? Следите сейчас очень внимательно: этот вывод не возникает в формализме, он возникает лишь при интерпретации результата исполнения формальной процедуры! Формализм лишь выдает предложение, строчку текста: «Сократ смертен». Однако, сами по себе понятия «Сократ» и «быть смертным» существуют лишь вне формализма, в сознании интерпретирующего.
Чтобы понять это, давайте проведем один очень опасный мысленный эксперимент: запустим вычислительную программу составления силлогизмов, и попытаемся получить с ее помощью пример Аристотеля.
Введите P: человек
Введите Q: смертен
Введите R: Сократ
В этот момент программа ненадолго зависает. Тут неожиданно мы с вами и со всем человечеством гибнем оттого, что на Землю приземляется корабль ужасно радиоактивных пришельцев. Огорченные пришельцы подходят к компьютеру, который как раз выдает последнюю строчку результата:
Сократ смертен
Радиоактивные пришельцы на самом деле обладают одним бессмертным «я» на всех, как Борг из «Звездного пути», но называют себя, по случайному совпадению, не Боргом, а Сократом. Верное на наш взгляд утверждение оказывается для них прямо ложным. Выходит, истинность утверждения зависит от этого самого взгляда. Формализм генератора верных утверждений из верных посылок сработал, но верного по смыслу утверждения не выдал — потому, что нет того, кто бы интерпретировал посылки и утверждение как истинное. Со сменой точки зрения и предпосылка «Сократ есть человек», и вывод «Сократ смертен» превращаются из истинных в ложные.
На этом закончим наш опасный мысленный эксперимент и оживем, но запомним, что смысла формальные системы не содержат и не производят, а затем немного поиграем в кубики.
IV. Кубики для взрослых
Построим простую ФС, которую будем называть «система ХИХИ»1. Возьмем неограниченный запас кубиков или табличек с буквами Х, А, И. Хоть общее число кубиков неограниченно, но на них встречаются только три этих буквы. Множество { Х, А, И } называется лексическим множеством или алфавитом ФС. Алфавит системы должен быть, по правилам игры в кубики, конечным множеством.
Из кубиков можно составить строки ФС. Например, из наших кубиков можно сложить строки ХИХИХИ, ИАИА, ХХХХХХ и АХ. Эти строки будут лексически верными. Строка АГА, в то же время, не является лексически верной, потому что Г не входит в алфавит системы ХИХИ.
Кроме того, строки ФС должны быть синтаксически верными. Далее для краткости будем говорить просто верные строки, имея в виду, что они и синтаксически, и, как из того естественно следует, лексически верные. Верные строки определяются двумя способами, которые обычно используются вместе.
Во первых, зададим начальное подмножество верных строк извне, по нашему произволу 2. Для нашей игры в кубики скажем, что строка ХИ верна3.
Во-вторых, введем несколько правил замены строк. Эти правила строго формальны — их легко исполнять не задумываясь, а задачу запрограммировать их на компьютере решит любой школьник на «пять». Важно помнить, что эти правила верны только для верных строк: из верной строки получается верная. К неверным, синтаксически или, еще страшнее того, лексически недопустимым строкам эти правила применять запрещается. Набор правил всегда конечный: «правила, порождающие правила» не разрешаются. Для нашей системы введем следующие правила4:
1. К любой строке, заканчивающейся на И, можно дописать в конец А. Пример: ХИХИ → ХИХИА.
2. Подстроку, следующую за Х {доб. до конца всей строки}, можно удвоить: ХИ → ХИИ, ХАХИ → ХАХИАХИ, ХАХИ → ХАХИИ.
3. Три И подряд можно заменить на А: ХИИИИ → ХИА, ХИИИИ → ХАИ.
4. Две А подряд можно выбросить: ИААХ → ИХ, ИАААИ → ИАИ.
Начиная с заданных верных строк и применяя правила вновь и вновь к каждому очередному результату, будем получать все больше и больше верных строк, например,
ХИ → ХИИ (правило 2),
ХИИ → ХИИИИ (опять 2),
ХИИИИ → ХАИ (3),
ХАИ → ХАИА (1),
и так далее. Все строки справа от стрелки получены применением формальных правил из верных строк, и, стало быть, верны по определению. Вы уже заметили, что в выборе правил есть произвол. К примеру, к строке ХАХИИИАААИИИ можно применить любое из четырех правил, причем все, кроме первого, еще и более чем одним способом. В этом нет ничего запрещенного, поскольку обычно нас интересует вопрос, является ли некая данная строка верной, то есть можно ли ее получить из других верных строк ФС, применяя любые из правил любым возможным способом.
Имеется счетное множество5 всех строк, которые порождаются ФС. Доказательство того, что это множество счетно, я опускаю, но запомним, что все верные строки, порождаемые ФС, можно пронумеровать натуральными числами. Этот результат нам будет важен.
Здесь нам следует еще раз вспомнить о том, что никакого смысла в верных строках ФС нет. ФС может служить инструментом для переработки смыслов, вкладываемых в строки извне системы, но она ни содержит, ни производит смысла. Слова, сложенные из кубиков, не имеют никакого особого значения: это только слова, сложенные из кубиков.
Перед тем, как мы перейдем к следующей части, попробуйте продолжить нашу игру в кубики. Требуется определить, является ли ХА верной строкой в системе ХИХИ. Либо в ее произведете по правилам 1—4 из других заведомо верных строк (в нашем случае из заведомо верной строки ХИ), либо докажете, что этого сделать невозможно. Решение — или, не огорчайтесь, даже попытка решения этой задачи сразу даст вам почувствовать, какие сложности возникают даже в таких простых ФС, как наша система ХИХИ.
1 2 3 4 5 6 7
__________________________________
⇧ 1. Hofstadter 1999, p. 33.
⇧ 2. Это множество может быть конечным или даже бесконечным. Бесконечное множество может получаться из правила, например, в некоей системе, где Ы входит в алфавит, строки любой длины из Ы могут быть объявлены верными. Такие правила называются схемами.
⇧ 3. Не удивляйтесь, что мы обойдемся без обычных в описании ФС терминов «аксиома» и «теорема», которые скорее внесли бы в это популярное изложение путаницу, нежели ясность, отсылая читателя к омонимичным, но иным понятиям школьной математики.
⇧ 4. Те, кто интересуется формальными грамматиками, должны заметить, что правила представляют собой контекстно-зависимую грамматику. Не любая ФС обладает контекстно-свободной грамматикой (КСГ), потому что вычислительная мощность ФС та же, что и у машины Тьюринга и, следовательно, неизбежно превышает таковую стековой машины, выражающей КСГ.
⇧ 5. Счетное множество возможно бесконечно, но его элементы можно перенумеровать натуральными числами — разумеется, применяя определенное правило. К примеру, множество целых чисел счетно, а нумеровать их можно так: у числа 0 будет номер 1, у 1 номер 2, у −1 номер 3, у 2 номер 4, и так далее: у положительных четные номера, у соответствующих отрицательных нечетные на единицу больше.
Кантор доказал, что множество рациональных дробей, то есть чисел вида p/q, где p и q натуральные числа, тоже счетно, придумав элегантный способ пронумеровать их. Этот способ называется «диагональным аргументом». Попробуйте и вы придумать такой способ. Счетность множества верных строк тоже доказывается диагональным аргументом.
I. Введение
Часто приходится слышать, будто бы некая «теорема Геделя» якобы доказывает, что процессы в сознании вообще и мышление в частности не могут быть алгоритмизированы и смоделированы на вычислительной машине. Многие пускаются в весьма пространные рассуждения, будто бы доказывающие это. Во всех этих рассуждениях непременно обнаруживается логический изъян. Несмотря на обилие таких рассуждений, безупречного доказательства того, что вычислительные формализмы не способны охватить когнитивные процессы, не существует. Не существует, однако, и доказательства обратного — что сознание описуемо формальной системой; к этому мы обратимся в самом конце.
Нам следует разобрать несколько «опровержений» вычислимости сознания и найти в них логические ошибки. Чтобы понять их, однако, вначале нам потребуется разобраться, что же такое теоремы Геделя, о чем говорят эта теоремы, и о том, насколько применим их объект к понятиям о реальном сознании.
Тема эта достаточно обширна, так что нам стоит разбить ее на цикл из нескольких статей, где бы мы могли остановиться на ключевых моментах подробнее. Надеюсь, что этот рассказ будет понятен всем, даже тем, кто далек от математики и когнитивистики. Мы не будем заниматься математикой, мы будем играть в кубики, и еще просто рассуждать. Мы же все умеем это с детства, так что даже ничего нового нам делать не придется. Если по ходу изложения у вас появятся вопросы или сомнения, понимаете ли вы предмет верно, обязательно спрашивайте; буду очень рад ответить возможно подробнее.
II. Библиография
Предмет, о котором мы будем говорить, много лучше и подробнее освещается в книгах; если вы хотите вникнуть в тему глубже, чем позволит короткая статья здесь, лучше обратиться к следующим работам. Вероятно, читать их имеет смысл именно в этом порядке, хотя многое зависит от подготовки и специальных знаний читателя.
1. Хофштадтер Д. Гедель, Эшер, Бах. Самара : Бахрах-М, 2001. Книга эта подобна фуге, где параллельные голоса создают гармонию смыслов. Одна из тем — рассказ о теоремах Геделя и неразрешимости.
2. Подниекс К. М. Вокруг теоремы Геделя. Рига : Зинатне, 1981. Это замечательное математическое введение в теоремы Геделя; там же вы найдете их доказательство, которое мы здесь разбирать не будем. О применимости их к сознанию, однако, в книге не говорится.
3. Franzén T. Gödel's Theorem: An Incomplete Guide to its Use and Abuse. Wellesley, Mass. : AK Peters, 2005 (спасибо
alexey_rom за ссылку). Книга написана несколько менее популярно, чем [1], и требует определенных математических знаний, но в ней разбираются и те вопросы, что мы разбираем сейчас.III. Смертен ли Сократ?
Теоремой или теоремами Геделя обычно называют совокупность утверждений о неполноте арифметик, начало которым было положено Куртом Геделем в работе, опубликованной в 1931 г., а затем значительно усиленных другими математиками; в частности, более сильное утверждение, которое чаще всего сегодня и называют теоремой Геделя (в единственном числе) доказано Баркли Россером, учеником Алонцо Черча, в 1936 г.
Чтобы понять теорему Геделя, сначала следует разобраться в предмете, котором она говорит, а говорит она о формальных системах (ФС). ФС, как следует из их названия, имеют дело с формой. Понятие формы, отдельно рассматриваемой от сущности предмета, восходит к философии Аристотеля; он же и изобрел формализмы — силлогизмы:
Каждый человек смертен.
Сократ — человек.
Следовательно, Сократ смертен.
Силлогизм задает правила для операции над верными утверждениями для получения верных же утверждений. Правило построения силлогизма — формальное, лишенное содержания, в которое можно подставить любые, внешние по отношению к силлогизму утверждения:
Все P есть Q.
R есть P.
Следовательно, R есть Q.
Мотив разделения формы и смысла будет центральным в нашем повествовании. Обратите внимание еще раз: сам по себе формальный силлогизм никакого смысла не имеет: вывод «следовательно, R есть Q» совершенно бессмыслен, покуда R и Q не заменены на определенные высказывания. В то же время, смысл возникает при интерпретации формализма, но не в самом формализме. Мы, снаружи формализма, придаем высказываниям смысл. Мы говорим, что все люди смертны, и что Сократ есть человек. После этого мы берем Аристотелев формализм — как инструмент — и подставляем в него эти утверждения, и получаем вывод: Сократ смертен. Где возникает этот вывод? Следите сейчас очень внимательно: этот вывод не возникает в формализме, он возникает лишь при интерпретации результата исполнения формальной процедуры! Формализм лишь выдает предложение, строчку текста: «Сократ смертен». Однако, сами по себе понятия «Сократ» и «быть смертным» существуют лишь вне формализма, в сознании интерпретирующего.
Чтобы понять это, давайте проведем один очень опасный мысленный эксперимент: запустим вычислительную программу составления силлогизмов, и попытаемся получить с ее помощью пример Аристотеля.
Введите P: человек
Введите Q: смертен
Введите R: Сократ
В этот момент программа ненадолго зависает. Тут неожиданно мы с вами и со всем человечеством гибнем оттого, что на Землю приземляется корабль ужасно радиоактивных пришельцев. Огорченные пришельцы подходят к компьютеру, который как раз выдает последнюю строчку результата:
Сократ смертен
Радиоактивные пришельцы на самом деле обладают одним бессмертным «я» на всех, как Борг из «Звездного пути», но называют себя, по случайному совпадению, не Боргом, а Сократом. Верное на наш взгляд утверждение оказывается для них прямо ложным. Выходит, истинность утверждения зависит от этого самого взгляда. Формализм генератора верных утверждений из верных посылок сработал, но верного по смыслу утверждения не выдал — потому, что нет того, кто бы интерпретировал посылки и утверждение как истинное. Со сменой точки зрения и предпосылка «Сократ есть человек», и вывод «Сократ смертен» превращаются из истинных в ложные.
На этом закончим наш опасный мысленный эксперимент и оживем, но запомним, что смысла формальные системы не содержат и не производят, а затем немного поиграем в кубики.
IV. Кубики для взрослых
Построим простую ФС, которую будем называть «система ХИХИ»1. Возьмем неограниченный запас кубиков или табличек с буквами Х, А, И. Хоть общее число кубиков неограниченно, но на них встречаются только три этих буквы. Множество { Х, А, И } называется лексическим множеством или алфавитом ФС. Алфавит системы должен быть, по правилам игры в кубики, конечным множеством.
Из кубиков можно составить строки ФС. Например, из наших кубиков можно сложить строки ХИХИХИ, ИАИА, ХХХХХХ и АХ. Эти строки будут лексически верными. Строка АГА, в то же время, не является лексически верной, потому что Г не входит в алфавит системы ХИХИ.
Кроме того, строки ФС должны быть синтаксически верными. Далее для краткости будем говорить просто верные строки, имея в виду, что они и синтаксически, и, как из того естественно следует, лексически верные. Верные строки определяются двумя способами, которые обычно используются вместе.
Во первых, зададим начальное подмножество верных строк извне, по нашему произволу 2. Для нашей игры в кубики скажем, что строка ХИ верна3.
Во-вторых, введем несколько правил замены строк. Эти правила строго формальны — их легко исполнять не задумываясь, а задачу запрограммировать их на компьютере решит любой школьник на «пять». Важно помнить, что эти правила верны только для верных строк: из верной строки получается верная. К неверным, синтаксически или, еще страшнее того, лексически недопустимым строкам эти правила применять запрещается. Набор правил всегда конечный: «правила, порождающие правила» не разрешаются. Для нашей системы введем следующие правила4:
1. К любой строке, заканчивающейся на И, можно дописать в конец А. Пример: ХИХИ → ХИХИА.
2. Подстроку, следующую за Х {доб. до конца всей строки}, можно удвоить: ХИ → ХИИ, ХАХИ → ХАХИАХИ, ХАХИ → ХАХИИ.
3. Три И подряд можно заменить на А: ХИИИИ → ХИА, ХИИИИ → ХАИ.
4. Две А подряд можно выбросить: ИААХ → ИХ, ИАААИ → ИАИ.
Начиная с заданных верных строк и применяя правила вновь и вновь к каждому очередному результату, будем получать все больше и больше верных строк, например,
ХИ → ХИИ (правило 2),
ХИИ → ХИИИИ (опять 2),
ХИИИИ → ХАИ (3),
ХАИ → ХАИА (1),
и так далее. Все строки справа от стрелки получены применением формальных правил из верных строк, и, стало быть, верны по определению. Вы уже заметили, что в выборе правил есть произвол. К примеру, к строке ХАХИИИАААИИИ можно применить любое из четырех правил, причем все, кроме первого, еще и более чем одним способом. В этом нет ничего запрещенного, поскольку обычно нас интересует вопрос, является ли некая данная строка верной, то есть можно ли ее получить из других верных строк ФС, применяя любые из правил любым возможным способом.
Имеется счетное множество5 всех строк, которые порождаются ФС. Доказательство того, что это множество счетно, я опускаю, но запомним, что все верные строки, порождаемые ФС, можно пронумеровать натуральными числами. Этот результат нам будет важен.
Здесь нам следует еще раз вспомнить о том, что никакого смысла в верных строках ФС нет. ФС может служить инструментом для переработки смыслов, вкладываемых в строки извне системы, но она ни содержит, ни производит смысла. Слова, сложенные из кубиков, не имеют никакого особого значения: это только слова, сложенные из кубиков.
Перед тем, как мы перейдем к следующей части, попробуйте продолжить нашу игру в кубики. Требуется определить, является ли ХА верной строкой в системе ХИХИ. Либо в ее произведете по правилам 1—4 из других заведомо верных строк (в нашем случае из заведомо верной строки ХИ), либо докажете, что этого сделать невозможно. Решение — или, не огорчайтесь, даже попытка решения этой задачи сразу даст вам почувствовать, какие сложности возникают даже в таких простых ФС, как наша система ХИХИ.
1 2 3 4 5 6 7
__________________________________
⇧ 1. Hofstadter 1999, p. 33.
⇧ 2. Это множество может быть конечным или даже бесконечным. Бесконечное множество может получаться из правила, например, в некоей системе, где Ы входит в алфавит, строки любой длины из Ы могут быть объявлены верными. Такие правила называются схемами.
⇧ 3. Не удивляйтесь, что мы обойдемся без обычных в описании ФС терминов «аксиома» и «теорема», которые скорее внесли бы в это популярное изложение путаницу, нежели ясность, отсылая читателя к омонимичным, но иным понятиям школьной математики.
⇧ 4. Те, кто интересуется формальными грамматиками, должны заметить, что правила представляют собой контекстно-зависимую грамматику. Не любая ФС обладает контекстно-свободной грамматикой (КСГ), потому что вычислительная мощность ФС та же, что и у машины Тьюринга и, следовательно, неизбежно превышает таковую стековой машины, выражающей КСГ.
⇧ 5. Счетное множество возможно бесконечно, но его элементы можно перенумеровать натуральными числами — разумеется, применяя определенное правило. К примеру, множество целых чисел счетно, а нумеровать их можно так: у числа 0 будет номер 1, у 1 номер 2, у −1 номер 3, у 2 номер 4, и так далее: у положительных четные номера, у соответствующих отрицательных нечетные на единицу больше.
Кантор доказал, что множество рациональных дробей, то есть чисел вида p/q, где p и q натуральные числа, тоже счетно, придумав элегантный способ пронумеровать их. Этот способ называется «диагональным аргументом». Попробуйте и вы придумать такой способ. Счетность множества верных строк тоже доказывается диагональным аргументом.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
Re: возражение не понял
2009-12-18 17:47 (UTC)Я такие утверждения (и обратные к ним) "истинными" не называю - а чтобы они были истинными, их надо постулировать - т.е. превратить в аксиому (вернее, одно из них). Это и есть _дополнение_ системы новой аксиомой.
Соответственно, фишка в том, что если дополнить несамоссылающуюся ФС аксиомой со ссылкой на себя, она станет противоречивой.
Re: возражение не понял
2009-12-18 17:56 (UTC)одно из них -- нельзя, нужно "правильное". иначе получится, что аксиома "не истинна" во "внешнем мире". ну, или переделать "внешний мир".
> Соответственно, фишка в том, что если дополнить несамоссылающуюся
> ФС аксиомой со ссылкой на себя, она станет противоречивой.
нет, Юрик, она не станет противоречивой. с чего бы? но она останется неполной -- в ней опять найдется свое гёделевское утверждение.
Re: возражение не понял
2009-12-18 18:02 (UTC)Нет, не получится. Дело в том, что правила вывода следуют способам доказательства во внешнем мире. Поэтому если это утверждение не является аксиомой во внешнем мире, т.е. доказуема - значит, она выводима и в системе. Вот, как пример - геометрия Лобачевского. Пятый постулат Евклида можно так постулировать, а можно сяк. В природе, как ты знаешь, встречается и то, и то :)
"нет, Юрик, она не станет противоречивой. с чего бы? но она останется неполной -- в ней опять найдется свое гёделевское утверждение."
Как же не станет, когда станет? Мы выведем то же самое доказательство, только внутри системы (помни, что правила вывода в системе соответствуют способам доказательства во "внешнем мире").
Re: возражение не понял
2009-12-18 19:53 (UTC)> правила вывода следуют способам доказательства во внешнем мире.
да.
> это утверждение не является аксиомой во внешнем мире
да.
> значит, она выводима и в системе.
нет. в этом-то вся и суть.
> Пятый постулат Евклида можно так постулировать, а можно сяк. В
> природе, как ты знаешь, встречается и то, и то :)
Да. Но если ты в ФС брать за аксиому ложное с т.з. "внешнего мира" утверждение, получится фигня. Чтобы получилась не фигня, тебе придется что-то сделать с "внешним миром", чтобы аксиоме соответствовала истина, или поменять правила интерпретации высказываний ФС. В контексте нашего разговора я не знаю, возможно ли это сделать.
> Как же не станет, когда станет? Мы выведем то же самое
> доказательство, только внутри системы
Не понял. У меня есть невыводимое утверждение. Если я делаю из него аксиому, с какой радости новая ФС станет противоречивой, если она не была таковой?
Re: возражение не понял
2009-12-18 20:06 (UTC)Как мы во "внешнем мире" узнаём, что оно ложное?
"Не понял. У меня есть невыводимое утверждение. Если я делаю из него аксиому, с какой радости новая ФС станет противоречивой, если она не была таковой?"
Представь, что из данного утверждения выводится его отрицание. Тогда это утверждение не должно быть аксиомой, иначе из него можно будет вывести его отрицание, а значит, и вообще любое утверждение в ФС. И вся наша красота летит ко всем чертям.
Re: возражение не понял
2009-12-18 20:34 (UTC)подумал. кажется, тут все немножко сложнее, чем мне представлялось, сейчас не могу сразу сформулировать. но не суть.
> Представь, что из данного утверждения выводится его отрицание.
это как? оно независимо от аксиом, следовательно, оно должно быть эквивалентно своему отрицанию? такого не бывает, у нас работает закон исключенного третьего.
----
слушай, а тебе не кажется, что мы здесь можем задолбать хозяев? может, пошли в почту?
Re: возражение не понял
2009-12-18 20:45 (UTC)Ау,
">> Представь, что из данного утверждения выводится его отрицание.
> это как? оно независимо от аксиом, следовательно, оно должно быть эквивалентно своему отрицанию? такого не бывает, у нас работает закон исключенного третьего."
Закон исключенного третьего работает только для выводимых утверждений. А для невыводимых - не работает. Если угодно, у нас вообще никаких "всеобщих законов" нету - есть начальные точки (aka "аксиомы") и правила вывода. И всё.
Тут не надо путать "аксиомы" и аксиомы. "Аксиомы" внутри ФС имеют лишь формальный смысл, как стартовые точки. Например, для в ХИХИ "аксиома" - это ХИ. И всё.
Re: возражение не понял
2009-12-19 01:25 (UTC)Напротив, мне было бы интересно, если бы вы продолжили здесь.
Re: возражение не понял
2009-12-18 21:45 (UTC)Re: возражение не понял
2009-12-19 01:23 (UTC)Re: возражение не понял
2009-12-19 04:27 (UTC)Моя идея состоит в том, что гёделево утверждение G - того же самого сорта, только немного завуалированное, чтобы этого не было заметно. А может быть, и вообще то же самое.
***
Ещё вот как придумал сформулировать. Приём "приведение к противоречию" (или "от противного") неявно исходит из того, что предположение, которое мы в нём делаем, либо истинно, либо ложно (это закон исключённого третьего, как ты верно заметил). Однако самоссылающиеся утверждения не подчиняются этому закону (Парадокс Лжеца, приведённый выше). А утверждение G - именно такое. Поэтому при доказательстве его истинности нельзя использовать приём "от противного".
Я ПОНЯЛ ГЛАВНУЮ ФИШКУ
2009-12-20 13:02 (UTC)Главная фишка состоит в том, что нельзя говорить, будто G истинна. Т.е. её нельзя добавить в ФС в качестве аксиомы. Ну в самом деле, как только мы добавим её в ФС в качестве аксиомы, она немедленно станет выводима - из себя же, как аксиомы :)
Т.е. G, конечно, валидна и невыводима. Как и ~G. Но она не истинна и не ложна!
Re: Я ПОНЯЛ ГЛАВНУЮ ФИШКУ
2009-12-20 14:09 (UTC)но фишку ты не понял. само-собой, мы не можем говорить о том, что G истинна или ложна, пока мы внутри ФС -- просто понятий таких там нет. В качестве аксиомы ее добавить можно. При этом мы получим уже некую другую ФС, в которой G будет тривиально выводима. Но ~G не будет выводима, и, будучи проинтерпретирована (вышли из системы!) окажется люжной, в то время как G окажется истинной (мы интерпретируем высказывания таким образом, что все выводимые утверждения -- теоремы -- становятся истинами, а их отрицания -- ложью)
Re:Re: Я ПОНЯЛ ГЛАВНУЮ ФИШКУ
2009-12-20 15:20 (UTC)Re: Я ПОНЯЛ ГЛАВНУЮ ФИШКУ
2009-12-21 09:16 (UTC)Не понял.
> К сожалению, проверка внутренней непротиворечивости (лучше "поиск противоречия" - так может быть быстрее получен результат)
> - задача совсем нетривиальная.
более того, внутри ФС (далее под ФС мы понимаем формализацию арифметики) она не решаема -- непротиворечивость можно доказать только если ФС противоречива.
> Иначе можно было бы относительно просто построить ФС на теориях физиков/биологов/астрономов и иже с ними
это уже философия, я ее тоже не понимаю :)
Re: Я ПОНЯЛ ГЛАВНУЮ ФИШКУ
2009-12-21 04:44 (UTC)Три раза согласен, по каждому пункту.
"Но ~G не будет выводима."
А тут не согласен.
Когда мы заводим себе аксиомы, мы ничего не можем утверждать о выводимости их отрицаний. Например, мы можем завести аксиомы "дважды два равно четыре" и "дважды два равно пять", а потом доказать, что система противоречива, поскольку из одной аксиомы выводится отрицание другой. Это я к тому, что самого того факта, что G - это аксиома, ещё недостаточно для того, чтобы утверждать, что ~G не выводима.
А вообще, ты же ведь читаешь
Re: Я ПОНЯЛ ГЛАВНУЮ ФИШКУ
2009-12-21 09:07 (UTC)Конечно. Если система противоречива, то выводимо вообще все. Но мы считаем, что система непротиворечива, а в этом случае -- тебе же в ru_math уже показали -- ~G не выводима.
Re: Я ПОНЯЛ ГЛАВНУЮ ФИШКУ
2009-12-21 13:43 (UTC)На каком основании? Заметь, у нас тут есть _две_ системы. Старая, без дополнительных аксиом, и новая, с одной дополнительной аксиомой. Про старую известно, что она непротиворечива. Но про новую непротиворечивость надо доказывать заново.
Re: Я ПОНЯЛ ГЛАВНУЮ ФИШКУ
2009-12-22 07:39 (UTC)Re: возражение не понял
2009-12-21 10:20 (UTC)> Как мы во "внешнем мире" узнаём, что оно ложное?
Ты знаешь, как изменится "мир", если мы возьмем ~G в качестве аксиомы? Если я правильно понимаю, у нас появятся бесконечные ординалы.
Re: возражение не понял
2009-12-21 15:15 (UTC)