Почему обобщение определяется правилом вывода?

[gefest_md]

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

чтобы существовал вывод, в котором обобщение не применялось к свободным переменным посылки, которую мы собираемся «перенести вправо», и чтобы оно также не применялось к формулам, вывод которых зависит от неё.

Значит я предположил, что существует вывод формулы $\forall x(x=1)$ из допущения $x=1$, которое в этом выводе может используется, а может нет.

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

почему это не работает для "если $\vdash x=1$, то $\vdash \forall x~(x=1)$".

Можно так объяснить. Неверно, что $\models x=1$ (не тавтология). Таблица истинности не дает только истина. Поэтому неверно, что $\vdash x=1$ (теорема о непротиворечивости).

-- Вс авг 27, 2017 22:43:07 --

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

Под $T$ и имеется в виду множество формул -. аксиом некой теории. Зачем их переписывать в варианте с чертой? Ясно же, что когда над чертой пишут $\varphi$, то имеют в виду формулу, выводимую из аксиом некой теории. Или Вы не согласны?

Аксиомы вообще не пишу слева от $\vdash$. Только простые допущения. Я имел в виду, что первый вариант и вариант с чертой это две формы записи одного и того же. Поэтому $T$ не должен быть в одном варианте и не быть в другом.

[epros]

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

epros
Ну вот выразите правило обобщения через правила Бернайса и остальное, и все необходимые ограничения должны явиться сами собой.

У Верещагина и Шеня всё это проделано, но чтобы появились ограничения что-то незаметно. В правилах Бернайса было ограничение (одна из формул не должна содержать соответствующую переменную). Но потом эта формула выбрана тождественно истинной и из правила обобщения ограничение выпало.

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

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

О! Вот она, сермяжная правда, где-то тут. Поскольку теорема дедукции формулируется для вывода, важно, что понимается под "выводом". Если она формулировалась для вывода с помощью только modus ponens, то к выводу с использованием правила обобщения может быть и неприменима.

Вообще-то хотелось бы всякие "в зависимости от того, как понимать" исключить. Понимание должно быть однозначным.

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

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

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

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

Насколько я помню книгу Верещагина и Шеня (Верещагин подарил мне экземпляр), там всё изложено хорошо, кроме одного ляпа в главе про нестандартный анализ.

Речь не о ляпах. Просто в отношении правила обобщения имеет место какая-то недосказанность, с которой хотелось бы разобраться.

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

gefest_md в сообщении #1243564 писал(а):

Можно так объяснить. Неверно, что $\models x=1$ (не тавтология). Таблица истинности не дает только истина. Поэтому неверно, что $\vdash x=1$ (теорема о непротиворечивости).

Ну и что? Выражение "если ... то ..." означает условный вывод, разве нет? А к условному выводу и применяется теорема дедукции.

gefest_md в сообщении #1243564 писал(а):

Аксиомы вообще не пишу слева от $\vdash$. Только простые допущения.

Какая разница? Аксиомы - это условные допущения, при которых верны выводы соответствующей теории.

gefest_md в сообщении #1243564 писал(а):

Я имел в виду, что первый вариант и вариант с чертой это две формы записи одного и того же. Поэтому $T$ не должен быть в одном варианте и не быть в другом.

Намеренное исключение аксиом слева от $\vdash$ меняет смысл правила - делает его общезначимым, вместо применения в конкретном контексте. Например, я бы записал теорему дедукции так:

$(T, A \vdash B) \vdash (T \vdash A \to B)$

Исключив $T$, получим:

$(A \vdash B) \vdash A \to B$

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

[arseniiv]

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

Вообще-то хотелось бы всякие "в зависимости от того, как понимать" исключить. Понимание должно быть однозначным.

Но ни один из выборов, насколько понимаю, не считается более естественным. Выводы менее ограничены — теорему придётся, теорема — выводы, и ограничения в обоих случаях довольно простые, чтобы легко предпочесть один другому.

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

Я подозреваю, что у натуральной дедукции проблем гораздо больше, поэтому остерегаюсь туда лезть.

Я сам в ней немного плаваю, но проблемой можно было бы назвать разве что представление выводов хитрого вида деревьями (хитрее, чем в гильбертовском исчислении), которые, однако, всё равно можно «линеаризовать». Ещё метапроблемой может быть то, что освещается она, видимо, в меньшем числе книг, и выбор подробного начального учебника может оказаться не таким широким. Но если оценивать с потолка, это должна быть вторая по популярности система.

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

Так что лучше уж иметь дело с чётко зафиксированным небольшим количеством правил вывода, а остальное выражать аксиомами.

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

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

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

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

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

Исключив $T$, получим:

$(A \vdash B) \vdash A \to B$

Точнее, $(A \vdash B) \vdash (\vdash A \to B)$. А то у вас от опечатки метауровни смешались.

[epros]

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

