Логика первого и второго порядка

[EminentVictorians]

Хочу для общего развития разобраться, в чем разница между логикой первого порядка и второго порядка. В википедии написано, что "логика второго порядка допускает также квантификацию предикатов и функциональных символов (над множествами)". Далее там же приводится пример формулы из логики второго порядка: ${\displaystyle \forall P((0\in P\land \forall i(i\in P\to i+1\in P))\to \forall n(n\in P))}$. Я эту формулу понимаю следующим образом: "какое бы множество мы ни взяли, если оно индуктивно, значит оно содержит натуральные числа". Вот это словосочетание "какое бы множество мы ни взяли", как я понял, законно только в логике второго порядка (т.к. она допускает кванторы по множествам). Потом я вспомнил, что $ZFC$ является теорией первого порядка. Но ведь в ней тоже можно вроде бы брать кванторы по множествам, разве нет? А эти 2 вещи как-то не увязываются вместе. В общем, помогите разобраться, что к чему.

[mihaild]

В ZF можно писать кванторы по объектам теории. Никто не гарантирует, что все "настоящие" множества в нашей модели присутствуют.
Стандартный пример: добавьте к ZF константу $c$ и аксиомы "$c$ лежит в любом индуктивном множестве", "$c \neq 0$", "$c \neq 1$", "$c \neq 2$" и т.д. У получившейся теории есть модель, но в этой модели нет "обычного" множества $0, 1, \ldots$.

[EminentVictorians]

mihaild в сообщении #1558586 писал(а):

В ZF можно писать кванторы по объектам теории.

Я хочу формализовать такое рассуждение: "Пусть $X$ - множество. Рассмотрим его булеан $2^X$. Для любого $m \in 2^X$ выполняется свойство $\varphi(x)$." У меня получится записать это в $ZFC$? Булеан - это множество (по аксиоме булеана), а значит я связал квантором переменную, значения которой множества, т.е. объекты теории. Вроде все в порядке.

mihaild в сообщении #1558586 писал(а):

Никто не гарантирует, что все "настоящие" множества в нашей модели присутствуют.

А о какой модели речь? Просто я не понял, когда модель появилась и какая. Пока вроде все в рамках строчек формальной системы происходит.

[mihaild]

EminentVictorians в сообщении #1558588 писал(а):

У меня получится записать это в $ZFC$?

Да. Собственно чтобы это записать и аксиомы не очень нужны, они понадобятся, чтобы сказать, почему записано то, что хотелось.
Ваше утверждение записывается примерно так $\forall y ((\forall z(z \subseteq x \leftrightarrow z \in y)) \rightarrow (\forall z(z \in y \rightarrow \varphi(x))))$. Где $a \subseteq b$ это сокращение для $\forall c (c \in a \rightarrow c \in b)$, где $c$ не входит в формулу.

EminentVictorians в сообщении #1558588 писал(а):

А о какой модели речь?

О модели ZFC.

В рамках строчек разница в том, что в теории первого порядка все кванторы одного вида, а в теории второго порядка - двух. Дальше, чтобы говорить, что дает второй вид кванторов, нужна интерпретация. И в ней окажется, что, например, квантор по всем предикатам включает, в том числе, тождественную истину (соответствует "множеству" всех множеств).

[EminentVictorians]

mihaild, у меня проблема вот какая. Я читал, что язык логики первого порядка менее выразителен, чем язык логики второго порядка. Ну я подумал, что в принципе это логично, т.к. логика второго порядка допускает высказывания с кванторами по свойствам, а логика первого порядка - нет. Но потом я захотел увидеть конкретное рассуждение, которое формализуется в логике второго порядка и не формализуется в логике первого порядка. И не придумал ни одного. Вот и вопрос в связи с этим: что дает логика второго порядка по сравнению с логикой первого порядка?

-- 27.06.2022, 00:27 --

Под рассуждением я, конечно же, имею в виду математическое рассуждение. Желательно какое-нибудь базовое и не слишком сложное.

[mihaild]

С рассуждениями в логике второго порядка всё гораздо сложнее (нет полных эффективных дедуктивных систем - если в логике первого порядка есть правила вывода, по которым можно вывести любое утверждение, выполненное во всех моделях, то для логики второго порядка так не получится).

Выразительность языка определяется тем, что на нём можно описать. Например на языке первого порядка нельзя описать стандартную модель натуральных чисел, а на языке второго - можно.

[EminentVictorians]

mihaild в сообщении #1558599 писал(а):

