Логіка першого порядку — Вікіпедія

Логіка першого порядку (числення предикатів) — це формальна система в математичній логіці, в якій допускаються висловлення відносно змінних, фіксованих функцій, і предикатів. Є розширенням логіки висловлювань. В свою чергу є частковим випадком логіки вищого порядку[en].

Визначення[ред. | ред. код]

Мови логіки першого порядку будуються на основі сигнатури, що складається із множини функціональних символів і множини предикатних символів . З кожним функціональним і предикатним символом пов'язана арність (число агрументів). Крім того використовуються додаткові символи:

  • Символи змінних, зазвичай і т. д.,
  • Пропозиційні зв'язки: ,
  • Квантори: загальності та існування ,
  • Службові символи: дужки і кома.

Перелічені символи разом із символами з і утворюють Алфавіт логіки першого порядку. Складніші конструкції визначаються індуктивно:

  • Терм — це символ змінної, або має вид , де  — функціональний символ арності , а  — терми.
  • Атом — має вид , де  — предикатний символ арності , а  — атоми.
  • Формула — це або атом, або одна з наступних конструкцій: , де  — формули, а  — змінна.

Змінна називається зв'язаною в формулі , якщо має вид або , або може бути представлена в одній з форм , причому вже зв'язана в , і .

Якщо не зв'язана в , її називають незв'язаною в . Формулу без незв'язаних змінних називають замкнутою формулою. Теорією першого порядку називають довільну множину замкнутих формул.

Аксіоматика[ред. | ред. код]

Наступна система логічних аксіом логіки першого порядку містить усі аксіоми числення висловлень (у наведеному випадку — аксіоми Лукашевича) та дві додаткові аксіоми:

  1. ,
  2. , якщо не присутній в в незвязаному стані

У четвертій аксіомі  — формула, одержана внаслідок підстановки терма замість змінної в формулі . Підстановка деякого терма замість змінної можлива не в усіх випадках. Умови існування такої підстановки та її результат можна визначити індуктивно.

  • Якщо  — атомарна формула, то терм може замінити довільну змінну цієї формули. Результат позначається .
  • Якщо має вигляд тоді підстановка замість можлива лише тоді, коли така підстановка можлива для формули і тоді дорівнює
  • Якщо має вигляд , тоді підстановка замість можлива лише тоді, коли така підстановка можлива для формул і тоді рівна
  • Якщо має вигляд , тоді підстановка замість можлива у двох випадках:
    • Змінна зустрічається у формулі лише у зв'язаному стані.
    • змінна не зустрічається у термі і підстановка замість можлива у формулі Тоді результат визначається наступним чином:
    • Якщо дорівнює , то дорівнює
    • Якщо не дорівнює , то дорівнює

Окрім того є два правила виводу:

  • Modus ponens:
  • Правило узагальнення (GEN):

Ці аксіоми і правила виводу є схемами і можна заміняти довільними формулами.

В цій аксіоматиці використовуються лише дві пропозиційні зв'язки: і квантор загальності . Інші пропозиційні зв'язки і квантор існування можна визначити наступним чином:

  • позначає
  • позначає
  • позначає

Усі наведені вище аксіоми називаються логічними. Якщо не існує інших аксіом, то таку формальну систему називають численням предикатів першого порядку. Числення предикатів першого порядку є прикладом теорії першого порядку. Усі теорії першого порядку визначаються подібно до числення предикатів першого порядку, однак вони мають додаткові аксіоми, які ще називають власними аксіомами теорії.

Виведення формул і теорем[ред. | ред. код]

Нехай деяка множина формул мови першого порядку, а  — деяка задана формула. Тоді кажуть, що формула виводиться з множини формул (позначається ), якщо існує така скінченна послідовність формул , де для кожної формули :

  1. є аксіомою, або
  2. належить множині або
  3. виводиться з попередніх формул послідовності за допомогою котрогось із правил виводу.

Якщо при цьому множина  — порожня (формула виводиться лише за допомогою аксіом і правил виводу), то формула називається теоремою (для цього використовується позначення ).

Множина формул називається несуперечливою, якщо для довільної формули не виконується одночасно і .

Приклад виведення[ред. | ред. код]

Доведемо, що

Приклад виводу
Номер Формула Спосіб одержання
1 Гіпотеза
2 Правило узагальнення і 1
3 Гіпотеза
4 2, 3 і modus ponens
5 Правило узагальнення і 4.

Приклади теорій першого порядку[ред. | ред. код]

Теорія груп[ред. | ред. код]

У цьому випадку маємо один функціональний символ арності 0 (позначимо його ), один функціональний символ арності 2 (позначимо його ) і один предикатний символ арності 2 (позначимо його ). Також писатимемо і замість і .

Власні формули теорії:

  1. (властивість асоціативності)
  2. (властивість нейтрального елемента)
  3. (існування оберненого елемента)
  4. (рефлексивність рівності)
  5. (симетричність рівності)
  6. (транзитивність рівності)
  7. (підстановка рівності)

Теорія абелевих груп[ред. | ред. код]

Використовуються усі позначення і аксіоми попереднього пункту, а також додаткова аксіома комутативності:

Семантика[ред. | ред. код]

У класичній логіці інтерпретація формул логіки першого порядку задається на моделі першого порядку, яка визначається такими даними:

  • Базова множина[en] ,
  • Семантична функція , що відображає
    • кожен -арний функціональний символ із в -арну функцію ,
    • кожен -арний предикатний символ із в -арне відношення .

Припустимо  — функція, що відображає кожну змінну в деякий елемент із , яку і називатимемо підстановкою. Інтерпретація терму на відносно підстановки задається індуктивно:

  • , якщо  — змінна,

Подібним чином визначається істинність формул на відносно

  • , тоді і тільки тоді коли ,
  • , тоді і тільки тоді коли  — хибно,
  • , тоді і тільки тоді коли і істинні,'
  • , тоді і тільки тоді коли або істинно,
  • , тоді і тільки тоді коли з випливає ,
  • , тоді і тільки тоді коли для деякої підстановки , яка відрізняється від тільки на змінній ,
  • , тоді і тільки тоді коли для всіх підстановок , які відрізняються від тільки на змінній .

Формула , істинна на , що позначається , якщо , для всіх підстановок . Формула називається загальнозначимою, (позначається ), якщо для всіх моделей . Формула називається виконуваною , якщо хоча б для однієї .

Властивості[ред. | ред. код]

Коректність і повнота[ред. | ред. код]

Наведена вище система аксіом і правил виводу є коректною, тобто для будь-якої множини формул із випливає . Також дана система є повною: із випливає . Зокрема, з цих тверджень випливає, що для числення предикатів першого порядку загальнозначимі формули збігаються із теоремами формальної системи. Також у будь-якій теорії першого порядку всі виведені у ній формули збігаються з формулами, істинними в усіх моделях цієї теорії.

Компактність[ред. | ред. код]

Деяка множина формул є виконуваною тоді і тільки тоді, коли виконуваними є всі її скінченні підмножини.

Нерозв'язність[ред. | ред. код]

На відміну від логіки висловлень логіка першого порядку є нерозв'язною у разі наявності принаймні одного предиката арності не менше 2 (за винятком рівності), тобто немає ефективного методу визначення «існує чи не існує виведення деякої формули?» у певній теорії першого порядку.

Див. також[ред. | ред. код]

Література[ред. | ред. код]