По-моему, это не особо обоснованно. Аксиома — это то же правило вывода с нулём посылок.

Всякая аксиома - правило вывода, но не всякое правило вывода - аксиома.

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

Точнее, $(A \vdash B) \vdash (\vdash A \to B)$. А то у вас от опечатки метауровни смешались.

Думаете, есть разница? Вроде бы, если перед $\vdash$ пусто, то $\vdash$ можно смело выкидывать. Да, это понижает уровень "мета" на единицу. Но это имеет понятное объяснение: Если мета-теория считает, что нечто "выводимо" без всяких условий, значит она принимает это нечто за свою собственную аксиому.

[george66]

Давайте знак $\vdash$ употреблять в каком-то одном смысле. Я подумал: они действительно записывают правило обобщения в виде $\varphi(x)\vdash\forall x\varphi(x)$? Если да, то это редкое употребление $\vdash$, обычно тут ставят вертикальную черту. В книжку лезть мне мучительно лень.

-- 28.08.2017, 22:01 --

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

[arseniiv]

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

Думаете, есть разница? Вроде бы, если перед $\vdash$ пусто, то $\vdash$ можно смело выкидывать. Да, это понижает уровень "мета" на единицу.

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

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

Если мета-теория считает, что нечто "выводимо" без всяких условий, значит она принимает это нечто за свою собственную аксиому.

Это бессмысленно и/или неверно (выбирайте на вкус). У вас же был вроде неплохой такой уровень, куда он делся?

[george66]

Объясняю через соответствие Галуа. Для каждого конечного списка переменных $x_1,x_2\ldots x_n$ (для краткости $\Gamma$, такие списки будем называть контекстами) рассмотрим множество всех формул, свободные переменные которых содержатся в списке $\Gamma$. Для $\Gamma=(x,y)$ это будет множество всех формул, содержащих в качестве свободных переменных только $x$ и $y$ (не обязательно все, переменные могут быть фиктивными). На каждом таком множестве формул задан порядок по включению (задаваемых формулами множеств) $\subseteq$, самой маленькой будет формула $\bot$, а самой большой формула $\top$. Есть монотонная операция добавления фиктивной переменной, по формуле $\varphi$ над контекстом $\Gamma=(x_1,x_2\ldots x_n)$ она выдаёт ту же формулу, рассматриваемую как формула над контекстом $\Gamma,y=(x_1,x_2\ldots x_n,y)$, для удобства обозначим эту формулу $\varphi_y$ (формула $\varphi$, к которой фиктивно добавлена свободная переменная $y$). Операция $\forall y$, наоборот, по формуле над контекстом $\Gamma,y$ выдаёт формулу над контекстом $\Gamma$ и является правой сопряжённой к добавлению фиктивной переменной, что выражается условием
$\varphi_y\subseteq\psi$ если и только если $\varphi\subseteq\forall y\psi$, где $\varphi$ над контекстом $\Gamma$, а $\psi$ над контекстом $\Gamma,y$
Если порядок обозначить штопором, получаем
$\varphi_y\vdash\psi$ если и только если $\varphi\vdash\forall y\psi$

[epros]

arseniiv, а как Вы относитесь к записи $(T \vdash A) \to A$, которой, судя по некоторым признакам, выражается "semantic consistency" теории $T$ с точки зрения мета-теории?

Как Вы понимаете, это не то же самое, что синтаксическая непротиворечивость, которую можно выразить как $\neg ((T \vdash A) \land (T \vdash \neg A))$.

george66, Ваши сообщения ещё почитаю повнимательнее попозже.

[Xaositect]

Semantic consistency это же $(T\vdash A) \to (\vDash A)$.

[epros]

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

Semantic consistency это же $(T\vdash A) \to (\vDash A)$.

Хм. Может я туплю сейчас, но мне казалось, что $\vdash A$ означает выводимость исключительно из логических аксиом, в то время как утверждение в мета-теории $A$ означает, что оно выведено из аксиом мета-теории.

И правильно ли я понимаю, что Гёделевское утверждение о том, что построенное им предложение $G$ утверждает собственную недоказуемость в теории $T$, тоже нужно записать как $\neg (T \vdash G) \leftrightarrow (\vdash G)$? Исключительно ради "не смешивания мета-уровней"?

Просто мне этот символ $\vdash$ представляется совершенно лишним, ибо $(\vdash A) \to A$ (но неверно, что $A \to (\vdash A)$). И вот я смотрю статью википедии Propositional calculus, нахожу там правило Conditional proof и вижу, что авторы статьи разделяют моё мнение (о том, что данный символ лишний).

[Xaositect]

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

Хм. Может я туплю сейчас, но мне казалось, что $\vdash A$ означает выводимость исключительно из логических аксиом, в то время как утверждение в мета-теории $A$ означает, что оно выведено из аксиом мета-теории.

Да. А что мы понимаем под semantic consistency? Это же вроде существование модели?

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

