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

При исследовании конкретной математической теории фиксируют некоторые наборы исходных предикатных символов соответствующей арности , исходных функциональных символов соответствующей арности и исходных предметных символов .

Множество называется алгебраическим типом или сигнатурой математической теории.

Принципиальное отличие УИП от ИП заключается в следующем.

1. Алфавит УИП состоит из предметных переменных, логических и вспомогательных символов, а также некоторых исходных предикатных символов соответствующей арности , некоторых исходных функциональных символов соответствующей арности и некоторых исходных предметных символов .

В результате элементы области интерпретации такого языка будут описываться не только с помощью предметных переменных, но и с помощью так называемых термов – специальных выражений языка, которые индуктивно определяются следующим образом:

а) все предметные переменные и предметные символы являются термами,

б) если f – сигнатурный n-арный функциональный символ и – термы, то выражение является термом.

2. Формулы УИП определяются по аналогии с формулами ИП за исключением исходного шага индукции – определения атомарных формул, которые в данном случае имеют вид выражений , для любых термов и сигнатурных n-арных предикатных символов P.

Записывают , если в формулу F входят предметные переменные .

Формула без свободных вхождений переменных называется замкнутой формулой или предложением.

3. Множество аксиом УИП описывается пятью определенными в предыдущем разделе схемами аксиом , в которых теперь являются произвольными формулами УИП, и дополнительной системой формул S специальных аксиом рассматриваемой математической теории. Аксиомы первого вида называются логическими и аксиомы второго вида – нелогическими аксиомами УИП.

4. Правилами вывода УИП являются правило modus ponens (MP) и правило обобщения (Gen).

5. Формула F называется теоремой УИП, если найдется такая конечная последовательность формул , в которой =F и каждая формула либо является логической аксиомой из схем , либо является нелогической аксиомой из множества S, либо получается из некоторых предыдущих формул этой последовательности по одному из правил вывода MP или Gen.

Последовательность формул называется выводом или доказательством формулы F.

Вывод формулы F сокращенно обозначают символом |-F и говорят, что «F есть теорема». Множество всех таких теорем обозначается символом Th_W(S) и называется элементарной теорией (или теорией первого порядка) узкого исчисления предикатов сигнатуры W с множеством аксиом S.

Принципиальное отличие интерпретации формул языка УИП от описанной ранее интерпретации формул алгебры предикатов заключается в том, что определение истинности формул УИП сигнатуры W вводится с помощью интерпретации этого языка в конкретных алгебраических системах с первоначально фиксированными предикатными, функциональными и предметными символами сигнатуры W.

Для придания содержательного смысла формулам УИП сигнатуры W сначала задается область интерпретации – непустое множество M, которое является областью возможных значений всех предметных переменных, и затем на этом множестве M для каждого символа сигнатуры фиксируется соответствующий математический объект: для каждого предикатного символа арности фиксируется -арное отношение на множестве M, для каждого функционального символа арности фиксируется -арная алгебраическая операция на множестве M и для каждого предметного символа фиксируется элемент в множестве M.

В результате получается алгебраическая система с основным множеством M, которая называется алгебраической W-системой и обозначается или просто . Такая система называется также интерпретацией языка УИП сигнатуры W.

Конкретные значения предметным переменным по-прежнему присваиваются с помощью оценок предметных переменных, т.е. отображений a таких переменных в область интерпретации M.

Не нашли, что искали? Воспользуйтесь поиском по сайту: