Математическая логика и теория алгоритмов

взяв другие аксиомы и, может бь!ть, другие правила вывода, получить ti = vc, Оказывается, что можно. Например, построим формальную аксиоматическую (дедуктивную) теорию £ 1, которая отличается от L только тем, что вместо схем аксиом А1-АЗ здесь имеются лишь три конкретные аксиомы: 1)ai=:>(a2=> ai); 2) (AI=>(A2=> АЗ))=>((А1=> A2)=>(AI=> A})); 3) ('U2=i>1 /(i)=>((1 A2=>A I)=:> A2), ho, кроме правила вывода MP {modusp o n e n s ) , имеется еще одно пра­ вило вывода - правило подстановки, разрешающее подстановку лю­ бой формулы на места всех вхождений данной пропозициональной буквы в данную формулу. При этом можно показать, что Г/л = Vc =T l . Оказывается, можно даже построить формальную аксиоматиче­ скую (дедуктивную) теорию L2 с тем же алфавитом и множеством формул, что и L, но всего с одной схемой аксиом (((-r^[=>5)=i>('l D))=i>E)=:>{{E=i>A)=>{D=i>A)) и единственным правилом вывода - MP (modusp o n e n s ) . Здесь тоже Tj.2 = Vc =Tr^. Возможны и другие задания формальных аксиоматиче­ ских (дедуктивных) теорий так, чтобы ее множество теорем совпадало с множеством Vc. ...абстракции отражают природу глубже, вернее, полнее. В. И. Ленин § 13. Теории первого порядка Теория первого порядка (теория К) представляет собой фор­ мальную аксиоматическую теорию, Следовательно, для ее задания необходимо определить символы, формулы, аксиомы и конечное чис­ ло правил вывода. 1. Символами всякой теории первого порядка служат: 1,=^ - пропозициональные связки; 168