И правильно ли я понимаю, что Гёделевское утверждение о том, что построенное им предложение $G$ утверждает собственную недоказуемость в теории $T$, тоже нужно записать как $\neg (T \vdash G) \leftrightarrow (\vdash G)$? Исключительно ради "не смешивания мета-уровней"?

Нет, в теореме Геделя как раз уровни смешиваются, $G \leftrightarrow \neg (PA \vdash G)$.

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

Просто мне этот символ $\vdash$ представляется совершенно лишним, ибо $(\vdash A) \to A$

Это может быть неверно, см. теорему Лёба.

[epros]

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

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

Хм. Может я туплю сейчас, но мне казалось, что $\vdash A$ означает выводимость исключительно из логических аксиом, в то время как утверждение в мета-теории $A$ означает, что оно выведено из аксиом мета-теории.

Да. А что мы понимаем под semantic consistency? Это же вроде существование модели?

Ну так существование модели же доказывается с использованием аксиоматики мета-теории. Так что если Ваше "да" означает согласие с моим предположением, что $\vdash A$ означает выводимость исключительно из логических аксиом, то $(T \vdash A) \to (\vdash A)$ никак не может означать semantic consistency теории T, ибо означает всего лишь, что теория T не содержит ничего, кроме общезначимых утверждений.

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

Нет, в теореме Геделя как раз уровни смешиваются, $G \leftrightarrow \neg (PA \vdash G)$.

Ну так истинность $G$ вроде бы доказывается отсюда как раз с использованием $(PA \vdash G) \to G$: Предположим, что $PA \vdash G$, отсюда $G$, отсюда $\neg (PA \vdash G)$, противоречие. Значит $\neg (PA \vdash G)$, значит $G$.

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

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

Это может быть неверно, см. теорему Лёба.

Это если интерпретировать $\vdash A$ как доказуемость в мета-теории. А я полагаю, что оно должно означать выводимость только из логических аксиом. Ибо очень странно, если убрав $B$ из $B \vdash A$, мы расширяем объём выводимых $A$.

[Xaositect]

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

Ну так существование модели же доказывается с использованием аксиоматики мета-теории. Так что если Ваше "да" означает согласие с моим предположением, что $\vdash A$ означает выводимость исключительно из логических аксиом, то $(T \vdash A) \to (\vdash A)$ никак не может означать semantic consistency теории T, ибо означает всего лишь, что теория T не содержит ничего, кроме общезначимых утверждений.

У меня там не $\vdash$, а $\vDash$. Модель, конечно, надо было сделать явной, $\exists M\, (T\vdash A \to M\vDash A)$

[beroal]

Цитата:

Формула \(A\) выводима из \(\Gamma\), если существует вывод \(\Gamma\), в которой она является последней формулой. В этом случае мы пишем \(A\vdash\Gamma\).

Цитата из учебника Верещагина и Шеня. То есть \(\vdash\) обозначает отношение в метатеории.

На странице «Universal generalization» Википедии \(\vdash\) — это символ секвенции, то есть символ объектного языка. Поэтому там требуют, чтобы \(y\) не встречалось в \(\Gamma\).

На странице «List of rules of inference» Википедии:

Цитата:

Restriction 2: \(\beta\) is not mentioned in any hypothesis or undischarged assumptions.

В учебникe Верещагина и Шеня система вывода гильбертовская, в ней нет гипотез. Я думаю, правило Gen кажется странным именно потому, что оно корректно только в такой «неестественной» системе вывода.

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

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

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

Теорема в арифметике Пеано: \(\forall y(x\leq y)\to x=0\).

[epros]

Xaositect, извините, что сразу не смог ответить. Теперь я понял, что Вы хотели сказать. Квантор существования сильно помог, ибо без него я читал это как "всё доказуемое в теории - общезначимо".

Да, это consistency в смысле теории моделей. Просто я говорил немного о другой семантике - той, с точки зрения которой "правда всегда одна". В том смысле, в котором Гёдель говорил об "истинности" арифметических формул - не "в некоторой модели", а "в принципе".

В общем, всё это было сказано только в обоснование того, что в смешивании мета-уровней нет криминала.

beroal в сообщении #1244002 писал(а):

То есть \(\vdash\) обозначает отношение в метатеории.

Это понятно. Вопрос в том, что это отношение (выводимости) может пониматься по-разному в зависимости от того, какие правила вывода приняты.

P.S. А выражать ли это символом $\vdash$ или горизонтальной чертой, по-моему, вопрос только удобства. Мне вот многоэтажные выражения кажутся неудобными.

beroal в сообщении #1244002 писал(а):

В учебникe Верещагина и Шеня система вывода гильбертовская, в ней нет гипотез. Я думаю, правило Gen кажется странным именно потому, что оно корректно только в такой «неестественной» системе вывода.

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

beroal в сообщении #1244002 писал(а):

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

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