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

(,),' - знаки пунктуации; Хъ Х2,... - счетное множество предметных переменных; яь - конечное (возможно и пустое) или счетное множество предметных констант; j f (i,k>0) - непустое, конечное или счетное множество преди­ катных букв; ( i , k > l ) - конечное (возможно и пустое) или счетное множе­ ство функциональных букв; \fxi ,3Xi (г>1) - кванторы всеобщности и кванторы существова­ ния. Различные теории первого порядка могут отличаться друг от друга составом символов. Например, в некоторых теориях могут со­ всем отсутствовать функциональные буквы. Из перечня символов видно, что некоторые из них обязательно принадлежат всем теориям первого порядка. 2. Формулы теории первого порядка определяются точно так же, как определяются формулы в логике предикатов. 3. Аксиомы теории К разбиваются на два класса: логические ак­ сиомы и собственные аксиомы. Логическиеаксиомы: каковы бы ни были формулы А, В, С тео­ рии К, следующие формулы являются логическими аксиомами теорииК\ А1: А ^ ( В ^ А у , А2: (А-=^(В^С))=>{(А:=>В)=>(А=>СУ); A3: (] ^)=^((1 В=>А)^В); А4: \ f X iA(xi)=i>A(t), здесь A(xi) есть формула теории К и t есть терм теории К, свободный ; для х, в A(xi); А5: V x ,(A=t'B)=i>(A=:>VxiB), если формула А не содержит сво­ бодных вхождений х,. Собственные аксиомы. Собственные аксиомы не могут быть сформулированы в общем случае, ибо меняются от теории к теории. 169