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

 

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

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

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

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

1) Конечное множество предметных переменных {x₁,x₂,…x_k};

2) Конечное множество предметных констант {a₁,a₂,…a_n};

3) Конечное множество функциональных символов {f₁,f₂,…f_m};

4) Конечное, непустое множество предикатных констант {p₁,p₂,…p_r};

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

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

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

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

 

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

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

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

2) Если f ¾ функциональный символ, и t₁,t₂,…t_n ¾ термы, то f(t₁,t₂,…t_n) ¾ терм.

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

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

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

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

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

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

Q(x₁,x₂,…,x_n) = ("x_i) P(x₁,x₂,…x_n) или

Q(x₁,x₂,…,x_n) = ($x_i) P(x₁,x₂,…x_n).

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

("x) P(x) = P(a₁) &P(a₂) &…&P(a_n) и

($x) P(x) = P(a₁) Ú P(a₂) Ú …ÚP(a_n).

 

Система аксиом исчисления предикатов включает в себя аксиомы исчисления высказываний А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) Правило подстановки.

Подстановка (t_i вместо x_i) есть множество q = {x₁=t₁,x₂=t₂,… x_k=t_k }, где x₁,x₂,…,x_k ¾ попарно различные предметные переменные, x_i¹x_j при i¹j , t₁,t₂,…,t_k  ¾ термы, если x_i= t_i, то t_i отличается от x_i.Правило подстановки означает, что если P(x₁,x₂,…x_k)¾ выводим, то и формула P(t₁,t₂,…t_k) =q (P(x₁,x₂,…x_k)) ¾ выводима.

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; просмотров: 591; Мы поможем в написании вашей работы!

Поделиться с друзьями:

---

---

Мы поможем в написании ваших работ!