imported>NapalmBot: Декодирование ссылок по запросу stjn

2024-03-31T12:22:14Z

Декодирование ссылок по запросу stjn

Новая страница

'''Логика второго порядка''' в [[Математическая логика|математической логике]] — [[формальная система]], расширяющая [[Логика первого порядка|логику первого порядка]]<ref>Shapiro (1991) and Hinman (2005) give complete introductions to the subject, with full definitions.</ref> возможностью [[Квантор всеобщности|квантификации общности]] и [[Квантор существования|существования]] не только над переменными, но и над [[предикат]]ами и функциональными символами. Логика второго порядка несводима к логике первого порядка. В свою очередь, она расширяется [[Логика высшего порядка|логикой высших порядков]] и [[Теория типов|теорией типов]].

== Язык и синтаксис ==
[[Формальный язык|Формальные языки]] логики второго порядка строятся на основе множества функциональных символов <math>\mathcal{F}</math> и множества [[предикат]]ных символов <math>\mathcal{P}</math>. С каждым функциональным и предикатным символом связана [[арность]] (число аргументов). Также используются дополнительные символы

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

Перечисленные символы вместе с символами <math>\mathcal{P}</math> и <math>\mathcal{F}</math> образуют алфавит логики первого порядка. Более сложные конструкции определяются [[Математическая индукция|индуктивно]].

* [[Терм (логика)|Терм]] — это символ индивидуальной переменной, либо выражение, которое имеет вид <math>\ f(t_1,\ldots,t_n)</math>, где <math>\ f</math> — функциональный символ арности <math>\ n</math>, а <math>\ t_1,\ldots,t_n</math> — термы либо выражение вида <math>\ F(t_1,\ldots,t_n)</math>, где <math>\ F</math> — функциональная переменная арности <math>\ n</math>, а <math>\ t_1,\ldots,t_n</math> — термы.
* Атом — имеет вид <math>\ p(t_1,\ldots,t_n)</math>, где <math>p</math> — предикатный символ арности <math>\ n</math>, а <math>\ t_1,\ldots,t_n</math> — термы или <math>\ P(t_1,\ldots,t_n)</math>, где <math>P</math> — предикатная переменная арности <math>\ n</math>, а <math>\ t_1,\ldots,t_n</math> — термы.
* Формула — это или атом, или одна из следующих конструкций: <math>\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</math>, где <math>\ A, A_1, A_2</math> — формулы, а <math>\ x, F, P</math> — индивидуальная, функциональная и предикатная переменные. (Конструкции <math>\forall F A, \exists F A, \forall P A, \exists P A</math> являются формулами второго и не [[Логика первого порядка|первого порядка]]).

== Аксиоматика и доказательство формул ==
{{В планах|посвящён=[[Логика первого порядка#Аксиоматика и доказательство формул|аксиоматике и правилам вывода]]|дата=2013-10-13}}

== Семантика ==
В классической логике интерпретация формул логики второго порядка задаётся на модели второго порядка, которая определяется следующими данными.

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

== Свойства ==
В отличие от логики первого порядка, логика второго порядка не имеет свойств [[Формальная система#Полнота|полноты]] и [[компактность|компактности]]. Также в этой логике является неверным утверждение [[Теорема Лёвенгейма — Скулема|теоремы Лёвенгейма — Скулема]].

== Примечания ==
{{примечания}}

== Литература ==
# 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.

{{вс}}
{{Логика}}
[[Категория:Математическая логика]]

Логика второго порядка - История изменений

imported>NapalmBot: Декодирование ссылок по запросу stjn