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

[epros]

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

Как же Вы их различаете, безымянные ?

По содержанию, посимвольным сравнением строк. Правда не понимаете или прикалываетесь?

Кстати, функции в языке программирования тоже можно различать не только по имени, но и по коду. Но вот сослаться по коду из кода функции на саму себя не получится.

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

Если у высказываний нет имен, значит надо их дать (что Гедель и сделал) - числами.

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

Чтобы закрыть этот вопрос с Гёделем, поясню. Гёделевское высказывание (то самое, которое утверждает собственную недоказуемость в некоторой теории) на самом деле является всего лишь высказыванием арифметики о несуществовании некоего натурального числа. То, что это число является номером доказательства данного высказывания в данной теории, знает только метатеория, которая присваивает номера высказываниям языка и доказательствам теории. То бишь, это знание выражено не в синтаксисе, а в аксиоматике метатеории.

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

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

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

[Someone]

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

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

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

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

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

И грамматика тоже определяется в метатеории.

[arseniiv]

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

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

О Диэдр, неужели я действительно настолько плохо образую контекст? Имелся в виду язык нулевого или первого порядка, расширенный пропозициональными переменными и остальными упомянутыми конструкциями. Потом вместо пропозициональных переменных я ввёл «цитатные» (и соответствующие термы, образуемые как описано выше и вставляющиеся в формулы как там же).

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

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

Если $a$ — цитатная переменная и $q$ — цитата, $\mu a.q$ — цитата. Ещё цитаты образуются цитированием формулы и пока больше никак. (Это на всякий случай.)

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

Вопрос заключался в том, как чисто синтаксически определяется ссылка на само высказывание, содержащее ссылку.

Как переменная, связанная охватывающим $\mu$. Т. е. $a$ в $q$ в $\mu a.q$ ссылается на $\mu a.q$.

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

Но терм метаязыка и выражаемый им объект - терм арифметики - это разные вещи, которые относятся к разным языкам.

Можете трактовать мой язык не как язык с самоссыланием, но надо добавить, что языки с таким описанием создавались раньше, и я даже читал описание одного из них от Смаллиана, но ничего тогда не понял в семантике. Иронично будет, если он сейчас здесь переоткрыт.
____________

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

Вот берем формулу факториала на хаскеле

Это не формула, это, эм, определение. Формуле по соответствию К.—Г. будет отвечать выражение — например,

Используется синтаксис Haskell

y (\f x -> case x of { [] -> 0; (_:as) -> 1 + f as })

где y — определённый где-то выше какой-нибудь комбинатор фиксированной точки. Можно даже считать, что вместо y стоит соответствующее выражение (мне просто его лень писать). Правда, я тут соврал, и этому выражению будет соответствовать не формула, а вывод из гипотезы (получается функция одного аргумента). Если определённый тип списков населён, то населён тип натуральных чисел (да, скучновато, но соответствию К.—Г. интересны типы, а не то, какой терм нужного типа мы нарисуем; а так-то доказать то же можно и термом \_ -> 0).

Вообще же тут это оффтоп, по-моему.

[shkolnik]

Хотелось бы еще, но т.к. оффтоп, последнее (надеюсь) уточнение:

Someone в сообщении #1141125 писал(а):

И грамматика тоже определяется в метатеории.

Может ли эта аналитическая грамматика-метатеория, включать в себя арифметику ?

[Someone]

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

Хотелось бы еще, но т.к. оффтоп, последнее (надеюсь) уточнение:

Someone в сообщении #1141125 писал(а):

И грамматика тоже определяется в метатеории.

Может ли эта аналитическая грамматика-метатеория, включать в себя арифметику ?

Может. Более того, если вдруг нужна формализованная метатеория, то можно использовать арифметику Пеано. Или теорию множеств.
Но метатеория — это не грамматика, а средство формализации (предметной) теории. В метатеории определяется алфавит предметной теории, её синтаксис, аксиомы и правила вывода. В ней же строятся модели предметной теории, определяется выводимость, доказываются метатеоремы… Например, теоремы Гёделя о неполноте арифметики — типичные метатеоремы.