|
В предыдущей главе мы привели пример формальной системы – некоторого исчисления равенств, интерпретации которого содержали булевы алгебры. Обсудим теперь вопрос о формализации математических теорий вообще. При полной формализации теории никаких «интуитивно понятных» действий над объектом теории не допускается: все должно быть заложено в ее синтаксисе (алфавите, правилах образования формул) и средствах дедукции – постулатах (включая правила введения новых знаков для сокращения записи комбинаций основных знаков[79]). В общем случае полностью формализованная математическая теория имеет два этажа – формализованную логику и надстроенную над ней специально математическую часть (в случае формальной арифметики этой частью является теория натуральных чисел). Логическая часть обычно строится не как исчисление равенств, а как пропозициональное исчисление – исчисление высказываний[80], расширяемое в исчисление предикатов. Обрисуем кратко пропозициональную (относящуюся к высказываниям) часть такого рода аксиоматически‑дедуктивной системы. В качестве схем аксиом в ней выбирается конечный (как правило, небольшой) набор формул (схем формул). В системе Фреге, в которой из числа логических знаков фигурировали только знаки отрицания и импликации, постулатами были формулы (схемы формул): 1. (? ? (? ? ?)) 2. ((? ? (? ? ?)) ? ((? ? ?) ? (? ? ?))) 3. ((? ? (? ? ?)) ? (? ? (? ? ?))) 4. ((? ? ?) ? (~? ? ~?)) 5. (? ? ~~?) 6. (~~? ? ?). объявляемые аксиомами (схемами аксиом), и правило вывода, называемое обычно модус поненс (лат. modus ponens): «Если доказаны формулы вида (? ? ?) и ?, то доказана формула ?» (отметим, что это – постулаты его работы 1879 г.)[81]. Нетрудно проверить, что любая формула, имеющая структуру какой‑либо схемы аксиом, является тождественно‑истинной (проверку можно осуществить, построив для каждой схемы аксиом соответствующую ей таблицу истинности). Можно также убедиться, что правило модус поненс, как говорят, сохраняет тождественную истинность, то есть, что если формулы (? ? ?) и ? тождественно‑истинны, то тождественно‑истинной будет и формула ? (в самом деле, если формулы (? ? ?) и а принимают значение «истинно», то ?, как это ясно из таблицы для импликации, может иметь только то же самое значение). Это дает основание объявить любую формулу, подпадающую под какую‑либо из схем 1 –6, верной, или доказанной (доказуемой), формулой и считать, что всякая формула, полученная из ранее доказанных формул по модусу поненсу, есть тоже доказанная (доказуемая) формула. Таким образов описанная система постулатов задает процесс порождение доказанных формул–теорем системы. Можно показав что если формула является тождественно‑истинной в табличной интерпретации, она когда‑либо неизбежно появится в качестве теоремы в упомянутом процессе (в этом состоит полнота исчисления высказываний)[82]. — 63 —
|