Как разгадать этот софизм?

[ET]

atlakatl в сообщении #1140399 писал(а):

А куда подевалось "менее одного не"?

Читайте внимательнее, что я написал:

Цитата:

Утверждение А не содержит или содержит более одного не

atlakatl в сообщении #1140399 писал(а):

И почему всё-таки "Неа"? - Конкретно.

Потому что неа. Изначальное суждение было об утверждении А. И отрицание его тоже должно быть о том же утверждении

[arseniiv]

Вообще никто не мешает на коленке точно определить язык и записать всё на нём. Для этого нам понадобится уметь рыться внутри формулы и уметь в данной формуле использовать её же. Определим соответствующие конструкции:
• $N\varphi$ есть формула, означающая «в формуле $\varphi$ ровно один символ $\neg$ и никаких $N$, либо никаких $\neg$ и ровно один $N$»;
• $\mu a.\psi$ есть формула, подстановка которой в $\psi$ вместо $a$ даёт эквивалентную; если $\alpha\leftrightarrow\psi$, то $\alpha\leftrightarrow\mu a.\psi[a/\alpha]$, где $\psi$ не содержит свободных вхождений $a$.

Тогда $A = \mu a.Na$, $B = \neg\mu a.Na$, но никак не $\mu a.\neg Na$ [UPD: в посте ниже эта формула зовётся $B'$]. Хотя это не означает, что это не две разные записи одного и того же. Если учесть, что $\mu a.\neg a\leftrightarrow\neg\mu a.\neg a$, можно и закончить. (С этим связана история про, насколько помню, Карри и его первый вариант λ-исчисления, но я не знаю, как именно он выглядел, так что гадать, в какой форме у него эта штука вылезла и сделала исчисление противоречивым, не стану. Но вылезла и сделала.)

[epros]

arseniiv в сообщении #1140442 писал(а):

• $N\varphi$ есть формула, означающая «в формуле $\varphi$ ровно один символ $\neg$ и никаких $N$, либо никаких $\neg$ и ровно один $N$»;

Интересно, как Вы это представляете себе синтаксически? Вот у нас есть аналитическая грамматика, которая при предъявлении ей строки говорит, формула это или нет. Поэтому подстрока $\varphi$ должна распознаваться как формула. Но и вся строка, в которой содержится и это $\varphi$, и какие-то слова про то, что оно якобы "формула", тоже должна распознаваться как формула того же языка. Вложенные кавычки что ли будете употреблять?

Вот, скажем, есть формула арифметики $2 \times 2 = 4$. Мы хотим сказать, что это - формула арифметики. И мы выражаем это так: $, где $\mathbb{A}$ обозначает язык арифметики. Однако это наше выражение уже есть не формула языка арифметики $\mathbb{A}$, а формула некоего расширенного языка $\mathbb{A}_1$. Вы же, насколько я понимаю, хотите расширить язык таким образом, чтобы в нём можно было сформулировать утверждение о том, что нечто является формулой его самого. Как?

[arseniiv]

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

Интересно, как Вы это представляете себе синтаксически?

Синтаксически как раз проблем нет. Когда мы начинаем выводить формулы, не обязательно оставлять верным $\vdash\varphi\leftrightarrow\psi\Rightarrow{}\vdash N\varphi\leftrightarrow N\psi$.

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

Поэтому подстрока $\varphi$ должна распознаваться как формула. Но и вся строка, в которой содержится и это $\varphi$, и какие-то слова про то, что оно якобы "формула", тоже должна распознаваться как формула того же языка.

Не понял, в чём проблема. Формулы отличаются от неформул тем, что у них есть вывод с помощью formation rules. Мы добавляем к обычным таким правилам для языка первого порядка ещё одно правило $\dfrac{\varphi\;\mathrm{wff}}{N\varphi\;\mathrm{wff}}$; однозначность чтения не нарушается и всё такое прочее.

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

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

См. выше. В любом случае, если вы говорите о проблемах, они начинаются намного раньше из-за $\mu$, и для них не нужно $N$, в то время как для разбора полётов в этой теме нужны они оба. По-моему, я показал, что нет смысла говорить о том, что неправильно сформулированное $B'$ чем-то отличается от $B$, раз уж мы всё равно можем вывести противоречие, а оттуда всё подряд, в том числе как $B\leftrightarrow B'$, так и $B\leftrightarrow\neg B'$.

[epros]

arseniiv в сообщении #1140475 писал(а):

Когда мы начинаем выводить формулы, не обязательно оставлять верным $\vdash\varphi\leftrightarrow\psi\Rightarrow{}\vdash N\varphi\leftrightarrow N\psi$.

Непонятно, причём здесь выводимость? Речь была только о том, является или не является некая строка формулой некоего языка.

arseniiv в сообщении #1140475 писал(а):

Не понял, в чём проблема. Формулы отличаются от неформул тем, что у них есть вывод с помощью formation rules. Мы добавляем к обычным таким правилам для языка первого порядка ещё одно правило $\dfrac{\varphi\;\mathrm{wff}}{N\varphi\;\mathrm{wff}}$; однозначность чтения не нарушается и всё такое прочее.

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

arseniiv в сообщении #1140475 писал(а):

В любом случае, если вы говорите о проблемах...

Нет, не о проблемах. Я и сам могу навскидку предложить некий синтаксис, в котором выразимо некое утверждение о том, что некая строка является формулой того же самого языка, в котором сформулировано это утверждение. Например, обозначим этот язык как $\mathbb{L}$ и будем считать, что $\langle x \rangle \in \mathbb{L}$ означает как раз то, что строка, подставляемая вместо $x$, является формулой языка $\mathbb{L}$. Тогда в грамматике языка $\mathbb{L}$ должно быть заложено правило: Если $x$ - строка в алфавите $\mathbb{L}$, то $\langle x \rangle \in \mathbb{L}$ - формула $\mathbb{L}$.

Отсюда следуют, например, что $\langle \langle x \rangle \in \mathbb{L} \rangle \in \mathbb{L}$ - тоже формула $\mathbb{L}$. Но я совершенно не вижу способа выразить в этом синтаксисе ссылку из формулы на саму же эту формулу. Поэтому непонятно, каким образом мы можем формализовать упомянутый ТС софизм.

[shkolnik]

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

Я и сам могу навскидку предложить некий синтаксис, в котором выразимо некое утверждение о том, что некая строка является формулой того же самого языка, в котором сформулировано это утверждение.
---
Отсюда следуют, например, что $\langle \langle x \rangle \in \mathbb{L} \rangle \in \mathbb{L}$ - тоже формула $\mathbb{L}$. Но я совершенно не вижу способа выразить в этом синтаксисе ссылку из формулы на саму же эту формулу.

Так нельзя : $x= \langle x \rangle \in \mathbb{L}$ ?

[arseniiv]

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

Поэтому непонятно, каким образом мы можем формализовать упомянутый ТС софизм.

Ну а для чего я написал про $\mu$? Пусть $A^\circ = Na$ «в $a$ ровно одно отрицание», где $a$ — пропозициональная переменная. Теперь надо отождествить $a$ со всей $A^\circ$, для этого возьмём (формально так) фиксированную точку этой штуки как функции от $a$, $\mu a.Na$, это и есть (по соглашению) формула, говорящая о себе. (Потом, когда будем выводить что-нибудь, добавим соответствующую аксиому $\mu a.\psi\leftrightarrow \psi[\mu a.\psi/a]$ (надо было выше прям так и написать, а я что-то вокруг да около), уже определяющую смысл этой конструкции явно.)

[epros]

shkolnik в сообщении #1140606 писал(а):

Так нельзя : $x= \langle x \rangle \in \mathbb{L}$ ?

Поскольку $x$ - это такая штука, вместо которой подставляется строка, данное утверждение о равенстве строк очевидным образом ложно.

arseniiv в сообщении #1140647 писал(а):

Пусть $A^\circ = Na$ «в $a$ ровно одно отрицание», где $a$ — пропозициональная переменная.

Я такого синтаксиса не понимаю. Если $a$ - пропозициональная переменная (т.е. символ специального вида), то что означают остальные слова внутри кавычек? В пропозициональных переменных не бывает никаких отрицаний.

К тому же раньше я слышал нечто иное:

arseniiv в сообщении #1140442 писал(а):

$N\varphi$ есть формула, означающая «в формуле $\varphi$ ровно один символ $\neg$ и никаких $N$, либо никаких $\neg$ и ровно один $N$»;

Здесь $\varphi$ названа "формулой", т.е. строкой некоего специального вида. А это не то же самое, что пропозициональная переменная (в синтаксическом смысле).

Выше я комментировал слова именно про "формулу", ибо хотел обратить внимание, что утверждение про то, что нечто - "формула", подразумевает проверку соответствующей строки с помощью аналитической грамматики. То бишь проверки того, сколько раз в этой строке встречается символ $\neg$, недостаточно.

arseniiv в сообщении #1140647 писал(а):

для этого возьмём (формально так) фиксированную точку этой штуки как функции от $a$, $\mu a.Na$, это и есть (по соглашению) формула, говорящая о себе

Здесь я уже окончательно потерял нить.

[buddy]

arseniiv в сообщении #1140647 писал(а):

это и есть (по соглашению) формула, говорящая о себе.

Примеры таких формул (если я не ошибаюсь):
- Любая рекурсивная программа.
- Программа, печатающая свой собственный текст.
- Самовоспроизводящиеся автоматы Неймана.
- Списки Лиспа.

[arseniiv]

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

Если $a$ - пропозициональная переменная (т.е. символ специального вида), то что означают остальные слова внутри кавычек?

Это было просто пояснение на словах. Этот текст не входит в $A^\circ$.

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

В пропозициональных переменных не бывает никаких отрицаний.

А вот это мне всё портит, если не подправить. Можно
(1) сказать, что $N\varphi$ имеет смысл «в $\varphi$ ровно одно отрицание» только тогда, когда $\varphi$ не содержит свободных пропозициональных переменных, и что-то ещё добавить, или
(2) всё-таки ввести в язык новые конструкции — цитаты, будем обозначать их как раз $\langle\ldots\rangle$, и сделать $N$ превращающим цитаты в формулы, а $\mu$ действующим на цитатах. Тогда моя конструкция будет иметь вид $N(\mu a.\langle Na\rangle)$, или более красиво $I(\mu a.\langle Na\rangle)$, где $I$ снимает цитирование. Заодно можно будет вернуть пропозициональные переменные в небытие.

Проблемы с парадоксом лжеца у такой системы (т. е. правила вывода соответствующие добавлены), по идее, должны остаться, даже если не вводить $I$, но я за один раз не смог ничего нарисовать.

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

Здесь $\varphi$ названа "формулой", т.е. строкой некоего специального вида. А это не то же самое, что пропозициональная переменная (в синтаксическом смысле).

Там она и есть формула, любая. Но в том числе может быть и пропозициональной переменной.

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

Выше я комментировал слова именно про "формулу", ибо хотел обратить внимание, что утверждение про то, что нечто - "формула", подразумевает проверку соответствующей строки с помощью аналитической грамматики. То бишь проверки того, сколько раз в этой строке встречается символ $\neg$, недостаточно.

Но какие проблемы там могут возникнуть?

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

Здесь я уже окончательно потерял нить.

Просто имеется конструкция $\mu a.\varphi$, являющаяся формулой, и, если дело дойдёт до аксиом, аксиома $\mu a.\psi\leftrightarrow \psi[\mu a.\psi/a]$, и это следует считать всем, что связано со смыслом такой конструкции. Можете понимать её как захочется или никак не понимать. Пока мы говорим о языке, но ни об интерпретациях, ни о выводе, чего ещё можно желать от синтаксиса, я не знаю.

(В новой редакции номер 2 будет конструкция $\mu a.q$, где $a$ — проп. переменная, $q$ — цитата, а всё вместе — тоже цитата, и аксиома $I(\mu a.q)\leftrightarrow I(q[\mu a.q/a])$, хотя переформулировки без $I$ здесь сейчас не будет. Если она вообще невозможна, тогда я ликую, потому что система сразу опять противоречива, как и хочется.)

-- Пт июл 29, 2016 15:01:35 --

buddy
Их сначала надо протащить в логику. Дальше я могу сказать только про две вещи из четырёх:

buddy в сообщении #1140776 писал(а):

- Списки Лиспа.

Тут надо отметить, что
(1) Если мы говорим о самом типе списков, его можно всегда выразить в системе без $\mu$ (понимаемом уже в распространённом смысле). Можно добавить несколько правил вывода к какой-нибудь теории типов и всё. (Или ничего не добавлять к такой, где уже есть тип $\mathbb N$, но это, наверно, не подходит под описание «списки лиспа», так что убрал подальше в скобки.)
(2) Если говорить о значениях такого типа, там и подавно ничего такого нет, ведь каждому списку сопоставится конечное дерево.

buddy в сообщении #1140776 писал(а):

- Любая рекурсивная программа.

В смысле, с рекурсией? Тогда тут тоже нет ничего такого, потому что комбинаторы фиксированной точки как есть в λ-исчислении, так никуда не деваются и в просто типизированном λ-исчислении, где никаких $\mu$ нет. У $Y$ будет тип $(a\to a)\to a$, например.

Боюсь, так только больше путаницы здесь возникнет.

[buddy]

Я, видимо, чего-то не понимаю.
Вот берем формулу факториала на хаскеле

 fac :: Integer -> Integer
 fac 0 = 1
 fac n | n > 0 = n * fac (n - 1)

Самоссылочная формула. Разве проблема расширить язык соответствующими правилами и соответствующей нотацией по рекурсивному вычислению значений истина-ложь?

-- 29.07.2016, 17:26 --

Если лист дерева, то ему можем присвоить значения 0/1, если не лист, то идет разбор дерева, поддеревья у которых все листы заменяем на вычисленное значение 0/1 и так добираемся до корня, таким образом вычисляя значения самоссылочной формулы. Для бесконечных поддеревье специального вида наверное тоже можно ввести какое-либо правило редуцирования его, но полцучится ли из этого что-либо разумное, совсем не уверен.

[shkolnik]

Я видимо тоже чего-то не понимаю. Вместо того чтобы строить нумерацию утверждений и предъявлять утверждение об утверждении с неким номером, которое может оказаться самим этим утверждением (аля-Геделевский номер), не легче ли изначально предусмотреть какие-то средства, в грамматике.

(Оффтоп)

В HQ9+ это вообще одно $Q$. Будем считать, что это некий синтаксис, в котором выразимо некое утверждение о том, что некая строка является формулой того же самого языка, в котором сформулировано это утверждение.
Простейшая формула, о том, что формула является формулой тогоже самого языка самой формулы - это $Q$

[shkolnik]

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

Поскольку $x$ - это такая штука, вместо которой подставляется строка, данное утверждение о равенстве строк очевидным образом ложно.

Кстати, если рассматривать эту формулу, как правило грамматики, то очевидным образом, если "штука" подставляемая вместо $x$ не удовлетворяет этому условию (ложна), то она не является словом в языке $\mathbb{L}$.

[epros]

arseniiv в сообщении #1140780 писал(а):

только тогда, когда $\varphi$ не содержит свободных пропозициональных переменных

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

arseniiv в сообщении #1140780 писал(а):

$\mu$ действующим на цитатах

Каким образом действующим? В общем, по мне, так что-то здесь слишком много недосказанного.

arseniiv в сообщении #1140780 писал(а):

Но какие проблемы там могут возникнуть?

Мы до проблем просто пока не добрались. Вопрос заключался в том, как чисто синтаксически определяется ссылка на само высказывание, содержащее ссылку. Т.е. здесь смешиваются два "уровня" логики: 1) синтаксический, на котором мы оперируем только именами объектов, и 2) семантический, на котором мы оперируем самими объектами. Например, на языках первого порядка объекты выражаются термами. На языке арифметики Пеано терм $1+1$ обозначает объект - число два. В метаязыке, на котором мы говорим о формулах и термах арифметики Пеано, будут термы, обозначающие такие объекты, как формула арифметики $0=1$, терм арифметики $1+1$ или терм арифметики $1+1+0$. Но терм метаязыка и выражаемый им объект - терм арифметики - это разные вещи, которые относятся к разным языкам.

