Критерии подстановки (Бурбаки, Книга 1, параграф 1, пункт 2)

[project15]

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


1. Что такое "критерии подстановки" в строгом смысле?
2. Что такое "критерии подстановки" в описательном, интуитивном смысле?
3. Почему эти критерии истинны? Их истинность декларируется безоговорочно или подлежит проверке?
4. Что значит "проверить" эти критерии?
5. Почему часть этих критериев завязана на сокращающем символе $\tau_{x}(A)$? Что мешает мне придумать другой сокращающий символ (например, $\upsilon_{x}(A)$, который тождественен с знакосочетанием, в котором первый образец некоторой буквы заменен этой же буквой, только со штрихом) и придумать какой-нибудь "критерий подстановки" с моим сокращающим символом (например, критерий подстановки CS6: Если в некотором знакосочетании A фигурирует только один образец некоторой буквы, то $\upsilon_{x}($\upsilon_{x}(A))$ тождественно с $(x''|x)A$).
6. Можно ли утверждать, что этими пятью критериями, приводимыми Бурбаки, исчерпываются все критерии подстановки? Или это количество произвольно, в том смысле, что можно придумать сколь угодно "правил манипулирования", которые можно назвать "критериями подстановки", и Бурбаки приводят именно эти критерии лишь потому что они первыми пришли им в голову и кажутся им очевидными? Иными словами, являются ли эти критерии в некотором смысле "составными кирпичиками" для других критериев (если они существуют, эти другие критерии)?
7. Зачем они нужны? Какие цели достигаются, благодаря использованию этих критериев? Какие сложности (типографские/умственные и т.д.) возникнут, если мы эти критерии не будем использовать?
8. Где они будут дальше использоваться?


Предвещая ответ на 7-ый вопрос, отмечу, что понятие "сокращающий символ" (или короче "символ") для меня абсолютно понятно, необходимость его введения тоже понятна. А вот с критериями подстановки беда.


Заранее благодарю за ответы. Буду очень рад если получу ответы хотя бы на часть этих вопросов.

[george66]

Очень не советую изучать логику по Бурбакам (всё остальное можно). Содержательно, подстановка - операция сложная, но мы её не замечаем, потому что не пишем явно. Если ввести знак для подстановки
$\varphi[t/x]$
и попытаться выписать аксиомы, то с логическими связками всё просто
$(\varphi\vee\psi)[t/x]=\varphi[t/x]\vee\psi[t/x]$
и так далее, а с кванторами такая простая аксиома работает неправильно
$(\forall x\varphi)[t/y]\neq\forall x(\varphi[t/y])$
поскольку терм $t$ может свободно содержать переменную $x$ и в правой части она "схватится квантором", чего не надо. Соответственно, при подстановке приходится переименовывать некоторые связанные переменные. Например, заменять $\forall x\varphi$ на $\forall z(\varphi[z/x])$. В результате становится очень трудно про подстановку что-то доказать. Если не хотите глубоко вникать в предмет, возьмите другой учебник логики (не Бурбаков).

[project15]

george66
До аксиом и кванторов я пока еще не дошел . Итак, по порядку

george66 в сообщении #1400803 писал(а):

Содержательно, подстановка - операция сложная, но мы её не замечаем, потому что не пишем явно.

Если подстановка - это операция (рассмотрим сначала содержательный аспект), то с какими объектами и что она делает?

george66 в сообщении #1400803 писал(а):

Если ввести знак для подстановки $\varphi[t/x]$

Как читать этот символ и что он обозначает?

(Оффтоп)

george66 в сообщении #1400803 писал(а):

Если не хотите глубоко вникать в предмет, возьмите другой учебник логики (не Бурбаков).

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

[george66]

$\varphi[t/x]$ означает "формула $\varphi$ в которой свободная переменная $x$ везде заменена на выражение $t$"
Например, возьмём формулу
$x+x=2x$
и заменим $x$ на число $3$
$(x+x=2x)[3/x]$
После некоторых вычислений получим
$3+3=2\times 3$
Вычисления состоят в том, чтобы двигать подстановку вглубь формулы. Сначала сквозь равенство
$(x+x)[3/x]=(2x)[3/x]$
Затем сквозь символы сложения и умножения
$x[3/x]+x[3/x]=2[3/x]\times x[3/x]$
Наконец, заменяем $x[3/x]$ на $3$ (подстановка сработала), а $2[3/x]$ на $2$ (потому что $2$ это константа, вместо неё ничего не подставляем)
$3+3=2\times 3$

[project15]

george66

george66 в сообщении #1400834 писал(а):

$\varphi[t/x]$ означает "формула $\varphi$ в которой свободная переменная $x$ везде заменена на выражение $t$"

