Основные определения логики предикатов первого порядка



 

Предположим, есть некоторое множество D объектов, называемое предметной областью. Символы, обозначающие элементы этого множества, называются предметными константами, а символ, обозначающий произвольный элемент предметной области ¾ предметной переменной.

Предикат¾это логическая функция одной или нескольких переменных P(x1,x2,… xn), определенная на множестве D и принимающая одно из двух значений, «истина» и «ложь», в зависимости от значений предметных переменных. Буква P ¾ предикатный символ. Предикат, зависящий от n переменных, называется n¾местным (или n¾арным) предикатом.

Для описания некоторой предметной области на языке исчисления предикатов (ИП) определяются множества исходных элементов, правила построения формул, система аксиом и множество правил вывода, каждое из которых описывает способ построения новых формул из исходных элементов и уже построенных формул.

 Исходными элементами ИП являются следующие множества:

1) Конечное множество предметных переменных {x1,x2,…xk};

2) Конечное множество предметных констант {a1,a2,…an};

3) Конечное множество функциональных символов {f1,f2,…fm};

4) Конечное, непустое множество предикатных констант {p1,p2,…pr};

5) Логические связки: Ø (отрицание), & (конъюнкция), Ú (дизъюнкция), Þ (импликация).

6) Кванторы: " (квантор всеобщности) и $ (квантор существования).

7) Специальные символы: ( ) + - */ < > . , [ ] : ;

8) Знак пустого дизъюнкта ð, который является тождественно ложной формулой.

 

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

  Определение терма ¾ рекурсивно:

1) Терм ¾ это предметная переменная или предметная константа.

2) Если f ¾ функциональный символ, и t1,t2,…tn ¾ термы, то f(t1,t2,…tn) ¾ терм.

Предикат вида p(t1,t2,…tn), где p ¾ предикатная константа, а t1,t2,…tn ¾ термы, является элементарной формулой.

Правила построения ППФ (Правильно Построенных Формул) в логике предикатов 1-го порядка следующие:

1) Всякая элементарная формула есть ППФ.

2) Если A и B¾ ППФ, а x ¾ предметная переменная, то каждое из выражений ØA, A&B, AÚB, AÞB, ("x)A, ($x)A есть ППФ.

3) Других правил построения ППФ нет.

Для формул с кванторами справедливо следующее утверждение: формула Q(x1,x2,…,xn) получена из формулы P(x1,x2,…xn) посредством присоединения квантора, если 

Q(x1,x2,…,xn) = ("xi) P(x1,x2,…xn) или

Q(x1,x2,…,xn) = ($xi) P(x1,x2,…xn).

Пусть D={a1 , a2, …, an} есть множество предметных констант, и P(x) ¾ предикат, определенный на множестве D, тогда справедливы утверждения:

("x) P(x) = P(a1) &P(a2) &…&P(an) и

($x) P(x) = P(a1) Ú P(a2) Ú …ÚP(an).

 

Система аксиом исчисления предикатов включает в себя аксиомы исчисления высказываний А1¾А11 и две аксиомы с кванторами А12 и А13.

A1) A Þ(BÞC)

A2) (AÞ(BÞC)) Þ((AÞB) Þ(AÞC))

A3) A&B ÞA

A4) A&B ÞB

A5) (AÞB) Þ((AÞC) Þ(AÞB&C))

A6) AÞAÚB

A7) BÞAÚB

A8) (AÞC) Þ((BÞC) Þ(AÚBÞC))

A9) (AÞB) Þ(ØBÞØA)

A10) A ÞØØA

A11) ØØAÞ A

A12) ("x) A(x) ÞA(t)

A13) A(t) Þ($x) A(x), A(x) ¾ППФ, t ¾терм, не содержащий x. Все аксиомы тождественно истинны.

 

Выводом P называется такое линейно упорядоченное множество элементов, что всякий элемент P является либо аксиомой, либо заключением применения некоторого правила вывода. Формула является выводимой, если можно построить вывод, заканчивающийся этой формулой.

В исчислении предикатов определены следующие правила вывода:

1) Все аксиомы выводимы.

2) Правило подстановки.

Подстановка (ti вместо xi) есть множество q = {x1=t1,x2=t2,… xk=tk }, где x1,x2,…,xk ¾ попарно различные предметные переменные, xi¹xj при i¹j , t1,t2,…,tk  ¾ термы, если xi= ti, то ti отличается от xi.Правило подстановки означает, что если P(x1,x2,…xk)¾ выводим, то и формула P(t1,t2,…tk) =q (P(x1,x2,…xk)) ¾ выводима.

3) Правило Modus Ponens (MP).

Если А ¾ выводимая ППФ, и A ÞB¾ выводима, то B ¾ также будет выводима.

4) Правило обобщения.

Если B ÞA(x)¾ выводимая ППФ, и B не содержит вхождений x, то формула B Þ("x)A(x) ¾ также будет выводима.

5) Правило конкретизации.

Если выводима формула A(x)ÞB, и B не содержит вхождений x, то формула ($x)A(x) ÞB ¾ также будет выводима.

6) Правило переименования переменных.

Если A¾выводимая ППФ, имеющая квантор $ и (или) ", то одна связанная переменная может быть заменена другой, не меняя истинностного значения формулы. Полученная формула также будет выводима.

7) Других правил вывода нет.

 


Дата добавления: 2018-04-04; просмотров: 337;