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

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

Ло́гіка другого́ поря́дку — у логіці є розширенням логіки першого порядку в якій допускаються змінні-функції і змінні-предикати, а також квантифікація над цими змінними. Дана логіка не спрощується до логіки першого порядку.

Мова і синтаксис[ред.ред. код]

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

  • Символи індивідуальних змінних, зазвичай \ x, y, z, x_1, y_1, z_1, x_2, y_2, z_2, і т.д.,
  • Символи функційних змінних \ F, G, H, F_1, G_1, H_1, F_2, G_2, H_2,. Кожній функційній змінній відповідає деяке додатне число — арність функції.
  • Символи предикатних змінних \ P, R, S, P_1, R_1, S_1, P_2, R_2, S_2,. Кожній предикатній змінній відповідає деяке додатне число — арність предикату.
  • Пропозиційні зв'язки: \lor,\land,\neg,\to,
  • Квантори: загальності \forall і існування \exists,
  • Службові символи: дужки і кома.

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

  • Терм — це символ змінної, або має вид \ f(t_1,\ldots,t_n), де \ f — функціональний символ арності \ n, а \ t_1,\ldots,t_n — терми або \ 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 — терми або \ P(t_1,\ldots,t_n), де P — предикатна змінна арності \ n, а \ t_1,\ldots,t_n — терми.
  • Формула — це або атом, або одна з наступних конструкцій: \neg A, (A_1\lor A_2), (A_1\land A_2), (A_1\to A_2), \forall x A, \exists x A, \forall F A, \exists F A, \forall P A, \exists P A, де \ A, A_1, A_2 — формули, а \ x, F, P — індивідуальна, функційна і предикатна змінні.

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

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

  • Базова множина \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}, кожну функційну змінну арності n в n-арну функцію \sigma(f):\mathcal{D}\times\ldots\times\mathcal{D}\rightarrow\mathcal{D} і кожну предикатну змінну арності n в n-арне відношення \sigma(p)\subseteq\mathcal{D}\times\ldots\times\mathcal{D}. Функцію s називатимемо також підстановкою. Інтерпретація [\![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) для функційного символа f
  • [\![f(x_1,\ldots,x_n)]\!]_s = s(f)(\![x_1]\!]_s,\ldots,\![x_n]\!]_s) для функційної змінної F

Подібним чином визначається істинність \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 P(t_1,\ldots,t_n), тоді і тільки тоді коли s(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 \exists F\, \phi, тоді і тільки тоді коли \mathcal{D}\models_{s'} \phi для деякої підстановки s', яка відрізняється від s тільки на функційній змінній F,
  • \mathcal{D}\models_s \exists P\, \phi, тоді і тільки тоді коли \mathcal{D}\models_{s'} \phi для деякої підстановки s', яка відрізняється від s тільки на предикатній змінній x,
  • \mathcal{D}\models_s \forall x\, \phi, тоді і тільки тоді коли \mathcal{D}\models_{s'} \phi для всіх підстановок s', які відрізняються від s тільки на індивідуальній змінній x,
  • \mathcal{D}\models_s \forall F\, \phi, тоді і тільки тоді коли \mathcal{D}\models_{s'} \phi для всіх підстановок s', які відрізняються від s тільки на функційній змінній F,
  • \mathcal{D}\models_s \forall P\, \phi, тоді і тільки тоді коли \mathcal{D}\models_{s'} \phi для всіх підстановок s', які відрізняються від s тільки на предикатній змінній P.

Формула \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}.

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

На відміну від логіки першого логіка другого порядку не має властивостей повноти і компактності. Також у цій логіці є невірним твердження теореми Ловенгейма—Сколема.

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

Джерела[ред.ред. код]

  1. Henkin, L. (1950). "Completeness in the theory of types". Journal of Symbolic Logic 15 (2): 81–91.
  2. Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
  3. Shapiro, S. (2000). Foundations without Foundationalism: A Case for Second-order Logic. Oxford University Press. ISBN 0-19-825029-0.
  4. Rossberg, M. (2004). "First-Order Logic, Second-Order Logic, and Completeness". in V. Hendricks et al., eds.. First-order logic revisited. Berlin: Logos-Verlag.
  5. Vaananen, J. (2001). "Second-Order Logic and Foundations of Mathematics". Bulletin of Symbolic Logic 7 (4): 504–520.