пропозициональные связки

[Kras]

У нас тут, короче, небольшая путаница пошла. Началось с того, что в соседней теме я определил пропозициональные связки как функции $B^n \to B$, где $B$ — булево множество. Всё хорошо, но аксиоматика теории множеств (любая) сама по себе использует пропозициональные связки. Возникает порочный круг: теория множеств использует логику, а логика использует понятия теории множеств. Выход из сложившейся ситуации только один: построить такую теорию, которая бы объясняла совершенно независимо что такое отрицание, импликация, конъюнкция...

Вопрос в том, а как это сделать?

[Xaositect]

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

А в конце концов, все интерпретируется либо в естетсвенном языке в среде естественных математиков, либо в состояниях компьютера в компьютерных пруверах.

[Kras]

Интересно, а сами понятия синтаксис, алфавит, интерпретация имеют какое-то строгое истолкование? Впрочем, мы не об этом.

Цитата:

Логическая связка - это символ, и он ничего не означает пока мы не зафиксировали какую-то его интерпретацию.

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

[Xaositect]

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

[arseniiv]

Kras в сообщении #1019651 писал(а):

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

Тут добавить к сказанному уже нечего. Просто посмотрите, как кодируется одна формальная теория в другой (практически всегда арифметике, она же всем знакома — хотя вот можно взять теорию двоичных строк, разницы в выразительности не будет), а потом внешнюю воспринимайте как неформальную.

(Оффтоп)

Кстати говоря, имея знакомство с аксиоматической арифметикой и имея некоторые соображения, которые можно получить в том числе из теории типов, можно легко записать аксиоматическую теорию двоичных строк (или описать частично рекурсивные функции над ними). Если не пробовали — попробуйте, это упражнение небессмысленное.

[Kras]

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

В данном случае, например, полная теория множеств совершенно не нужна, достаточно теории конечных множеств, которая интерпретируется в обычной арифметике.

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

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

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

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

[iifat]

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

[arseniiv]

Kras в сообщении #1019893 писал(а):

Аксиоматика Пеано ничего не даёт для объяснения логических связок, более того сама использует логические связки.

А это не обычная арифметика, а формализованная. Обычная формулируется на естественном языке и понимается в меру распущености. ( )

Kras в сообщении #1019893 писал(а):

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

О Диэдр, но это-то вообще сама простота! Только я для своей простоты буду вместо чисел использовать бинарные строки. Нам нужно закодировать символы $(, ), \wedge, \vee, \to, \leftrightarrow, \neg, \forall, \exists, =, v, '$ (переменные будут $v,v',v'',\ldots$) и функциональные и предикатные символы теории (для теории множеств, понятно, один только $\in$). Кстати, тут полезно бы использовать польскую нотацию (скобки выкидываем), индексы де Брёйна (выкидываем связанные переменные и некорректные подстановки) и прочие упрощающие жизнь штучки.

Итак, символов получилось 13 (это знак, знак!). Значит, каждый из них будем кодировать четырьмя нулями-единицами. Пускай, например, коды будут соответственно 0001—1101. Кодом строки в нашем алфавите будет строка длины $4n$, каждая последовательная четвёрка цифр которой равны коду какого-то символа. Дальше мы можем выразить конкатенацию строк через конкатенацию строк (удивительно), выразить всякие подстановки, проверку на то, является ли строка формулой, есть ли в формуле подформула и т. п.. Потом станем кодировать последовательности формул как строки, в которых отдельные формулы разделены, скажем, последовательностью 0000. Теперь можно выразить, является ли последовательность выводом и другие вещи.

Я просто не знаю, на что дать ссылку (ну не на GEBaEGB Хофштадтера же, там для нематематиков), а так это кусок конспекта того, что есть в книгах с классическим доказательством теорем Гёделя о неполноте.

-- Вт май 26, 2015 17:07:03 --

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

что есть в книгах

Но там обычно арифметика, но не составит труда сопоставить последовательности натуральным числам. Хотя бы просто добавляем к последовательности слева единицу и рассматриваем результат как представление в двоичной системе. Соотношения $xy = z, x = \varepsilon, x = 0, x = 1$ выразить удастся ($\varepsilon$ — это пустая строка).

[Kras]

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

Теперь можно выразить, является ли последовательность выводом

Так это самый главный вопрос. После вопроса "А как выводить?"

[arseniiv]

Добавляя к тому ещё посту, это такая страшная тривиальщина, что, боюсь, сейчас будут косо смотреть.

Kras в сообщении #1019911 писал(а):

Так это самый главный вопрос. После вопроса "А как выводить?"

Ну, правилами вывода выводить, очевидно. Как вы проверите, является ли формула применением правила вывода к набору других формул? Рассмотрим, например, Modus ponens $\varphi,\varphi\to\psi\vdash\psi$. Выводимость $A,B\vdash C$ по MP равносильна тому, что $B = A\to C$ или $A = B\to C$. А если рассматривать упорядоченные наборы формул, ещё проще (ровно $B = A\to C$). С другими правилами может быть сложнее (правила Бернайса, например — там нужно, чтобы в одной из формул переменная была свободной), но усердие, как говорил Козьма Прутков, всё превозмогает!

(Оффтоп)

Пришлось отредактировать формулы из-за вхождений в них \varpsi. Бывает, что усердие превозмогает и рассудок (опять Прутков).

-- Вт май 26, 2015 17:20:14 --

Ну а проверка на то, вывод ли вся последовательность, идёт прямо по определению.

[Kras]

Верно ли я понимаю, что логические операции (как функции) никакого отношения не имеют к символам $ \wedge, \vee, \to, \leftrightarrow, \neg$, которые применяются в исчислении высказываний?

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

Цитата:

Аксиоматика Пеано ничего не даёт для объяснения логических связок, более того сама использует логические связки.

А это не обычная арифметика, а формализованная. Обычная формулируется на естественном языке и понимается в меру распущености. ( )

Вот здесь возникает самое большое удивление.

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

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

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

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

Так какая арифметика имелась в виду?

[arseniiv]

Kras в сообщении #1019964 писал(а):

Верно ли я понимаю, что логические операции (как функции) никакого отношения не имеют к символам $ \wedge, \vee, \to, \leftrightarrow, \neg$, которые применяются в исчислении высказываний?

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

[Kras]

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

[arseniiv]

В том, что $I(\varphi\wedge\psi) = I(\varphi)\wedge I(\psi)$, где справа уже булева функция.

-- Вт май 26, 2015 19:25:55 --

Если что, произвол интерпретаций выражается в другом.

[Kras]

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

$I(\varphi\wedge\psi) = I(\varphi)\wedge I(\psi)$

Можно подробнее, что это означает?