Я пока не понял, как Вы предлагаете чисто синтаксически внутри высказывания языка выражать имя, обозначающее объект, который является ничем иным, как самим эти высказыванием. И мне будет интересно, что произойдёт, если мы слегка изменим это высказывание, но не изменим это имя внутри него? Имя станет соответствовать новому высказыванию? Притом, что то же имя в старом высказывании соответствует старому высказыванию? А что будет, если мы сформулируем высказывание о высказывании, внутри которого упоминается это имя? К какому из высказываний будет относиться это имя?

(Пример на естественном языке)

"Мы не знаем как трактовать высказывание о том, что данное высказывание ложно".

buddy в сообщении #1140831 писал(а):

Самоссылочная формула. Разве проблема расширить язык соответствующими правилами и соответствующей нотацией по рекурсивному вычислению значений истина-ложь?

Пока не вижу связи между рекурсивной функцией в языке программирования и самоссылающимся высказыванием. Код функции ссылается на саму функцию по её имени. Это возможно по той причине, что имя и код функции - разные вещи. В языке программирования предусмотрены средства для связывания имени с кодом функции - определение функции, которое следует за её описанием (т.е. за резервированием данного имени). В естественном же языке, а также в таких формальных языках, как язык логики первого порядка, у высказываний нет имён. Слова "данное высказывание" не являются уникальным именем данного высказывания, поэтому под ними можно понимать что угодно.

