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

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

Мова і синтаксис

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

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

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

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

Семантика

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

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

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

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

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

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

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

Властивості

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

Див. також

Джерела

  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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.