Синтаксис и семантика языка логики предикатов.

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

Классическое  исчисление предикатов (первого порядка) — это формальная теория, в которой определены следующие компоненты:

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

Исчисление предикатов, которое не содержит предметных констант, функторов, предикатов и собственных аксиом, называется чистым. Исчисление предикатов, которое содержит предметные константы и/или функторы и/или предикаты и связывающие их собственные аксиомы, называется прикладным.

Исчисление предикатов, в котором кванторы могут связывать только предметные переменные, но не могут связывать функторы или предикаты, называется исчислением первого порядка. Исчисления, в которых кванторы могут связывать не только предметные переменные, но и функторы, предикаты или иные множества объектов, называются исчислениями высших порядков.

 

Логика - доступно для всех