Я аспирант по математике, а не философ, поэтому, пожалуйста, потерпите меня. Тем не менее, мне интересно узнать, на что именно я провожу большую часть своей недели!
На практике математическое доказательство, по-видимому, не является явной формальной дедукцией в рамках формальной системы. Вместо этого доказательство кажется своего рода критическим осмыслением вещей, которые кажутся обязательно истинными. Предположения, используемые в этом мышлении, могут быть разумно идентифицированы, но они не формулируются явно в самом начале.
Учитывая это, какова природа математических выводов на практике? Являются ли они «неформальными выводами»? Есть ли какие-либо эпистемологические преимущества в явном формировании математических выводов в рамках формальной системы, а не в том, что обычно практикуется (например, вы, вероятно, не доказали что-то вроде фундаментальной теоремы исчисления, проследив ее до аксиом, таких как ZFC, но, возможно, это должно быть Выполнено)? Если да, то почему это не стандартная процедура в математическом сообществе?
Я надеюсь, что эти вопросы, по крайней мере, относительно ясны - и заранее спасибо за любые идеи!
Мне кажется, что доказательство — или, по крайней мере, имеет тенденцию быть — чем-то, что, по мнению математиков в соответствующей области, может быть формализовано. Формализация будет включать в себя явное указание тех шагов, которые в противном случае неявно принимаются как действительные. Проблема в том, что это, вероятно, затенит основной результат кучей деталей, так что чтение корректуры фактически потратит время читателей, заставив их пробираться через результаты, которые они уже давно приняли. Вероятно, поэтому формализация не является «стандартной процедурой в математическом сообществе».
При этом формализация привлекает все больше внимания из-за растущего интереса к компьютерным доказательствам; ср. этот пост Майка Шульмана о компьютерной формализации . В частности, обратите внимание на комментарий Шульмана о «дополнительном преимуществе занятий математикой с помощником по доказательству (в отличие от формализации математики, которую вы уже сделали на бумаге), что, я думаю, особенно заметно для теории типов и теории гомотопических типов».
Ваше доказательство может быть не совсем формальным, но ожидается, что оно должно быть по крайней мере фальсифицируемым. Если бы она была полностью формальной, то ее можно было бы не только фальсифицировать, но и верифицировать. Если кто-то просматривает ваше доказательство и указывает на ошибки или пробелы, ожидается, что вы признаете ошибки и либо признаете пробелы, либо объясните, как эти пробелы можно заполнить.
От вас как от автора доказательства и от вашей аудитории ожидают большего. Если ваша аудитория просто не заметит ваше доказательство или у нее есть более важные дела, чем прочитать и проверить ваше доказательство, то ваше доказательство еще не является настоящим математическим доказательством. Но если есть читатели, и они указывают на ошибки или дыры, то автор должен постараться ответить адекватно. Читатели заметят, если вы не ответите должным образом на вопросы и возражения. Для них это будет похоже на игру в шахматы с ребенком, который еще не до конца понимает правила игры. Они могут попытаться объяснить правила, но часто в результате ваше доказательство просто игнорируется и больше не считается частью математики.
Гипносифл
Джеймс Кингсбери