Определим синтаксис логики предикатов первого порядка.
Классическое исчисление предикатов (первого порядка) — это формальная теория, в которой определены следующие компоненты:
1. Алфавит
связки основные Ø ®
дополнительные & Ú
служебные символы ( , )
кванторы всеобщности «
существования $
предметные константы a, b, …, a1, b1, …
переменные x, y, …, x1,y1, …
предметные предикаты P, Q, …
функторы f, g, …
2. Формулы имеют следующий синтаксис:
<�формула> :: = <�атом> |
Ø<�формула> |
(<�формула> ® <�формула>)
«<�переменная><�формула>|
$< переменная >< формула >
<�атом> :: = <�предикат>(<�список термов>)
<�список термов> :: = <�терм> | <�терм>, <�список термов>
<�терм> :: = <�константа> |
<�переменная> |
<�функтор>(<�список термов>)
При этом должны быть выполнены следующие контекстные условия: в терме f(t1, …, tn) функтор f должен быть n-местным. В атоме (или атомарной формуле) P(t1, …, tn) предикат P должен быть n – местным.
Вхождения переменных в атомарную формулу называются свободными. Свободные вхождения переменных в формулах А и В остаются свободными и в формулах ØАи А ® В. Вхождения переменной x в формулы «x A и $x A называются связанными. Вхождения других переменных (отличных от x), которые были свободными в формуле А, остаются свободными. Формула, не содержащая свободных вхождений переменных, называется замкнутой.
Формулы вида A и ØA, где A — атом, называются литеральными формулами (или литералами).
В формулах «x A и $x A подформула A называется областью действия квантора по x.
Обычно связки и кванторы упорядочивают по приоритету следующим образом: Ø, «, $, &, Ú, ®. Лишние скобки при этом опускают.
Терм t называется свободным для переменной x в формуле A, если никакое свободное вхождение переменной x в формулу A не лежит в области действия никакого квантора по переменной y, входящей в терм t. В частности, терм t свободен для любой переменной по формуле A, если никакая переменная терма не является связанной переменной формулы A
Исчисление предикатов, которое не содержит предметных констант, функторов, предикатов и собственных аксиом, называется чистым. Исчисление предикатов, которое содержит предметные константы и/или функторы и/или предикаты и связывающие их собственные аксиомы, называется прикладным.
Исчисление предикатов, в котором кванторы могут связывать только предметные переменные, но не могут связывать функторы или предикаты, называется исчислением первого порядка. Исчисления, в которых кванторы могут связывать не только предметные переменные, но и функторы, предикаты или иные множества объектов, называются исчислениями высших порядков.