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

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

Мова і синтаксисРедагувати

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

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

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

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

СемантикаРедагувати

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

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

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

  •  , якщо   — змінна,
  •   для функційного символу  
  •   для функційної змінної  

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

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

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

ВластивостіРедагувати

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

Див. такожРедагувати

ДжерелаРедагувати

  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.