Войти в систему

Home
    - Создать дневник
    - Написать в дневник
       - Подробный режим

LJ.Rossia.org
    - Новости сайта
    - Общие настройки
    - Sitemap
    - Оплата
    - ljr-fif

Редактировать...
    - Настройки
    - Список друзей
    - Дневник
    - Картинки
    - Пароль
    - Вид дневника

Сообщества

Настроить S2

Помощь
    - Забыли пароль?
    - FAQ
    - Тех. поддержка



Пишет Misha Verbitsky ([info]tiphareth)
@ 2007-06-20 23:11:00


Previous Entry  Add to memories!  Tell a Friend!  Next Entry
Настроение: sick
Музыка:Куклы Напрокат - ПОВЕРИЛА
Entry tags:logic, math

тезис о формализации математики
Неожиданно сообразил:
а ведь убежденность в возможности формализации
математических доказательств
есть примерно то же самое,
что тезис Черча, утверждающий, что любой алгоритм (в
житейском смысле этого слова) сводится к
машинам Тьюринга. Сейчас считается, что это
определение алгоритма, в силу очевидной
недоказуемости тезиса. Люди пишут на языках
высокого уровня, предполагая, что перевести программу
на машинные коды или к машине Тьюринга или
свести доказательство к формальным языкам
при желании всегда можно. Хотя этого никто не
проверял, и проверить не может (трансляторы
в машинные коды существуют, но доказать их
безошибочность - задача такой же сложности,
как и проверка формализуемости доказательства).

Так вот, тезис о формализации математики имеет ту
же самую природу: на практике формализовать (или свести
к машине Тьюринга) можно только самые простые вещи,
но чтоб сомневаться в сводимости, нужно быть чем-то
вроде финитиста.


Привет



(Читать комментарии) - (Добавить комментарий)


[info]kaledin
2007-06-21 05:04 (ссылка)
Nu mozhet byt', vopros chisto terminologicheskij. No vazhno, chto est' (2) -- a priori sovershenno ne ochevidno, chto mashina Turing'a, \lambda-calculus i rekursivnye funkcii dayut odno i to zhe. Ehto tipa falsifiable prediction.

(Ответить) (Уровень выше)


(Читать комментарии) -