[Recent Entries][Archive][Friends][User Info]
Below are the 2 most recent journal entries recorded in the "Misha Verbitsky" journal:| June 20th, 2007 | |
|---|---|
| 11:11 pm [Link] |
тезис о формализации математики Неожиданно сообразил: а ведь убежденность в возможности формализации математических доказательств есть примерно то же самое, что тезис Черча, утверждающий, что любой алгоритм (в житейском смысле этого слова) сводится к машинам Тьюринга. Сейчас считается, что это определение алгоритма, в силу очевидной недоказуемости тезиса. Люди пишут на языках высокого уровня, предполагая, что перевести программу на машинные коды или к машине Тьюринга или свести доказательство к формальным языкам при желании всегда можно. Хотя этого никто не проверял, и проверить не может (трансляторы в машинные коды существуют, но доказать их безошибочность - задача такой же сложности, как и проверка формализуемости доказательства). Так вот, тезис о формализации математики имеет ту же самую природу: на практике формализовать (или свести к машине Тьюринга) можно только самые простые вещи, но чтоб сомневаться в сводимости, нужно быть чем-то вроде финитиста. Привет Current Mood: |
| June 9th, 2007 | |
| 06:52 pm [Link] |
убежден в невозможности формальных доказательств Смешное. http://sowa.livejournal.com/92839.html ![[info]](http://lj.rossia.org/img/userinfo-lj.gif) sowa@lj убежден в невозможности формальныхдоказательств, потому что те были бы слишком длинные. Напомнило мне деятельность ультра-финитистов, таких немножко ебнутых персонажей от матлогики, которые не верят в очень большие числа. Известный диссидент Есенин-Вольпин (последователь и отчасти основатель учения) имеет ученый труд, страниц на несколько тысяч, с опровержением теоремы Геделя о неполноте. Дескать утверждение, которое невозможно вывести или опровергнуть, получилось бы слишком длинное, а такие длинные утверждения рассматривать ненаучно. Юмор состоит в том, что труд Есенина-Вольпина гораздо длиннее, чем соответствующая работа Геделя, никем не прочитан (и никогда не будет прочитан), и в силу этого же самого аргумента, гораздо менее научен. sowa@lj полагает, что иллюзию о возможностиформальных доказательств следует оставить, а в качестве критерия научности пользоваться консенсусом. Это конечно замечательная идея, проблема в том, что убежденность в возможности (и отчасти желательности) формализации есть часть этого же самого консенсуса. Поэтому, если исходить из консенсуса как единственного критерия, возможность формализации можно считать доказанной. sowa@lj глуп, и все его комментаторы мудаки,один я такой умный. Ну, еще Валерия Ильинична.  Привет Current Mood: |
sick