Мечта о финитизме I: Гедонизм

Я начну с цитаты из замечательной статьи Лесли Лампорта «How to write a proof»:
«The proofs have been carried out to an excruciating level of detail … The reader may feel that we have given long, tedious proofs of obvious assertions. However, what he has not seen are the many equally obvious assertions that we discovered to be wrong only by trying to write similarly long, tedious proofs.»

Много веков что математические доказательства, что математические построения (как в геометрии: помните, там часто достраивают всякие штуки, чтобы доказательство провести) записывали обычными человеческими словами. В 19ом веке случился кризис, стало понятно, что если доказательства записывать недостаточно строго, возможны очень тонкие ошибки, которые очень тяжело заметить.

( Read more... )

Мечта о финитизме II: Аскетизм

Изначальная идея Гильберта по установлении математики на прочные основания состояла в том, чтобы выделить супернадёжную базовую теорию ("финитизм") и внутри неё доказать непротиворечивость всей остальной математики. (К сожалению, идея с доказательством непротиворечивости сильной системы из средствами более слабой, оказалась несостоятельна, но этот вопрос пока отставим в сторону.)

В прошлом посте я рассказал о том, что системой, позволяющей с комфортом и большой общностью работать с финитарными объектами, является недавно сформулированная OTT (Observable Type Theory). В такой системе вести метаматематические доказательства чрезвычайно удобно, однако на роль камменного фундамента она подходит едва ли: слишком уж большая и сложная теория. Тут нужна аскетичная теория.

В качестве таковой Торальф Сколем разработал ( Read more... )

Каталог постов по основаниям математики

( Read more... )

Каталог постов про образование за последнее время

( Read more... )

(no subject)

Превосходная статья о математике, её особенном отделении в 20ом веке от естественных наук и проблеме с преподаванием: http://www.ams.org/notices/201201/rtx120100031p.pdf

via sorhed