1. Можно ли использовать вместо слова "формула" слово "знакосочетание"?
2. Что такое "выражение $t$" ? Произвольное знакосочетание?
3. "Свободная переменная $x$ - это обязательно буква или вместо $x$ может быть логический знак или специальный знак теории?
4. Можно ли обойтись без упоминания "свободная переменная x", а вместо этого сказать "интересующая нас конкретная буква, которую мы обозначили за x, в каждом своем экземпляре заменена знакосочетанием A?
5. Если ответы утвердительные (на 3-ий вопрос - "обязательно буква"), то в чем тогда разница между $\varphi[t/x]$ и $(t|x)\varphi$?

[george66]

Немедленно бросьте Бурбаки и возьмите нормальный учебник. Среди Бурбаков не было логиков. Забудьте также слово "знакосочетание". Есть формулы и термы.

[Geen]

Кстати, извиняюсь если оффтоп, а не проще ли было бы вместо "строк" использовать "(направленный ациклический) граф"?

[project15]

george66

george66 в сообщении #1400846 писал(а):

Забудьте также слово "знакосочетание"

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

george66 в сообщении #1400846 писал(а):

Есть формулы и термы.

Терм теории $\mathfrak{T}$ - знакосочетания первого рода, встречающиеся в формативных кострукциях теории $\mathfrak{T}$. Определения соотношений Бурбаки тоже дают. Я подозреваю, что под словом "формула" вы понимаете именно "соотношение" в терминологии Бурбаки.

Как бы то ни было, мне пока еще рано думать про термы, формулы и т.д. Надо разобраться с критериями подстановки. Все вопросы в топике на данный момент для меня актуальны.

[project15]

Geen

Geen в сообщении #1400850 писал(а):

Кстати, извиняюсь если оффтоп, а не проще ли было бы вместо "строк" использовать "(направленный ациклический) граф"?

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

[project15]

У меня появилось несколько предположений о том, что из себя представляют критерии подстановки. Сразу сделаю оговорку о том, что все, что я написал ниже - мое представление, которое может оказаться полным бредом. Я лишь приступаю к изучению матлогики, не судите строго . Буду признателен за любые комментарии, замечания и критику.


Я начну с предложения, которое Бурбаки приводят в введении к первой книге:

Цитата:

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

На мой взгляд это предложение прекрасно олицетворяет собой ту ситуацию, которая складывается вокруг критериев подстановки. Касательно этого предложения, естественным образом встает вопрос его истинности. Не углубляясь в философский анализ понятия истины, я попытался ответить на этот вопрос. На первый взгляд это предложение кажется настолько очевидным, насколько это вообще возможно. Бурбаки даже называют его трюизмом. Но так ли это предложение очевидно? Если количество шаров в мешке конечно, то это и впрямь трюизм. Конечно, можно и здесь сказать, что наша интуиция не способна представить мешок в котором, например, $10^{10^{10}}$ шаров, но в таком случае придется вообще признать, что мы отказываемся от всякого рационального употребления наших умственных способностей. С этой оговоркой "финитный случай" этого предложения и впрямь можно признать трюизмом. Но если в мешке шаров бесконечно много, так ли это предложение очевидно? Мне, например, совсем неочевидно. И здесь, на мой взгляд, и кроется та "степень истинности", с которой мы принимаем критерии подстановки. Требовать "доказать" критерий подстановки по сути тоже самое, как и требовать "доказать" предложение о шарах в мешке (специально взял это слово в кавычки, т.к. употребляю это слово как синоним слову "проверить"; термин "доказательство" в матлогике имеет строгий смысл). Если некоторое знакосочетание теории конечно, то критерии подстановки являются трюизмами (опять же с оговоркой о том, что знакосочетание может быть очень длинным, но мы предполагаем, что наши интеллектуальные способности позволяют делать выводы о таких знакосочетаниях). Если же некоторое знакосочетание бесконечно (а требования конечности для знакосочетаний нету), то мы признаем за этими критериями подстановки "истинность того же порядка" как и истинность предложения о шарах. Т.к. мы, говоря о критериях подстановки, рассматриваем знакосочетания исключительно как синтаксический объект, то эти критерии подстановки - объекты метаматематики.

С этой точки зрения постараюсь ответить на часть своих же вопросов.

project15 в сообщении #1400787 писал(а):

1. Что такое "критерии подстановки" в строгом смысле?
2. Что такое "критерии подстановки" в описательном, интуитивном смысле?

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

project15 в сообщении #1400787 писал(а):

3. Почему эти критерии истинны? Их истинность декларируется безоговорочно или подлежит проверке?
4. Что значит "проверить" эти критерии?

Вопрос истинности критериев подстановки (в моем представлении) раскрыт в основном параграфе этого сообщения.

Ответы на оставшиеся вопросы сильно зависят от того, есть ли рациональное зерно в моем представлении критериев подстановки.

[arseniiv]

