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

[epros]

Пример утверждения, являющегося тавтологией второго порядка, таков:
«Всемогущий либо существует, либо не существует».

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

$\forall X ~ [\exists x ~ X(x) \vee \nexists x ~ X(x)]$.

В переводе с закорючек на русский язык сие звучит так: «Для любого свойства обладающий им объект либо существует, либо не существует». Понимаете: «любое» - значит включая и противоречивым образом или вообще никак не определённые свойства. Достаточно того, чтобы синтаксически это было «свойством». Значит, берём свойство «всемогущества» и, особо не задумываясь над его определением, формулируем вышеозначенное утверждение, кое является «истиной в конечной инстанции во всех интерпретациях».

Продемонстрировать тавтологичность указанной выше формулы даже для противоречивым образом определённых свойств нетрудно. Допустим, что у нас есть некое определение свойства, которое записано некой формулой $\varphi(X)$ (из того, что свободная переменная обозначена большой буквой, видно, что она обозначает свойство). Рассмотрим утверждение, ограниченое указанным определением:

$\forall X ~ \varphi(X) \to [\exists x ~ X(x) \vee \nexists x ~ X(x)]$.

Рассмотрим пример противоречивого определения свойства:

$\varphi(X) \equiv \nexists Y \forall x ~ Y(x) \leftrightarrow X(x)$

Такого свойства просто не может существовать - это бы породило парадокс. Но это значит, что при подстановке любого свойства в формулу, мы получим ложный $\varphi(X)$, а значит - истинную импликацию.

Ну а раз при любом определении $\varphi(X)$ импликация остаётся истинной, значит можно определить:

$\varphi(X) \equiv \top$, т.е. вместо конкретного определения свойства $X$ просто сказать, что любое свойство нам подходит.

Вот такая она, логика второго порядка: Оказывается, она где-то внутри себя знает правильный ответ на вопрос о существовании «Всемогущего» (правда нам его не говорит). И это не смотря на то, что мы не знаем корректного определения всемогущества. Бедные агностики...

[migmit]

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

Понимаете: «любое» - значит включая и противоречивым образом или вообще никак не определённые свойства.

Не значит.

[epros]

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

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

Понимаете: «любое» - значит включая и противоречивым образом или вообще никак не определённые свойства.

Не значит.

Значит, значит. Будьте внимательнее: противоречивость не позволяет утверждать существование такого свойства. Но это не запрещает формулировать в отношении него утверждение о том, что такой объект «либо есть, либо нет».

-- Ср авг 15, 2012 21:16:11 --

Кстати, классический пример, иллюстрирующий неполноту логики второго порядка, который приводит Шапиро, по-сути ничем не отличается (хотя он не из области «теологии», а из «чистой» математики). Он пишет, что предложением логики второго порядка можно выразить гипотезу континуума, которая «либо истина, либо ложна», но ни доказать, ни опровергнуть этого нельзя. Так вот, это — про свойство «иметь промежуточную кардинальность между счётной и континуальной»: утверждается, что объект с таким свойством «либо существует, либо нет». Не вижу большой разницы со свойством «всемогущества».

[migmit]

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

Значит, значит. Будьте внимательнее: противоречивость не позволяет утверждать существование такого свойства. Но это не запрещает формулировать в отношении него утверждение о том, что такой объект «либо есть, либо нет».

Я про противоречивые не говорю. Я говорю про неопределённые.

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

Он пишет, что предложением логики второго порядка можно выразить гипотезу континуума, которая «либо истина, либо ложна», но ни доказать, ни опровергнуть этого нельзя. Так вот, это — про свойство «иметь промежуточную кардинальность между счётной и континуальной»: утверждается, что объект с таким свойством «либо существует, либо нет». Не вижу большой разницы со свойством «всемогущества».

Разницу между строго определённым свойством и болтовнёй не видите?

[epros]

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

Я про противоречивые не говорю. Я говорю про неопределённые.

Ещё раз: подстановка любого свойства в формулу происходит чисто синтаксически, никто не требует проверки его определения.

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

Разницу между строго определённым свойством и болтовнёй не видите?

