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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

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

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

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

  • Символи змінних, зазвичай \ x, y, z, x_1, y_1, z_1, x_2, y_2, z_2, і т. д.,
  • Пропозиційні зв'язки: \lor,\land,\neg,\to,
  • Квантори: загальності \forall та існування \exists,
  • Службові символи: дужки і кома.

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

  • Терм — це символ змінної, або має вид \ f(t_1,\ldots,t_n), де \ f — функціональний символ арності \ n, а \ t_1,\ldots,t_n — терми.
  • Атом — має вид \ p(t_1,\ldots,t_n), де p — предикатний символ арності \ n, а \ t_1,\ldots,t_n — терми.
  • Формула — це або атом, або одна з наступних конструкцій: \neg F, (F_1\lor F_2), (F_1\land F_2), (F_1\to F_2), \forall x F, \exists x F, де \ F, F_1, F_2 — формули, а \ x — змінна.

Змінна \ x називається зв'язаною в формулі \ F, якщо \ F має вид \forall x G або \exists x G, або може бути представлена в одній з форм \neg H, (F_1\lor F_2), (F_1\land F_2), (F_1\to F_2), причому \ x вже зв'язана в H, F_1 і F_2.

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

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

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

  1. (A \to (B \to C))
  2. ((A \to (B \to C)) \to ((A \to B) \to (A \to C)))
  3. ((\neg A \to \neg B) \to (B \to A))
  4. \forall x A \to A[t/x],
  5. \forall x (A \to B)\to (A \to \forall x B), якщо x\; не присутній в A\; в незвязаному стані

У четвертій аксіомі A[t/x]\; — формула, одержана внаслідок підстановки терма t\; замість змінної x в формулі A\;. Підстановка деякого терма замість змінної можлива не в усіх випадках. Умови існування такої підстановки та її результат можна визначити індуктивно.

  • Якщо A — атомарна формула, то терм t\; може замінити довільну змінну x\; цієї формули. Результат позначається A[t/x]\;.
  • Якщо A\; має вигляд \lnot B тоді підстановка t\; замість x\; можлива лише тоді, коли така підстановка можлива для формули  B\; і A[t/x]\; тоді дорівнює \lnot B[t/x].
  • Якщо A має вигляд B \to C, тоді підстановка t\; замість x\; можлива лише тоді, коли така підстановка можлива для формул  B\; і C.\; A[t/x]\; тоді рівна B[t/x] \to C[t/x].
  • Якщо A\; має вигляд \forall y B, тоді підстановка t\; замість x\; можлива у двох випадках:
    • Змінна x\; зустрічається у формулі  B\; лише у зв'язаному стані.
    • змінна y\; не зустрічається у термі t\; і підстановка t\; замість x\; можлива у формулі  B.\; Тоді результат визначається наступним чином:
    • Якщо x\; дорівнює y, то A[t/x]\; дорівнює \forall y B
    • Якщо x\; не дорівнює y\;, то A[t/x]\; дорівнює \forall y B[t/x]

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

  • Modus ponens:
    \frac{A, A \to B}{B}
  • Правило узагальнення (GEN):
    \frac{A}{\forall x A}

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

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

  • (A \lor B) позначає (\lnot (A \to (\lnot B)))
  • (A \land B) позначає ((\lnot A) \to B)
  • (\exists x A) позначає (\lnot \forall x (\lnot A))

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

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

Нехай \Sigma\; деяка множина формул мови першого порядку, а A\; — деяка задана формула. Тоді кажуть, що формула A\; виводиться з множини формул \Sigma\; (позначається \Sigma \vdash A), якщо існує така скінченна послідовність формул A_1, A_2 \ldots A_n = A, де для кожної формули A_i\;:

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

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

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

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