george66 в сообщении #1400803 писал(а):

Если не хотите глубоко вникать в предмет, возьмите другой учебник логики (не Бурбаков).

Даже если и хотеть, наверно тоже не стоит их брать, они мне мозг сломали, а потом оказалось, что матлогика на самом деле всё-таки весьма проста.

-- Пн июн 24, 2019 23:17:29 --

project15 в сообщении #1400808 писал(а):

Попробую Бурбаков почитать, если через пару месяцев дальше первой главы не продвинусь, видимо возьму какую-нибудь другую книгу.

Если что, они в следующих томах сами постарались от выбранного в первом представления отодвинуться. По крайней мере я это слышал, хоть сам и не проверял.

-- Пн июн 24, 2019 23:30:59 --

Geen в сообщении #1400850 писал(а):

Кстати, извиняюсь если оффтоп, а не проще ли было бы вместо "строк" использовать "(направленный ациклический) граф"?

Не, это будет неудобно, тем более что строка — это вполне общеизвестное понятие среди математики, занимающейся формальными языками. Строки — это просто кортежи, все строки над алфавитом $\Omega$ собираются в $\Omega^* := \bigcup_{n = 0}^\infty \Omega^n$.

Чтобы представить кортеж графом, надо будет хитро сопоставлять разные вхождения одинаковых букв вершинам. Придётся рассматривать графы с точностью до изоморфизма «буквоназначений» вершинам. С линейно упорядоченным множеством будет то же. Выбрав единственный представитель каждого такого множества — а это окажутся ровно все конечные ординалы — мы получим традиционное определение, ну по крайней мере одно из (кортежи определяют кто как хочет, хотя для работы с кортежами разных длин хорошо как раз определение $A^n = (n\to A)$, множество функций в $A$ из ординала $n$).

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

-- Пн июн 24, 2019 23:43:49 --

project15 в сообщении #1400856 писал(а):

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

Это вы зря так думаете. Переменные в общем случае бывают разных сортов, и подставлять вместо переменной можно лишь терм соответствующего сорта; в классической (в смысле изложения и языка) логике первого порядка они как раз зовутся термы и формулы, а я использую «терм» в более общем смысле. Правда, в той же логике первого порядка есть переменные только одного сорта — вместо которых можно подставлять термы, и кроме того в терм там никогда не может входить как составная часть формула. Но в общем случае, и случае многосортных логик (если они и не нужны, есть другие полезные формализмы, где всё насчёт подстановки и подобного низкоуровневого сохраняется — теории типов в разнообразии), равноправия побольше, и термы могут строиться из термов других сортов, и замыкаться в конструкциях, подобных кванторным формулам, тоже переменные не единственного сорта. Это всё наталкивает на рассмотрение некоторого «обобщённого языка термов», про который и стоит спрашивать, какой смысл у подстановки, связанных переменных, $\alpha$-конверсии (замены связанных переменных) и прочего.

Кстати, можно рассматривать и такие языки, где любая подстановка корректна — такие, где связанные переменные заменены т. н. индексами де Брёйна. Термы таких языков не надо рассматривать с точностью до $\alpha$-конверсии, что часто удобно (хотя опять же в книжках для начинающих это часто считается неудобным, и я большей частью с этим согласен). Правильной бурбакистской книжкой по логике должна была бы быть именно такая: манипулирующая деревьями произвольных сортов, собранными из произвольного набора конструкторов, говорящая об индексах де Брёйна, разбирающаяся со всем общим синтаксисом перед определением конкретных языков для логик высказываний, первого порядка и каких угодно других, а также и теорий типов до кучи. Сейчас они полезны.

-- Пн июн 24, 2019 23:53:09 --

project15 в сообщении #1401306 писал(а):

Если же некоторое знакосочетание бесконечно (а требования конечности для знакосочетаний нету)

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

Я бы сказал, что свойства подстановок надо выводить из семантики. Когда мы строим формальный язык, мы всегда исходим из некоторого неформального «что я хочу получить» (и уж потом иногда получаем и формальное описание семантики, но здесь я имею в виду именно неформальное). Отношения подстановки со связыванием переменных рано или поздно сведутся к тому, что мы хотим от них.

project15 в сообщении #1401306 писал(а):

Ответы на оставшиеся вопросы сильно зависят от того, есть ли рациональное зерно в моем представлении критериев подстановки.

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

Я мог бы описать пример достаточно общего такого языка, но мне пальчиком будут грозить, что я вас запутаю ещё сильнее чем могли бы Бурбаки. (Но я наверно всё равно не удержусь.)

[gefest_md]

project15
Можете также почитать первую главу учебника Клини, «Математическая логика». Просто теоремы (метатеоремы) у Клини соответствуют критериям у Бурбаки, а формальные теоремы - теоремам, предложениям, леммам.