Исчисление предикатов

(Чистое) исчисле́ние предика́тов (первого порядка) - это формальная теория \mathcal K, в которой определены следующие компоненты:

1. Алфавит:

связки основные \neg,\to
  дополнительные \lor,\land
служебные символы   ( , )
кванторы всеобщности \forall
  существования \exists
предметные константы a,b,...,a1,b1,...
  переменные x,y,...,x1,y1,...
предметные предикаты P,Q,...
  функторы f,g,...

С каждым предикатом и функтором связано некоторое натуральное число, которое называется арностью, или местностью.

2. Формулы имеют следующий синтаксис:

\langleформула\rangle ::= \langleатом\rangle|

\neg\langleформула\rangle|
(\langleформула\rangle\to\langleформула\rangle)|
\forall\langleпеременная\rangle \langleформула\rangle|

\exists\langleпеременная\rangle \langleформула\rangle
\langleатом\rangle ::= \langleпредикат\rangle(\langleсписок термов\rangle)
\langleсписок термов\rangle ::= \langleтерм\rangle|\langleтерм\rangle,\langleсписок термов\rangle
\langleтерм\rangle ::= \langleконстанта\rangle|

\langleпеременная\rangle|

\langleфунктор\rangle(\langleсписок термов\rangle)

При этом необходимо учитывать следующие контекстные условия: в терме f(t1,...,tn) функтор f должен быть n-местным. В атоме (или атомарной формуле) P(t1,...,tn) предикат P должен быть n-местным.

Вхождения переменных в атомарную формулу называются свободными. Свободные вхождения переменных в формулах A и B остаются свободными в формулах \neg A и A \to B. В формулах \forall x A и \exists x A формула A, как правило, имеет свободные вхождения переменной x. Вхождения переменной x в формулы \forall x A и \exists x A называются связанными. Вхождения других переменных (отличных от x), которые были свободными в формуле A, остаются свободными и в формулах \forall x A и \exists x A. Формула, не содержащая свободных вхождений переменных, называется замкнутой.

3. Аксиомы (логические): любая система аксиом исчисления высказываний, плюс

P_1: \forall x A(x) \to A(t),

P_2: A(t) \to \exists x A(x),

где терм t свободен для переменной x в формуле A.

4. Правила вывода:

{A, A \to B}\over B Modus ponens, \frac{B \to A(x)}{B \to\forall x A(x)}\ \forall^+, \frac{A(x) \to B}{\exists x A(x) \to B}\ \exists^+,

где формула A содержит свободные вхождения переменной x, а формула B их не содержит.

 
Начальная страница  » 
А Б В Г Д Е Ж З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Ы Э Ю Я
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
0 1 2 3 4 5 6 7 8 9 Home