И семинар-в-пути с КП, и обсуждение в жж были для меня очень плодотворными - несмотря на то, что я не всегда лучшим образом выдерживал сменяющиеся роли симплицимуса и провокатора
( Read more... )
Мне тут неожиданно пришло в голову, что эта ситуация с метаматематикой действительно интересна и перспективна для сравнения научного и математического подходов
( ... )
Обсудить, разобраться в этом очень хочется. Но вот в Вашем комменте я пока что не понял, в чем разница между теорией доказательства (у ученого) и формальная модель доказательства. Тем, что эта модель строится без намерения ее сопоставлять с реальными доказательствами? А если сопоставить? Мне базовые вещи непонятны. Как вообще появилась идея, что нужно что-то (очевидное, не вызывающее сомнений) доказывать? И что это такое - доказывание? Или выведение? Было бы понятно, если бы идея, скажем, неевклитдовой геометрии появилась после Эйнштейна, когда обнаружилосб, что Евклид "не работает". Так нет же с глубокого далека они вцепились в пятый постулат - сначала пытались его доказывать, а потом решили, что он необязателен...
А как можно сопоставить формальную модель с реальностью? Ведь формальная - значит, всеобщая. То есть любое доказательство должно априори иметь такую форму. Это не знание, а норма. Норму сопоставить нельзя, ей можно только следовать. А если кто-то где-то не следует, то это просто ошибка.
Кстати, нельзя сказать, что модель там (у Геделя) совсем уж формальная. Точнее, она построена на том, что форма и содержание разведены как бы материально. За содержание отвечает система аксиом, а за форму (доказательства) - логическое исчесление. То есть содержание доказательства как бы выведено вовне - в предмет.
Но оказалось, что это не работает. И в модели Генцена уже кое-что (по крайней мере) по взрослому. Трансфинитную индукцию не о отнесёшь ни к аксиомам, ни к логике. Здесь уже нет этого дубового разведения формы и содержания.
== Как вообще появилась идея, что нужно что-то (очевидное, не вызывающее сомнений) доказывать?
Ну это несколько другая тема, или поворот темы. Это, в димо, как раз про игру? :)
Поскольку мы все время так или иначе упираемся в проблему знания, решил проконсультироваться у ГП и набрел на классный текст, который у меня забыл уже откуда. В архиве его нет, нет и в Вашей базе. "Основы современной теории знаний", лекции, читанные во МТИППе (технологическом ин-те пищевой промышленности) в ноябре-декабре 1972 года. Там четыре полноценных текста (правда, без схем), пятая - в виде заготовки ГП и обрубок предположительно шестой. Я подредактировал малость: https://disk.yandex.ru/i/JW-p4m3kx7uokA.
Reply
Но вот в Вашем комменте я пока что не понял, в чем разница между теорией доказательства (у ученого) и формальная модель доказательства. Тем, что эта модель строится без намерения ее сопоставлять с реальными доказательствами? А если сопоставить?
Мне базовые вещи непонятны.
Как вообще появилась идея, что нужно что-то (очевидное, не вызывающее сомнений) доказывать? И что это такое - доказывание? Или выведение?
Было бы понятно, если бы идея, скажем, неевклитдовой геометрии появилась после Эйнштейна, когда обнаружилосб, что Евклид "не работает". Так нет же с глубокого далека они вцепились в пятый постулат - сначала пытались его доказывать, а потом решили, что он необязателен...
Reply
Ведь формальная - значит, всеобщая. То есть любое доказательство должно априори иметь такую форму.
Это не знание, а норма. Норму сопоставить нельзя, ей можно только следовать.
А если кто-то где-то не следует, то это просто ошибка.
Кстати, нельзя сказать, что модель там (у Геделя) совсем уж формальная. Точнее, она построена на том, что форма и содержание разведены как бы материально.
За содержание отвечает система аксиом, а за форму (доказательства) - логическое исчесление.
То есть содержание доказательства как бы выведено вовне - в предмет.
Но оказалось, что это не работает.
И в модели Генцена уже кое-что (по крайней мере) по взрослому.
Трансфинитную индукцию не о отнесёшь ни к аксиомам, ни к логике.
Здесь уже нет этого дубового разведения формы и содержания.
== Как вообще появилась идея, что нужно что-то (очевидное, не вызывающее сомнений) доказывать?
Ну это несколько другая тема, или поворот темы.
Это, в димо, как раз про игру? :)
Reply
"Основы современной теории знаний", лекции, читанные во МТИППе (технологическом ин-те пищевой промышленности) в ноябре-декабре 1972 года. Там четыре полноценных текста (правда, без схем), пятая - в виде заготовки ГП и обрубок предположительно шестой.
Я подредактировал малость: https://disk.yandex.ru/i/JW-p4m3kx7uokA.
Reply
Reply
Leave a comment