Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Итак, формальная теория L оказалась построенной таким образом, что ее множество теорем {! £ ) в точности совпадает с множеством "истинных" формул (Fc) формализованной теории С. Из полноты в узком смысле теории L следует, что всякая попытка расширить множество Ti приводит к противоречивой теории, поэтому нельзя к А1-АЗ добавить недоказуемую из них формулу, не приходя при этом к противоречию. Естественно выяснить, можно ли, взяв другие аксиомы и, может быть, другие правила вывода, получить 71 = Vc- Оказывается, что можно. Например, построим формальную аксиоматическую (дедуктивную) теорию Ы, которая отличается от L только тем, что вместо схем аксиом А1-АЗ здесь имеются лить три конкретные аксиомы: 1) Ai^(A2^AI), 2) (Ai^(А2^АЗ))^((AI^A2)^(Ai^As)), 3) ( —A2^—AI)^((—A2^AI)^A2), HO, кроме правила вывода MP {modus ponens), имеется еще одно правило вывода правило подстановки, разрешающее подстановку любой формулы на места всех вхождений данной пропозициональной буквы в данную формулу. При этом можно показать, что Тц = Vc =Ti. Оказывается, можно даже построить формальную аксиоматическую (дедуктивную) теорию L2 с тем же алфавитом и множеством формул, что и L, но всего с одной схемой аксиом (((^^в)^( 7С^ ']D))^E)^{{E^A)^{D^A)) и единственным правилом вывода - MP {modus ponens). Здесь тоже Ти = Vc =Ti. Возможны и другие задания формальных аксиоматических (дедуктивных) теорий так, чтобы ее множество теорем совпадало с множеством Fc. ... абстракции отражают природу глубже, вернее, полнее. В. И. Ленин (Философские тетради) § 13. Теории первого порядка Теория первого порядка (теория К) представляет собой формальную аксиоматическую теорию. Следовательно, для ее задания необходимо определить символы, формулы, аксиомы и конечное число правил вывода. 1. Символами всякой теории первого порядка служат: V= {xi, Х2, Хз,...} - счетное множество (предметных) переменных. А = {aj, а2, аз,...} - конечное (возможно и пустое) или счетное множество предметных постоянных (констант). 122