Оцените «мощь» логики второго порядка на примере

[migmit]

epros в сообщении #608719 писал(а):

migmit в сообщении #608672 писал(а):

Ничего не понял. Кто принял, когда?

Я. Уже много дней назад.

Где?

epros в сообщении #608719 писал(а):

Я не спрашивал строится оно или выращивается в оранжерее. Я спросил константа это или нет.

В сигнатуре общепринятых теорий его нет.

epros в сообщении #608719 писал(а):

Пурга, которую Вы сейчас несёте, воистину удивительна. Сами-то себя послушайте: Вы сейчас мне доказываете, что не можете проверить синтаксическую корректность предложения $\forall x ~ S(x)=0$, не имея всей теории целиком (а имея только язык).

Отнюдь. Не имея языка - не могу. Имея язык, но не имея теории - могу.

epros в сообщении #608719 писал(а):

migmit в сообщении #608672 писал(а):

Да нет, именно что тащите. "Свойство" - это, по-вашему, не семантика?

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

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

[epros]

migmit в сообщении #608948 писал(а):

В сигнатуре общепринятых теорий его нет.

Не бывает никакой "сигнатуры общепринятых теорий". Есть описание синтаксиса языка логики первого порядка (или второго порядка). И согласно этому описанию константы могут использоваться.

Да, у конкретных теорий есть свои ограничения на синтаксис, называются "сигнатурой теории". Но речь не о конкретных теориях.

migmit в сообщении #608948 писал(а):

Отнюдь. Не имея языка - не могу. Имея язык, но не имея теории - могу.

Я уже несколько раз повторил, что речь о языке исчисления предикатов (логики первого порядка или второго порядка). Вы просто не желаете ничего слышать.

migmit в сообщении #608948 писал(а):

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

Против слова у меня никаких "бурных возражений" нет. Если Вы будете использовать его как синоним понятия свойства - пожалуйста. Возражения у меня будут, если бы будете под этим понятием подразумевать какую-то аксиоматику.

migmit в сообщении #608948 писал(а):

Где?

Наверное, пора прекращать этот бессмысленный спор. Ибо Вы не только не хотите слышать то, что неоднократно было сказано, но, оказывается, очень уж легко через некоторое время "забываете" и то, что казалось бы услышали.

[migmit]

epros в сообщении #608957 писал(а):

Не бывает никакой "сигнатуры общепринятых теорий". Есть описание синтаксиса языка логики первого порядка (или второго порядка). И согласно этому описанию константы могут использоваться.

Конечно. Входящие в сигнатуру рассматриваемой теории.

epros в сообщении #608957 писал(а):

Да, у конкретных теорий есть свои ограничения на синтаксис, называются "сигнатурой теории". Но речь не о конкретных теориях.

Тогда говорить вообще не о чем.

epros в сообщении #608957 писал(а):

migmit в сообщении #608948 писал(а):

Отнюдь. Не имея языка - не могу. Имея язык, но не имея теории - могу.

Я уже несколько раз повторил, что речь о языке исчисления предикатов (логики первого порядка или второго порядка). Вы просто не желаете ничего слышать.

Тогда ваша формула проваливает проверку на синтаксическую корректность.

epros в сообщении #608957 писал(а):

migmit в сообщении #608948 писал(а):

Где?

Наверное, пора прекращать этот бессмысленный спор. Ибо Вы не только не хотите слышать то, что неоднократно было сказано, но, оказывается, очень уж легко через некоторое время "забываете" и то, что казалось бы услышали.

Казалось бы, до чего просто привести ссылку, благо топик небольшой.

[epros]

migmit в сообщении #608964 писал(а):

Тогда говорить вообще не о чем.

Разговор изначально был про тавтологии. А это, знаете ли, по определению то самое, что ни от каких конкретных теорий не зависит.

migmit в сообщении #608964 писал(а):

Тогда ваша формула проваливает проверку на синтаксическую корректность.

С какой стати?

migmit в сообщении #608964 писал(а):

Казалось бы, до чего просто привести ссылку, благо топик небольшой.

А прочитать первое сообщение темы было слабо? Там было прямо сказано о том, что синтаксически под «всемогущим» подразумевается свойство.

[migmit]

epros в сообщении #608968 писал(а):

migmit в сообщении #608964 писал(а):

Тогда ваша формула проваливает проверку на синтаксическую корректность.

С какой стати?

Она использует символ, отсутствующий в языке.

epros в сообщении #608968 писал(а):