Доведемо, що A, (\forall x A to B) \vdash \forall x B

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

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

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

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

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

  1. \forall x \forall y \forall z (x\circ (y\circ z)=(x\circ y)\circ z) (асоціативність)
  2. \forall x (e \circ x= x (властивість нейтрального елемента)
  3. \forall x \exists y (x \circ y = e) (існування оберненого елемента)
  4. \forall x  (x = x) (рефлексивність рівності)
  5. \forall x \forall y (x = y \to y = x) (симетричність рівності)
  6. \forall x \forall y \forall z (x = y \to (y = z \to x = z)) (транзитивність рівності)
  7. \forall x \forall y \forall z (x = y \to (z \circ x = z \circ y \land  x \circ z = y \circ z)) (підстановка рівності)

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

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

\forall x \forall y (x \circ y = y \circ x)

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

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

  • Базова множина \mathcal{D},
  • Семантична функція \sigma, що відображає
    • кожен n-арний функціональний символ f із \mathcal{F} в n-арну функцію \sigma(f):\mathcal{D}\times\ldots\times\mathcal{D}\rightarrow\mathcal{D},
    • кожен n-арний предикатний символ p із \mathcal{P} в n-арне відношення \sigma(p)\subseteq\mathcal{D}\times\ldots\times\mathcal{D}.

Припустимо s — функція, що відображає кожну змінну в деякий елемент із \mathcal{D}, яку і називатимемо підстановкою. Інтерпретація [\![t]\!]_s терма t на\mathcal{D} відносно підстановки s задається індуктивно:

  • [\![x]\!]_s = s(x), якщо x — змінна,
  • [\![f(x_1,\ldots,x_n)]\!]_s = \sigma(f)(\![x_1]\!]_s,\ldots,\![x_n]\!]_s)

Подібним чином визначається істинність \models_s формул на \mathcal{D} відносно s

  • \mathcal{D}\models_s p(t_1,\ldots,t_n), тоді і тільки тоді коли \sigma(p)( \![x_1]\!]_s,\ldots,\![x_n]\!]_s),
  • \mathcal{D}\models_s \neg\phi, тоді і тільки тоді коли \mathcal{D}\models_s \phi — хибно,
  • \mathcal{D}\models_s \phi\land\psi, тоді і тільки тоді коли \mathcal{D}\models_s \phi і \mathcal{D}\models_s \psi істинні,'
  • \mathcal{D}\models_s \phi\lor\psi, тоді і тільки тоді коли \mathcal{D}\models_s \phi або \mathcal{D}\models_s \psi істинно,
  • \mathcal{D}\models_s \phi\to\psi, тоді і тільки тоді коли з \mathcal{D}\models_s \phi випливає \mathcal{D}\models_s \psi,
  • \mathcal{D}\models_s \exists x\, \phi, тоді і тільки тоді коли \mathcal{D}\models_{s'} \phi для деякої підстановки s', яка відрізняється від s тільки на змінній x,
  • \mathcal{D}\models_s \forall x\, \phi, тоді і тільки тоді коли \mathcal{D}\models_{s'} \phi для всіх підстановок s', які відрізняються від s тільки на змінній x.

Формула \phi, істинна на \mathcal{D}, що позначається \mathcal{D}\models \phi, якщо \mathcal{D}\models_s \phi, для всіх підстановок s. Формула \phi називається загальнозначимою, (позначається \models \phi), якщо \mathcal{D}\models \phi для всіх моделей \mathcal{D}. Формула \phi називається виконуваною , якщо \mathcal{D}\models \phi хоча б для однієї \mathcal{D}.

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

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

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

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

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

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

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

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

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

  • Гильберт Д., Аккерман В. Основы теоретической логики. М., 1947
  • Клини С. К. Введение в метаматематику. М., 1957
  • Мендельсон Э. Введение в математическую логику. М., 1976
  • Новиков П. С. Элементы математической логики. М., 1959
  • Черч А. Введение в математическую логику, т. I. М. 1960
  • «Філософський словник» / За ред. В. І. Шинкарука. — 2.вид., перероб. і доп. — К.: Голов. Ред. УРЕ, 1986.