Someone писал(а):
экси, не спорьте с Котофеичем по этому вопросу, он прав. Формулировка формальной системы без определённых представлений о натуральном числе невозможна. Даже математическую логику сформулировать не удастся, не говоря уже о собственно математических формальных системах.
А вот я попробую высказать мысль, как можно
до определённой степени избавиться от "интуитивных" представлений в основаниях математики. Можно исходить из того, что вся математика - это совокупность неких строк символов и правил манипулирования ими, а какой бы то ни было "смысл", придаваемый этим строкам, относится к применению математики, т.е. уже выходит за её пределы. В соответствии с этим пониманием "математическим объектом" всегда является строка символов в некотором алфавите, и ничто иное. Понятие "математически определено", если у нас есть способ, позволяющий построить конкретный математический объект в виде строки символов, подходящей под условие определения. Например, можно определить натуральное число в двоичном представлении, т.е. в алфавите {0,1}, если определить единицу как строку "1", и операцию инкремента как соответствующую операцию над двоичными строками, - это как раз соответствует аксиоматике Пеано.
Что касается логики, то она возникает в результате введения такого понятия, как "высказывание". Естественно, как и любой математический объект высказывание должно быть строкой символов. Собственно "высказыванием" строку символов делает наличие некоего способа (процедуры) "проверки высказывания". Если эта процедура завершается успехом, это означает, что высказывание "истинно". Далее определяются основные логические операции:
"И" завершается успехом когда проверки обоих аргументов завершаются успехом.
"ИЛИ" завершается успехом когда проверка одного из аргументов завершается успехом.
"НЕ" завершается успехом когда проверка самой процедуры проверки высказывания показала, что она не завершится успехом.
И т.п.
Таким образом логические тождества вводятся не как аксиомы, а являются следствием определений логических операций.
Это, как я понимаю, есть основы того, что называется "конструктивный анализ".
Конечно, он тоже стоит на неких базовых предположениях. Например, мы должны быть уверены, что все способны одинаково прочитать заданную строку символов (это называется "абстракция отождествления" или "распознавания"). Мы также должны быть уверены, что если у нас есть некий "теоретический" способ построения математического объекта (или проверки высказывания), то отсутствие необходимых ресурсов - достаточного количества бумаги для записи оч-чень длинной строки, достаточного времени или желания - не станет препятствием для его выполнения (это называется "абстракция потенциальной осуществимости" или "реализуемости").