Я вижу, что в данном случае её определённо нет. Вы доказали, что у свойства «всемогущества» и не может быть никакого строгого определения? О какой тогда болтовне Вы говорите? А может быть это свойство подразумевает под собой определение не хуже, чем какое-нибудь определение недостижимой кардинальности в теории множеств? А чем «строго определённое» свойство «иметь промежуточную кардинальность» лучше? Просто нафантазировали некое множество аксиом, оное свойство определяющих, вот и всё. Ну, допустим, что никто пока не продемонстрировал их противоречивости, зато продемонстрировали их независимость от других аксиом. Ну и что? Суть-то в том, что при подстановке свойства в тавтологию никто никаких проверок его определения от нас не требует, ибо это - чисто синтаксическая операция.

По моим понятиям, утверждение о том, что логика «знает ответ» на гипотезу континуума - это такая же шиза, как утверждение о том, что она знает ответ на вопрос о существовании «Всемогущего».

[Munin]

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

Вот такая она, логика второго порядка: Оказывается, она где-то внутри себя знает правильный ответ на вопрос о существовании «Всемогущего» (правда нам его не говорит).

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

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

[epros]

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

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

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

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

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

Правильный ответ - это выбор из «да» или «нет».

Поясню. Допустим, свойство определяется формулой языка $\varphi(X)$. Тогда утверждение о существовании объекта с таким свойством формализуется так:

$\forall X ~ \varphi(X) \to \exists x ~ X(x)$.

Утверждение о несуществовании, соответственно, так:

$\forall X ~ \varphi(X) \to \nexists x ~ X(x)$.

Если свойство определено противоречиво, то $\nexists X ~ \varphi(X)$, а значит оба утверждения истинны. Но дизъюнкция этих утверждений - тавтология, т.е. по крайней мере одно из них должно быть истинным. Тьфу, неточность: дизъюнкция, конечно, не ЭТИХ утверждений, а тех утверждений о существовании, которые стоят внутри импликации.

[Munin]

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

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

Вы перепутали некое свойство со своим. Я не о свойстве $X(x),$ а о свойстве $\exists x\,X(x)\vee\nexists x\,X(x).$

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

Правильный ответ - это выбор из «да» или «нет».

При чём здесь это?

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

Тогда утверждение о существовании объекта с таким свойством

Нет, интересует утверждение о непротиворечивости свойства.

[epros]

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

Вы перепутали некое свойство со своим. Я не о свойстве $X(x),$ а о свойстве $\exists x\,X(x)\vee\nexists x\,X(x).$

Тогда я не понимаю, что Вы хотели сказать. Вопрос состоял в том: «Существует ли Всемогущий?» Ответ на него может быть «да» или «нет». Об этом и говорит логика. Т.е. она утверждает, что никакие иные ответы неприемлемы, в частности, нельзя ответить, что понятие всемогущества не определенно, бессмысленно и т.п.

В каком смысле ответ может удовлетворять какому-то свойству? Кстати, $\exists x\,X(x)\vee\nexists x\,X(x)$ - это не свойство, а просто какая-то формула. У свойств в качестве аргументов подразумеваются объекты.

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

интересует утверждение о непротиворечивости свойства

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

[migmit]

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

Ещё раз: подстановка любого свойства в формулу происходит чисто синтаксически, никто не требует проверки его определения.

Проверки— не требует, а НАЛИЧИЯ — требует. Иначе у вас формулы не получится.

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

Я вижу, что в данном случае её определённо нет.

Гм. Могу лишь посоветовать протереть очки.

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

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

Ну, вот об этой например. Свойства "всемогущество" НЕ СУЩЕСТВУЕТ, пока не предъявлено определение. Мне всё равно, каким оно будет — об определениях договариваются, а не "доказывают".

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

Просто нафантазировали некое множество аксиом, оное свойство определяющих, вот и всё. Ну, допустим, что никто пока не продемонстрировал их противоречивости, зато продемонстрировали их независимость от других аксиом. Ну и что? Суть-то в том, что при подстановке свойства в тавтологию никто никаких проверок его определения от нас не требует, ибо это - чисто синтаксическая операция.

Ещё раз, для альтернативно одарённых. Никто не требует ПРОВЕРОК определения, требуется НАЛИЧИЕ.

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

По моим понятиям, утверждение о том, что логика «знает ответ» на гипотезу континуума - это такая же шиза, как утверждение о том, что она знает ответ на вопрос о существовании «Всемогущего».

Конечно. Логика вообще ничего не знает, у неё мозгов нет.

-- Чт авг 16, 2012 23:10:32 --

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

