Достаточно о логике. Давайте зададимся вопросом, как можно передавать математические знания? На мой взгляд, нет принципиальной разницы между применением языка для этой и для других целей. Мы используем язык, чтобы воздействовать на мысли и поступки других людей. Когда математик пишет статью или книгу, он рассчитывает предложить математическое построение другим людям; когда он делает записи, он, будущий, играет роль другого лица. Как и любое другое использование языка, передача математических сведений не спасает от непонимания. Имеются серьезные основания полагать, что построение небольших натуральных чисел одинаково для всех людей, но что касается сообщения о более сложных структурах, даже серьезные усилия добиться ясности не могут гарантировать полное понимание.
В этом отношении интуиционизм полностью противостоит формализму. Моей задачей не является описание позиции формализма, но сравнение обоих направлений могло бы способствовать прояснению каждого из них. Я позволю себе рассмотреть наиболее радикальный вид формализма, который лучше всего подходит для сравнения с интуиционизмом. Формалист смотрит на каждое интуитивное математическое рассуждение как на неточное. Он изучает язык, на котором выражены такие рассуждения, и пытается формализовать его. В результате получается формальная система, состоящая из конечного числа символов и конечного числа правил образования из них формул. С интуиционистской точки зрения, этот процесс относится к прикладной математике, и результатом служит очень простая математическая система. Эта формальная система может применяться в науке и в промышленности, ее роль сравнима с функцией машины на фабрике.
Конечно, у нас нет возражений против деятельности формалистов, и также несомненно, что ученые и инженеры больше заинтересованы в самих математических формулах, нежели в их абстрактной интерпретации. Между интуиционизмом и формализмом не возникает конфликтов, пока каждый из них придерживается своего предмета: интуиционизм — умственных построений, формализм — построения формальных систем, мотивированных их внутренней красотой или пользой для науки и промышленности. Но разногласия возникают, когда формалисты утверждают, что их системы выражают математическое мышление. Против этого интуиционисты выдвигают два возражения. Во-первых, как я только что объяснил, умственные построения не могут быть полноценно переданы посредством языка; во-вторых, обычная интерпретация формальных систем непригодна для умственного построения.
За время исследований формалистов была проделана большая работа в области доказательств непротиворечивости. С той точки зрения, которую я обрисовал, их ценность в основном практическая. Противоречивая система, в которой выводима любая формула, не может быть полезной. Претензии на то, что доказательство непротиворечивости предоставляет интерпретацию формальной системы, абсолютно необоснованны.
Однако, в интуиционистской математике формальные методы имеют свою область применения. Они — лучшие методы исследования предположений, использованных в заданных доказательствах. В последние годы они успешно применялись к доказательствам в Брауэровской теории последовательностей выбора. Формализация интуиционистской логики служит и другой цели, а именно, для выражения логических теорем на языке, понятном традиционным математикам. Метаматематическая работа над формальной системой интуиционистской логики, как бы интересна сама по себе она ни была, имеет мало общего с интуиционистской математикой.
