Теоретико-множественная установка нашла свое приложение и в логике. Она воплотилась в трудах выдающегося логика Готлоба Фреге (2848—1925), профессора математика Иенского университета. Беспощадный критик математических работ, содержащих хотя бы мелкие логические дефекты, человек пуританского поведения и нелегкого для окружающих характера, фанатически преданный науке труженик, он фактически был создателем современного аксиоматико-дедуктивного метода построения математических теорий. Этот метод был разработан им уже в работе 1879 года — с этого года обычно датируют начало исследований по логическим основаниям математики, носившей название «Запись в понятиях», а затем развернуто в двухтомном труде (при своем появлении почти никем не замеченном) «Основные законы арифметики» (1893, 1902). В первом томе этого труда в неявной форме содержалось широко известное теперь формально-логическое противоречие.. Узнав об этом противоречии (как это произошло, мы расскажем ниже), Фреге так же резко осудил труд своей жизни, как осуждал слабые работы других. Мы дадим краткую характеристику достижений Фреге в области формализации логики, а затем расскажем о трактовке им понятия натурального числа — основного понятия арифметики, да и, по-видимому, математики вообще[17].
В предыдущей главе мы привели пример формальной системы — некоторого исчисления равенств, интерпретации которого содержали булевы алгебры. Обсудим теперь вопрос о формализации математических теорий вообще. При полной формализации теории никаких «интуитивно понятных» действий над объектом теории не допускается: все должно быть заложено в ее синтаксисе (алфавите, правилах образования формул) и средствах дедукции — постулатах (включая правила введения новых знаков для сокращения записи комбинаций основных знаков[18]).
В общем случае полностью формализованная математическая теория имеет два этажа — формализованную логику и надстроенную над ней специально математическую часть (в случае формальной арифметики этой частью является теория натуральных чисел). Логическая часть обычно строится не как исчисление равенств, а как пропозициональное исчисление — исчисление высказываний[19], расширяемое в исчисление предикатов.
Обрисуем кратко пропозициональную (относящуюся к высказываниям) часть такого рода аксиоматически-дедуктивной системы. В качестве схем аксиом в ней выбирается конечный (как правило, небольшой) набор формул (схем формул). В системе Фреге, в которой из числа логических знаков фигурировали только знаки отрицания и импликации, постулатами были формулы (схемы формул):
1. (α → (β → α))
2. ((α → (β → γ)) → ((α → β) → (α → γ)))
3. ((α → (β → γ)) → (β → (α → γ)))
4. ((α → β) → (~α → ~β))
5. (α → ~~α)
6. (~~α → α).
объявляемые аксиомами (схемами аксиом), и правило вывода, называемое обычно
«Если доказаны формулы вида (α → β) и α, то доказана формула β» (отметим, что это — постулаты его работы 1879 г.)[20].
Нетрудно проверить, что любая формула, имеющая структуру какой-либо схемы аксиом, является тождественно-истинной (проверку можно осуществить, построив для каждой схемы аксиом соответствующую ей таблицу истинности). Можно также убедиться, что правило модус поненс, как говорят, сохраняет тождественную истинность, то есть, что если формулы (α → β) и α тождественно-истинны, то тождественно-истинной будет и формула β (в самом деле, если формулы (α → β) и а принимают значение «истинно», то β, как это ясно из таблицы для импликации, может иметь только то же самое значение).
Это дает основание объявить любую формулу, подпадающую под какую-либо из схем 1 —6, верной, или доказанной (доказуемой), формулой и считать, что всякая формула, полученная из ранее доказанных формул по модусу поненсу, есть тоже доказанная (доказуемая) формула. Таким образов описанная система постулатов задает процесс порождение доказанных формул—теорем системы. Можно показав что если формула является тождественно-истинной в табличной интерпретации, она когда-либо неизбежно появится в качестве теоремы в упомянутом процессе (в этом состоит
Построение логической теории высказываний в видь дедуктивной системы очерченного или родственного типа — как