Вопрос состоял в том: «Существует ли Всемогущий?» Ответ на него может быть «да» или «нет». Об этом и говорит логика.

(Оффтоп)

Вы перестали бить свою жену?

Логика ничего подобного не утверждает. Логика вообще не занимается несформулированными вопросами.

[epros]

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

Проверки— не требует, а НАЛИЧИЯ — требует. Иначе у вас формулы не получится.

Нет, нет, нет. Всё, что требуется, - это наличие у свойства имени собственного. Это уже позволяет применить правило подстановки данного имени вместо переменной $X$. Это - чисто синтаксическая операция. Не путайте это с проверкой определения (ибо проверка НАЛИЧИЯ определения - это тоже проверка). Определение формируется множеством аксиом, до которых мы может быть пока просто не добрались.

Другое дело, что ЕСЛИ свойство определено противоречиво или неоднозначно, то присвоение ему имени собственного автоматически делает теорию противоречивой. Этот факт не специфичен для свойств: для объектов (в том числе, в логике первого порядка) он тоже имеет место. Т.е. если теория определяет, скажем, константу $0$, то это автоматически подразумевает существование и единственность соответствующего объекта. Данная константа - имя собственное для объекта. И правило подстановки работает для неё так же. Т.е. если есть, скажем, утверждение $\forall x ~ S(x) \ne 0$, то подстановка $0$ вместо $x$ даст: $S(0) \ne 0$. Это - чисто синтаксическая операция. Никакое определение натурального числа (другие составляющие его аксиомы) при этом не проверяется, в том числе - и на НАЛИЧИЕ не проверяется.

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

Свойства "всемогущество" НЕ СУЩЕСТВУЕТ, пока не предъявлено определение.

В то, что Вы сейчас говорите, можно верить или не верить, но это - не классическая логика. В классической логике факт существования чего бы то ни было не зависит от того, кто кому что предъявил или не предъявил. От этого может только зависеть наше знание или незнание этого факта. Когда некто присваивает некоему свойству имя собственное (а "всемогущий" - это как раз имя собственное для свойства), этим он утверждает, что такое свойство существует и единственно. Да, он может врать (или ошибаться), но истинности тавтологии это не отменит. Так что из тавтологии "Всемогущий либо существует, либо не существует" никоим образом не следует существование свойства всемогущества.

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

Логика ничего подобного не утверждает. Логика вообще не занимается несформулированными вопросами.

"Для особо одарённых" повторю ещё раз: "Сформулированным" является любое синтаксически корректное предложение. Ни к каким определениям (которые задаются аксиоматикой) это отношения не имеет.

[Munin]

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

В каком смысле ответ может удовлетворять какому-то свойству? Кстати, $\exists x\,X(x)\vee\nexists x\,X(x)$ - это не свойство, а просто какая-то формула. У свойств в качестве аргументов подразумеваются объекты.

$x$ в этой формуле связано, а вот $X$ несвязано. Жаль, что вы с логикой второго порядка не настолько знакомы, чтобы обратить на это внимание. Видимо, дальше неинтересно.

[migmit]

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

Нет, нет, нет. Всё, что требуется, - это наличие у свойства имени собственного.

Конечно. Только в математическом тексте "имя собственное" — это сокращённое определение.

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

Не путайте это с проверкой определения (ибо проверка НАЛИЧИЯ определения - это тоже проверка).

Так не надо ничего проверять. Это во всяких играх, бывает, проверяют "а нет ли у меня в руках электронной отмычки", прежде чем приложить её к замку, а реально — если нет, так и прикладывать нечего, без всяких проверок.

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

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

Не путайте математический факт (существование, скажем, натурального числа) и метаматематический факт (существование определения).

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

Так что из тавтологии "Всемогущий либо существует, либо не существует" никоим образом не следует существование свойства всемогущества.

Конечно, не следует. Потому что это не тавтология, а бессмысленный набор букв.

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

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

Логика ничего подобного не утверждает. Логика вообще не занимается несформулированными вопросами.

"Для особо одарённых" повторю ещё раз: "Сформулированным" является любое синтаксически корректное предложение. Ни к каким определениям (которые задаются аксиоматикой) это отношения не имеет.

Конечно. А синтаксическая корректность подразумеват использование ТОЛЬКО таких понятий, которые были определены ранее.

[epros]

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

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

