Чтобы не было недопонимания, давайте я еще раз изложу свое текущее представление (хотя оно большей частью интуитивное, потому как никогда глубоко этой проблемой не занимался)
Ну тогда я, пожалуй, тоже изложу свою точку зрения.
В истории математики в некоторый момент произошел переход от того, что математика изучает некоторую идеализацию реального мира к тому, что математика изучает формальные модели, не обязательно непосредственно инерпретируемые в реальности. Мыслить об этих моделях можно по разному - как о некотором идеальном мире/мирах (платонизм), как о мысленных конструкциях математика, которые можно передавать с помощью языка (интуиционизм), как о формальных манипуляциях, смысл которым придается отдельно от самих манипуляций (формализм). Если пытаться очертить временной период, то начинается этот переход с признания комплексных чисел, создания неевклидовых геометрий и многомерных алгебр, и заканчивается кризисом оснований конца 19 - начала 20 века.
Математика до переходного периода занимается несколькими теориями, которые действительно появились на основе опыта и изучают некоторые идеальные объекты, отношения между которыми похожи на реальные. В рассуждениях без явного указания используются очевидные факты, основанные на представлениях о реальном мире - Евклид не доказывает, например, что две окружности в построении равностороннего треугольника на данном отрезке действительно пересекутся, а Ньютон не обсуждает существование площадей фигур.
Математика в переходный период характеризуется осознанием того, что если существуют несколько похожих "идеальных миров", нужно обязательно фиксировать все неявные предположения, которые мы приносим из мира реального, и если их немного менять, то можно получать что-то новое и интересное. В процессе этого старые теории постепенно заменяются на более формализованные, в которых нельзя уже просто в процессе доказательства, нигде не упоминая, использовать некое утверждение, которое кажется очевидным - все очевидные утверждения надо выписывать и они не незыблемы, их можно менять. Процесс этот доходит до самых основ и появляется необходимость зафиксировать те законы, по которым мы вообще получаем из одних утверждений другие, и самые базовым понятия мышления - появляется математическая логика и теория множеств. Старые теории, сохранив те же названия, "перековываются" под эти новые основания и отделяются от своей интерпретации в реальном мире.
Современная математика основана на этих формальных переосмыслениях теорий и начинает изучать собственно сами теории или, что то же самое, различные структуры, которые получаются фиксацией аксиом. Отправными точками являются математическая логика и построенные в процессе кризиса оснований формальная арифметика, гильбертовы основания геометрии, теория множеств, формальная конструкция действительных чисел, а также те теории, которые начали процесс отделения и которые удаляют или заменяют в некоторые законы - современная геометрия и современная алгебра.
Я утверждаю, что в современный период математические теории появлялись как формальные теории.
3) фиксировать в реальности какие-то новые объекты и отношения (пример - формирование понятия алгоритма и создание конструктивной математики).
Понятие алгоритма возникло как не менее 3 независимых формальных теорий, которые, как потом было доказано, эквивалентны.
Чёрч получил
-исчисление как остаток одной из своих теорий множеств после того, как он убрал оттуда логические операторы, приводящие к парадоксам типа расселовского. Он заметил, что в этом остатке можно формализовать натуральные числа и предложил функции, определяемые в этой теории, считать некоторым определением понятию "конструкция".
Понятие рекурсивной функции возникло как расширение понятия примитивно-рекурсивной функции, введенного Гёделем при доказательстве его теоремы о неполноте и основано на изучении предложенных Эрбраном систем равенств, по сути определение Эрбрана и Гёделя очень похоже на определение формальной системы в логике. Причем пришли Эрбран с Гёделем как раз проверкой того, сходится ли модель с опытом - после появления понятия примитивно рекурсивной функции Аккерман предложил пример "рекурсии, которая не является примитивной", то есть не примитивно рекурсивной функции, которую все согласились считать вычислимой.
И только Тьюринг строит свое определение как модель человека, который занимается некоторым рутинным вычислением, но при этом явно говорит, что все аргументы в пользу того, что именно это определение нужно считать определением вычислимости являются нематематическими.