shkolnik в сообщении #1140887 писал(а):

Вместо того чтобы строить нумерацию утверждений и предъявлять утверждение об утверждении с неким номером, которое может оказаться самим этим утверждением (аля-Геделевский номер)

Не понимаю, к чему Вы это? Здесь, вроде, не доказательство Гёделя обсуждалось.

shkolnik в сообщении #1140897 писал(а):

Кстати, если рассматривать эту формулу, как правило грамматики, то очевидным образом, если "штука" подставляемая вместо $x$ не удовлетворяет этому условию (ложна), то она не является словом в языке $\mathbb{L}$.

Я ничего не понял и у меня полное ощущение, что эта фраза - какая-то бессмыслица. Штука, подставляемая вместо $x$ является строкой символов, а поэтому она не может и не должна быть истинной или ложной. Это - просто строка символов. И как это равенство может быть правилом грамматики? Правила грамматики говорят о том, какие строки являются, а какие не являются предложениями (формулами) языка. Ну, иногда ещё - какие строки являются, а какие не являются термами языка (если в языке используется понятие "терм").

[shkolnik]

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

Не понимаю, к чему Вы это? Здесь, вроде, не доказательство Гёделя обсуждалось.

К чему тогда Ваши рассуждения:

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

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

Если у высказываний нет имен, значит надо их дать (что Гедель и сделал) - числами. Разве нет ? У высказываний нет имен - в анналы. Как же Вы их различаете, безымянные ?

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

Штука, подставляемая вместо $x$ является строкой символов, а поэтому она не может и не должна быть истинной или ложной. Это - просто строка символов. И как это равенство может быть правилом грамматики?

Строка символов не может быть истинной или ложной (хотя тоже странно звучит - любое утверждение - строка символов).
А вот правило грамматики - это возможность определить, истинно или ложно то, что пара строк равны. Например, равны ли строки $\{a,b,c\}$ и $\{b,a,c\}$. Если у Вас в грамматике нет праила сравнения строк - то и определить их равенство или не равенство Вы не можете.