В каком смысле ответ может удовлетворять какому-то свойству? Кстати, $\exists x\,X(x)\vee\nexists x\,X(x)$ - это не свойство, а просто какая-то формула. У свойств в качестве аргументов подразумеваются объекты.

$x$ в этой формуле связано, а вот $X$ несвязано. Жаль, что вы с логикой второго порядка не настолько знакомы, чтобы обратить на это внимание. Видимо, дальше неинтересно.

Формула и свойство - не одно и то же. Эта формула - тождественная истина независимо от аргумента $X$, вот и всё. Причём тут какое-то свойство какого-то ответа - непонятно.

-- Пн авг 20, 2012 12:28:53 --

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

А синтаксическая корректность подразумеват использование ТОЛЬКО таких понятий, которые были определены ранее.

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

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

Не путайте математический факт (существование, скажем, натурального числа) и метаматематический факт (существование определения).

Э-эээ, не пытайтесь запудрить мне и себе мозги. Утверждение о существовании - хоть в предметной теории, хоть в мета-теории записывается формулой вида $\exists x ~ \varphi$, где $\varphi$ - формула со свободной переменной $x$. Указанная формула - это определение объекта. А сам объект может быть чем угодно: может быть "натуральным числом" (в предметной теории), а может быть "формулой предметной теории, определяющей свойство $X$" (уже в мета-теории). Или наоборот: может быть "свойством всемогущества" (определённым в предметной теории), а может быть "формулой предметной теории, определяющей понятие натурального числа" (уже в мета-теории).

Ещё раз: определение понятия заключено во множестве аксиом. Это могут быть просто аксиомы предметной теории: $\varphi_1, \varphi_2, \dots ,\varphi_n$, а можно сформулировать одно мета-утверждение: "Формула $\varphi_1 \wedge \varphi_2 \wedge \dots \wedge \varphi_n$ определяет объект $X$".

-- Пн авг 20, 2012 12:42:04 --

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

Как он, по-Вашему, будет проверять наличие определения для упомянутой в предложении константы?

Вот пример синтаксически корректного предложения, являющегося утверждением о существовании: $\exists x ~ S(x)=0$. Аналитическая грамматика, проверяющая синтаксическую корректность, должна откуда-то достать определение константы $0$? Да не фига. Она просто проверит, что константу $0$ можно ставить в правый аргумент предиката равенства, и всё.

А чем это отличается, например, от синтаксической проверки этого:
$\nexists X \forall x ~ X(x) \leftrightarrow \operatorname{Omnipotent}(x)$?

[migmit]

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

Синтаксическая корректность - это только соответствие правилам языка, ничего больше.

А одно из правил языка - "использовать только известные слова".

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

Как он, по-Вашему, будет проверять наличие определения для упомянутой в предложении константы?

Вы правда считаете, что "формула" и "математический текст" - это одно и то же? Я вас разочарую. Формула не упоминает "константы" без их определения. В частности, формула, выражающая теорему из теории групп, включает в себя определение группы.

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

Э-эээ, не пытайтесь запудрить мне и себе мозги. Утверждение о существовании - хоть в предметной теории, хоть в мета-теории записывается формулой вида $\exists x ~ \varphi$,

А "определения", если я правильно помню, вообще метатеориями не рассматриваются. Определения - это просто сокращения речи. Наличие определения - не теорема метатеории, а метаматематический факт. Факт, говорящий О МАТЕМАТИКЕ.

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

Это могут быть просто аксиомы предметной теории: $\varphi_1, \varphi_2, \dots ,\varphi_n$, а можно сформулировать одно мета-утверждение: "Формула $\varphi_1 \wedge \varphi_2 \wedge \dots \wedge \varphi_n$ определяет объект $X$".

Это вообще какой-то бессмысленный набор слов.

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

-- Пн авг 20, 2012 12:42:04 --

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

Вот пример синтаксически корректного предложения, являющегося утверждением о существовании: $\exists x ~ S(x)=0$. Аналитическая грамматика, проверяющая синтаксическую корректность, должна откуда-то достать определение константы $0$?

Нет. Это мы должны его предоставить. Иначе формула не является синтаксически корректной.

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

Да не фига. Она просто проверит, что константу $0$ можно ставить в правый аргумент предиката равенства, и всё.

Нет, конечно.

Кстати, определение равенства мы тоже должны предоставить.