Например на языке первого порядка нельзя описать стандартную модель натуральных чисел, а на языке второго - можно.

Т.е. логика первого порядка слишком слаба, чтобы категоричным образом определить натуральные числа, так можно сказать?

[mihaild]

EminentVictorians в сообщении #1558619 писал(а):

Т.е. логика первого порядка слишком слаба, чтобы категоричным образом определить натуральные числа, так можно сказать?

Да.
Правда заметьте, что тут опять не чисто синтаксическое утверждение получается, а нужно привлекать семантику. И собственно у логики второго порядка есть две семантики - стандартная и Хенкина. И логика второго порядка с семантикой Хенкина - это просто немного спрятанная логика первого порядка, в ней есть компактность, но скажем в арифметике второго порядка с семантикой Хенкина нет категоричности.

[EminentVictorians]

mihaild, Вы простите, что я Вас вопросами заваливаю, просто для меня все это слишком ошеломительные факты. Этот факт о некатегоричности арифметики выглядит очень не в пользу логики первого порядка. Разве он не должен окончательно и бесповоротно ее похоронить?

[svv]

EminentVictorians в сообщении #1558665 писал(а):

Этот факт о некатегоричности арифметики выглядит очень не в пользу логики первого порядка. Разве он не должен окончательно и бесповоротно ее похоронить?

Предлагаю пожертвовать арифметикой.

[Nemiroff]

EminentVictorians в сообщении #1558665 писал(а):

Разве он не должен окончательно и бесповоротно ее похоронить?

Её -- это арифметику или логику? Впрочем арифметику не за что: некатегорично вообще почти всё.
В любом случае, отказаться от логики первого порядка сложно: логика делалась в том числе для получения проверяемых и автоматических доказательств. Рекурсивная неперечислимость не позволяет сделать в логике второго порядка "приличные" доказательства.
А ещё без теоремы о компактности жизнь не мила.

Ради категоричности теории заменять логику первого порядка на логику второго порядка -- это себя обманывать.

[EminentVictorians]

Nemiroff в сообщении #1558670 писал(а):

Её -- это арифметику или логику?

Логику первого порядка.

Арифметикой жертвовать жалко. Я лично считаю, что все люди, которые поняли, что такое натуральные числа, поняли их одинаковым образом. Я не представляю, как интуиция на счет натуральных чисел может быть разной у разных людей (хотя Вы говорили, что может. Если расскажете почему - прочитаю с большим интересом). Иными словами, я считаю категоричность натуральных чисел надежно установленным фактом. И когда что-то с ним не соотносится, то для меня это большой звоночек. Тем более, когда это логика первого порядка, про которую заведомо известно, что она ограничена в выразительных средствах.

[Nemiroff]

К сожалению, никакая "приличная" логика не может выделить истины из "категоричных натуральных чисел". У вас четыре варианта.
1) Ваша логическая система доказывает всё, что нужно о натуральных числах, но и ещё и что-то, что не нужно -- это самый плохой случай.
2) Вы гвоздями прибили "моя логическая система содержит все истины о натуральных числах и только их" -- это возможно. Но получившаяся система аксиом неперечислима, а поэтому её нельзя написать.
3) Вы сказали "нет, я буду использовать логику второго порядка, в ней я явно указываю, что такое натуральные числа". Да, указываете, но такая система не может доказывать теоремы -- потому что для неё нет приличной системы доказательства.
4) Вы взяли перечислимую систему аксиом с понятной теорией доказательства. По дороге вы рассыпали аксиомы, так что теперь ваша аксиоматика описывает нечто, что уже не всегда похоже на ваше исходное понятие о натуральных числах.

По поводу категоричности натуральных чисел в логике второго порядка вот ещё что: эта категоричность "философски ненастоящая". Для определения логики второго порядка вам нужно некоторое понятие о теории множеств -- мета-теория, если хотите. Можно взять ZFC. В этой мета-теории, конечно, будет категоричность -- но сама мета-теория некатегорична.

[EminentVictorians]

Верно ли я понимаю, что когда я доказываю обычным образом (не в формальном смысле, а просто как обычно делают в математике - с помощью естественного языка и обычных нормальных рассуждений) какие-то теоремы о натуральных числах, то я пользуюсь гораздо более сильными выразительными средствами, чем те, которые допускаются логикой первого порядка?

[mihaild]

На это есть разные взгляды, недавно что-то похожее обсуждалось в «Освоение математики фундаментально и для практики».