Ло́гіка другого́ поря́дку — у логіці є розширенням логіки першого порядку в якій допускаються змінні-функції і змінні-предикати, а також квантифікація над цими змінними. Дана логіка не спрощується до логіки першого порядку.
Мова і синтаксис Мови логіки другого порядку будуються на основі: множини функціональних символів і множини предикатних символів . З кожним функціональним і предикатним символом зв'язана арність (число аргументів). Крім того використовуються додаткові символи:
Символи індивідуальних змінних, зазвичай і т.д., Символи функційних змінних . Кожній функційній змінній відповідає деяке додатне число — арність функції. Символи предикатних змінних . Кожній предикатній змінній відповідає деяке додатне число — арність предикату. Пропозиційні зв'язки: , Квантори: загальності і існування , Службові символи: дужки і кома.
Перелічені символи разом із символами з і утворюють Алфавіт логіки першого порядку. Складніші конструкції визначаються індуктивно:
Терм — це символ змінної, або має вид , де — функціональний символ арності , а — терми або , де — функціональна змінна арності , а — терми. Атом — має вид , де — предикатний символ арності , а — терми або , де — предикатна змінна арності , а — терми. Формула — це або атом, або одна з наступних конструкцій: , де — формули, а — індивідуальна, функційна і предикатна змінні.
Семантика
У класичній логіці інтерпретація формул логіки другого порядку задається на моделі другого порядку, яка визначається такими даними:
Базова множина , Семантична функція , що відображає кожен -арний функціональний символ із в -арну функцію , кожен -арний предикатний символ із в -арне відношення .
Припустимо — функція, що відображає кожну індивідуальну змінну в деякий елемент із , кожну функційну змінну арності в -арну функцію і кожну предикатну змінну арності в -арне відношення . Функцію називатимемо також підстановкою. Інтерпретація терма на відносно підстановки задається індуктивно
, якщо — змінна, для функційного символу для функційної змінної
Подібним чином визначається істинність формул на відносно
, тоді і тільки тоді коли , , тоді і тільки тоді коли , , тоді і тільки тоді коли — хибно, , тоді і тільки тоді коли і істинні,' , тоді і тільки тоді коли або істинно, , тоді і тільки тоді коли з випливає , , тоді і тільки тоді коли для деякої підстановки , яка відрізняється від тільки на індивідуальній змінній , , тоді і тільки тоді коли для деякої підстановки , яка відрізняється від тільки на функційній змінній , , тоді і тільки тоді коли для деякої підстановки , яка відрізняється від тільки на предикатній змінній , , тоді і тільки тоді коли для всіх підстановок , які відрізняються від тільки на індивідуальній змінній , , тоді і тільки тоді коли для всіх підстановок , які відрізняються від тільки на функційній змінній , , тоді і тільки тоді коли для всіх підстановок , які відрізняються від тільки на предикатній змінній . Формула , істинна на , що позначається , якщо , для всіх підстановок . Формула називається загальнозначимою, (позначається ), якщо для всіх моделей . Формула називається виконуваною, якщо хоча б для однієї .
Властивості На відміну від логіки першого логіка другого порядку не має властивостей повноти і компактності. Також у цій логіці є невірним твердження теореми Ловенгейма—Сколема.
Див. також Логіка першого порядку Числення висловлень
Джерела Henkin, L. (1950). "Completeness in the theory of types". Journal of Symbolic Logic 15 (2): 81–91. Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0. Shapiro, S. (2000). Foundations without Foundationalism: A Case for Second-order Logic. Oxford University Press. ISBN 0-19-825029-0. Rossberg, M. (2004). "First-Order Logic, Second-Order Logic, and Completeness". in V. Hendricks et al., eds. First-order logic revisited. Berlin: Logos-Verlag. Vaananen, J. (2001). "Second-Order Logic and Foundations of Mathematics". Bulletin of Symbolic Logic 7 (4): 504–520.