очищенная от ненадёжных рассуждений
А вот я по умолчанию считаю, что любое логичное рассуждение человека надежно. Да, можно возразить, мол люди часто ошибаются, думая, что рассуждают логично. Например, люди раньше думали, что все непрерывные функции дифференцируемы. Я бы ответил так: ну так они и не рассуждали логично. Понятие "число", "непрерывность", "дифференцируемость" элементарно даже определены не были. Т.е. они рассуждали не логично, вот и ошиблись. Что в этом удивительного?
Если рассуждать логично, то можно привести пример непрерывной нигде не дифференцируемой функции и убедиться, что она действительно такая. И по мне это будет надежно установленным фактом.
Но потом приходит матлогика и пытается меня убедить, что проверка автопрувером выводимости какой-то строчки в какой-то формальной теории множеств якобы должна меня убеждать сильнее, чем здравый смысл. Почему я должен ей верить?
Про ненадежность можно еще привести в пример парадоксы, типа Рассела. Что вот, мол, обычные рассуждения привели к ерунде. Но. Мы же про непротиворечивость
ничего не знаем, верно? Т.е. парадоксы могут быть и там. Установить средствами
ее же непротиворечивость, насколько я понимаю, мы тоже не можем. Так чем же она тогда лучше?
Извините, но задачи, стоящие перед математиками (и далеко не только перед математиками), много сложнее, чем доказательство смертности Сократа.
Вот мне очень хотелось бы увидеть примеры применения нетривиальных результатов матлогики для задач в рамках обычных математических разделов. В тех учебниках, которые я читал, была человеческая логика. В научных статьях с архива, которые я немножко из интереса просматривал, тоже была самая обычная логика. Да, многие результаты мне там были не известны, но метод то как в учебнике. Формулируем теорему, доказываем ее, потом другую, потом еще одно следствие и, если повезет, приходим к какому-то результату. Выхода за рамки обычной логики вроде как и не было.