(Оффтоп)
[off]
Есть те, кто в этом сомневается.
Синтаксически разложить до аксиом ключевую теорему из публикации филдсовского лауреата? Легко! Например, в прошлом году удалось формализовать на Lean весьма нетривиальное утверждение из лекций Шольце. Об этом писал сам Шольце в посте "Half a year of the Liquid Tensor Experiment: Amazing developments". Пост доступен по
ссылке.Не вполне понял коннотацию.
В том, что подавляющее большинство "верят, что все нужные рассуждения можно полностью формализовать, и чисто синтаксически дойти от формул - аксиом ZFC до какой-нибудь ВТФ", я совершенно согласен с уважаемым
mihaild. Я лишь сообщил, что все-таки имеются сомневающиеся. Спасибо за ссылку.
Немного не понимаю, как можно сомневаться? Ведь по сути, если мы строим все на нек-ых утверждениях и аксиомах, используя строго определённые правила вывода, взятые из логики, то вне зависимости от того, математика ли это, или просто суждения, мы можем довести любой сложно полученный вывод до изначальных аксиом.
Так как - все промежуточные теоремы мы строим на 1)аксиомах; 2)или уже выедённых из акисом теоремах; 3)или выведенных из доказанных теорем теоремах , но мы используем одни и те же правила вывода. Следовательно исходя из науки логики, последовательно заменяя каждое суждение набором аксимом, соединённых правилами вывода, мы в конечном итоге придём к чистым соединенным аксиомам.
Из этого есть два исключения, которые порождается человеческим фактором: мы можем, сами того не понимая, совершить некоторое допущение то ли от недостатка изначальный акисиом, то ли от ошибки в рассуждениях (нерассмотрение всех случаев) или же неправильно использовать логические правила вывода. Следовательно, если теорию строить на строгих акисомах, используя одни и те же правила вывода (описанные наукой логикой), мы можем придти от сложных суждений к аксиомам.
Исходя из того, что я написал, мне интересно, как проаргумментирует свои суждения те, кто сомневаются в том, что все можно формализовать.[/off]