Аксиоматическая система исчисления предикатов

Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947;

Предикатов исчисление (Есенин-Вольпин А.С.). – В кн.: Философская энциклопедия, т. 4. М., 1967;

Клини С.К. Введение в метаматематику. М., 1957;

Мендельсон Э. Введение в математическую логику. М., 1976;

Новиков П.С. Элементы математической логики. М., 1973;

Смирнов В.А. Формальный вывод и логические исчисления. М., 1972;

Чёрч А. Введение в математическую логику, т. I. М., 1960;

А philosophical companion to first-order logic, ed. R.I.G.Hughe, 1993;

From Frege to Gödel: A source book in mathematical logic 1879–1931, Harvard University Press, 1967;

Smullyan R.M. First-order Logic. N. Y., 1968.

В.И.Маркин

Свойства формализованного исчисления предикатов
Формализованное исчисление предикатов (ФИП) развито достаточно глубоко, и теперь, как и в случае формализованного исчисления высказываний, надлежит рассмотреть свойства (или метатеорию) этого исчисления. Но теперь в области предикатов логика достигает такой выразительной силы, что становится логическим основанием конкретных математических теорий, и теоремы (по сути, метатеоремы) о логике рассуждений достигают поистине философской глубины.
Оправданность аксиоматизации
Теорема оправданности аксиоматизации утверждает, что если  , то  , т.е. из синтаксической выводимости следует семантическая выводимость. Ее очевидным следствием будет утверждение о том, что всякая теорема ФИП является общезначимой формулой (тавтологией) логики предикатов. Смысл этой теоремы состоит в утверждении фактически того, что мы не были "излишне щедры" в выборе аксиом и правил вывода для нашего формального исчисления и не включили в их число ничего лишнего, ибо доказуемыми в этом исчислении оказываются лишь общезначимые формулы логики предикатов. Доказательство этой теоремы не очень сложное, и мы получим ее в качестве следствия несколько более общей теоремы. Обратное же утверждение "если  , то  (т.е. при выборе аксиом и правил вывода мы не проявили и "излишней скромности", и для всякой общезначимой формулы логики предикатов в нашем ФИП вполне достаточно формальных средств, чтобы доказать ее), уже не столь очевидно, и доказательство его, приводимое дальше, потребует от нас значительно больших усилий.
Теорема оправданности имеет глубокий смысл: она оправдывает наши занятия математикой, убеждая в том, что наши логические рассуждения и умопостроения не уводят нас от смысла и от практики.