Page 64 - 4570

63

Для будь-якого R є ціле додатне j , таке, що для множини формул
i
A , A ,..., A і будь-якої формули A ефективно вирішується питання, чи
1 2 j
знаходяться ці формули A , A ,..., A у відношенні R з формулою A , і якщо це
1 2 j i
так, то A називають безпосереднім наслідком формул A , A ,..., A за
1 2 j
правилом R ( ,A A ,..., A ├ А.
)
i 1 2 j
Означення 2.22. Виведенням у теорії L називають таку послідовність
формул A , A ,..., A , коли будь-яка з формул A є або аксіомою, або
1 2 n i
безпосереднім наслідком деяких попередніх формул за одним із правил
виведення.
Означення 2.23. Теоремою теорії L називають таку формулу A , коли
існує виведення в теорії L формули A , в якому останнім елементом є формула
A . Це виведення називають виведенням формули А в теорії L.
Якщо є алгоритм для перевірки, чи А є теоремою теорії L, то теорію L
називають розв’язною теорією, інакше – теорією, що є нерозв’язною.
Означення 2.24. Формулу А називають наслідком у теорії L множини
формул Г тоді і тільки тоді, коли існує така послідовність формул A , A ,..., A ,
1 2 n
що A  A , і будь-яка з формул A є або аксіомою, або елементом Г, або
n i
безпосереднім наслідком деяких попередніх формул за одним із правил
виведення.
Послідовність A , A ,..., A називають виведенням А із Г, а елементи
1 2 n
множини Г – гіпотезами виведення.
Запис Г ├ А означає, що А є наслідком множини формул Г. Якщо множина
Г скінченна Г  { ,B B ,..., B ├ А, то пишуть B , B ,..., B ├ А. Якщо Г –
}
1 2 n 1 2 n
порожня множина , то запис Г ├ А можливий тоді і тільки тоді, коли А є
теорема. Замість  ├ А прийнято писати ├ А. Таким чином, ├ А є скороченим
підтвердженням, що А – теорема.
Наведемо декілька простих властивостей поняття виведення із посилок.
1. Якщо Г   і Г ├ А, то  ├ А.

2. Г ├ А тоді і тільки тоді, коли в Г є скінченною підмножиною  , для
якої  ├ А.
3. Якщо  ├ А і Г ├ А для будь-якого В із множини  , то Г ├ А.
Властивість 1 показує, що якщо А виведене із множини посилок Г, то вона
залишиться виведеною, якщо додати до Г нові посилки. Частина «тоді»
твердження 2 випливає із 1. Частина «тільки тоді» – це твердження є
очевидним, якщо будь-яке виведення А із Г використовує скінченне число
посилок із Г. Твердження 3 означає, якщо А вивідне із  і кожна формула, яка
є в  , також вивідна з Г, то А виводимо із Г.
Формальна аксіоматична теорія L для числення висловлювань задається
таким способом.
1. Символами теорії L є ,  , (,) і букви А і із цілими додатними числами
в ролі індексів: A , A , A ,.... Символи   , (,) називають примітивними
,
1 2 3
зв’язками, а А і – пропозиційними змінними, або пропозиційними буквами.