3.2. Исчисление предикатов
Исчисление предикатов первого порядка – это формальная теория K, в которой определены :
1. Алфавит:
· Связки: (основные), & ,
( дополнительные).
· Служебные символы: (,).
· Кванторы ,
.
· Предметные константы a,b,c,….
· Предметные переменные x, y, z,….
· Символы предикатов P,Q,R,….
· Символы функций f, g, h,….
Константы, переменные, функторы – называются термами.
2. Формулы. Слово называется формулой, если оно имеет следующий синтаксис:
1) Р(х1,…,хn) – атомарная формула (А).
Вхождения переменных в атомарную формулу называются свободными.
2) Если А – формула, то - тоже формула.
3) Если А и В – формулы, то - формулы.
4) Если А – формула, содержащая свободную переменную х, то - формулы.
Слово является формулой, если это следует из 1-4.
Вхождения переменных в формулах называются связанными, переменные не равные х остаются свободными.
Пример
- х – свободная переменная, у – связанная переменная.
Формула, не содержащая свободных переменных, называется замкнутой.
3. Аксиомы (логические).
1) Любая система аксиом исчисления высказываний.
А1:
А2:
А3:
2) Собственные аксиомы.
P1: ,
P2:,
где t – терм.
4. Правила вывода.
1. ,
2. - введение квантора общности,
3. - введение квантора существования.
Исчисление предикатов, в котором кванторы могут связывать только предметные переменные и не могут связывать функторы или предикаты называется исчислением первого порядка.