yandex rtb 1
ГоловнаЗворотній зв'язок
yande share
Главная->Математика і інформатика->Содержание->4.8. Исчисление предикатов первого порядка Теория К.

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

4.8. Исчисление предикатов первого порядка Теория К.

Символами теории К служат те же символы, что мы ввели ранее: пропозициональные связки, ¬, ,,  вспомогательные символы (,), множества предметных переменных: х1,x2,...,у1,...., предметные постоянные: а12,...,b,..., функциональные символы: f1n , i = 1,...,k, n=0,...,m., предикатные символы: P1n, i=l,...,k, n=0,...,m. Определения терма, формулы остаются в силе для теории первого порядка.

Аксиомы теории К разбивается на логические аксиомы и собственные.

Логические аксиомы. каковы бы ни были формулы А, В, С теории К, следующее формулы являются логическими аксиомами теории К

А1     АА)

A3    (АС))  ((АВ)  (АС))

A3     (¬В¬А)  ((¬ВА) В)

А4    xA(x) A(y), если у свободно для x в формуле А(х)

А5    x(AB(x)) (AxB(x)), если А не содержит свободных вхождений х.

Собственные аксиомы формулируются отдельно для каждой конкретной содержательной предметной области.

Теория первого порядка, не содержащая собственных аксиом, называется исчислением предикатов первого порядка. Правилами вывода во всякой теории первого порядка являются МР и Gen.

Аксиомы Al, A2, A3 теории К. И правило Мр определены в теории L, следовательно, все теоремы теории L включены во множество теорем теории К.

Метатеорема дедукции а теории К может быть сформулирована в ослабленном виде.

Метатеорема дедукции. Если существует вывод формулы В из множества гипотез Г и формулы Айв этом выводе ни при каком применении  правила  Gen  к  формулам,  зависящим  от   А,   не   связывается квантором никакая свободная переменная формулы А, то Г |— АВ.

Следствие 1. Если существует вывод Г|— АВ и в этом выводе ни разу не применялось правило Gen к формулам, зависящим от А, то Г|— АВ.

Следствие 2. Если существует вывод Г |—А. где А -замкнутая формула, то Г|— АВ,

 

29