А прочитать первое сообщение темы было слабо? Там было прямо сказано о том, что синтаксически под «всемогущим» подразумевается свойство.

Какое?

[Someone]

epros, Вы странные вещи говорите. Да, в логике второго порядка можно ссылаться на свойства, как на объекты. Пока Вы не имеете в виду какое-то конкретное свойство. Совокупность объектов-свойств образует некий универсум свойств. Как только Вы заикаетесь насчёт конкретного "свойства", сразу же возникает вопрос: а есть ли в этом универсуме свойство, о котором Вы говорите? Если нужное свойство возможно определить в языке теории, то всё хорошо. Если невозможно - увы, такого свойства может и не быть, и ссылаться на него нельзя.

[epros]

migmit в сообщении #609020 писал(а):

Она использует символ, отсутствующий в языке.

В каком языке? Описание языка исчисления предикатов первого порядка говорит нам, что использование функциональных символов допустимо. И синтаксический анализатор, который написан для распознавания корректности предложений языка исчисления предикатов (для любой теории) распознает $S$ как допустимый функциональный символ. Что Вам ещё нужно?

Другое дело, если мы спросим у синтаксического анализатора, является ли это предложением теории множеств. Тогда он ответит "нет" - именно потому, что в сигнатуре теории множеств нет функциональных символов.

migmit в сообщении #609020 писал(а):

Какое?

Что "какое"? Все вопросы про то, что означает константа, относятся к семантике. В рамках анализа синтаксиса мы можем говорить только о том, что в предложении упомянуто свойство "всемогущий". "Какое" оно - мы не знаем.

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

И это неочевидное на первый вгляд различие между логиками, в частности, порождает вполне конкретные различия в доказательных возможностях арифметик первого и второго порядков. (Для Someone: Что Вы скажете относительно этого?)

[Munin]

По-моему, вся тема высосана из пальца. epros-у просто почему-то не нравится логика второго порядка. Например, чего-то недопонял, недоучил, или просто пока учил - неприятно было, трудно. Общеизвестно, что логика второго порядка сложнее, глубже и содержательнее, чем первого (и вообще, чем больше порядок, тем больше эти качества). Но epros хочет убедить окружающих в обратном, чтобы все разделяли его отрицательные чувства по отношению к ней. Вот он и выдумал пример, а потом начал выдумывать аргументацию (всё сплошь словесную), пытаясь продвигать свою позицию.

[Xaositect]

epros в сообщении #609036 писал(а):

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

Это неверно. Подставлять можно только то, что выразимо в языке логики второго порядка как терм второго порядка.

[epros]

Xaositect в сообщении #609054 писал(а):

Это неверно. Подставлять можно только то, что выразимо в языке логики второго порядка как терм второго порядка.

Ну, я согласен с таким уточнением. Но константа это ведь тоже терм?

[Xaositect]

epros в сообщении #609060 писал(а):

Ну, я согласен с таким уточнением. Но константа это ведь тоже терм?

Разумеется.

[epros]

Munin в сообщении #609052 писал(а):

Вот он и выдумал пример

Ха. У Шапиро есть более содержательный пример: про свойство "иметь промежуточную кардинальность между счётной и континуумом". Вывод тот же самый: объект с таким свойством либо есть, либо нет. Причём и в том (объект есть), и в другом (объекта нет) случаях имеем недоказуемую тавтологию. Блеск. Отличие от моего примера состоит в том, что это свойство:
1) Выразимо формулой исчисления предикатов второго порядка.
2) Существование и единственность оного свойства доказуемы.

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

[Munin]

Неважно. Важно, что спор из ложной посылки.

[epros]

epros в сообщении #609036 писал(а):

любое свойство, независимо от того, выразимо ли оно какой-либо формулой какого-либо языка или нет.

epros в сообщении #609067 писал(а):

1) Выразимо формулой исчисления предикатов второго порядка.

Во избежание недопонимания поясню на пример, что я имею в виду под "выразимостью формулой языка". Вот, скажем, свойство натурального числа "быть чётным" выразимо формулой арифметики:

$\exists y ~ S(S(0)) \times y = x$.

Это - формула с одной свободной переменной $x$. Это значит, что если нам лень каждый раз вместо упоминания свойства "чётное" писать эту формулу, то мы вводим в сигнатуру теории предикатный символ $\operatorname{isEven}$ и определяем его следующей дополнительной аксиомой:

$\forall x ~ \operatorname{isEven}(x) \leftrightarrow \exists y ~ S(S(0)) \times y = x$.