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

[beroal]

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

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

Мне показалось, вы считаете, что горизонтальная черта обозначает отношение в метатеории? Я считаю, это символ в метатеории, символ языка описания систем вывода. Горизонтальная черта не обозначает отношения.

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

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

Вы правы, у Мендельсона доказана модифицированная формулировка теоремы о дедукции. Кстати, в формулировке затрагивается вывод (список, а не дерево вывода, но это детали).

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

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

Для тех, кто пишет доказательства на формальных языках, это как раз обычная форма. Надо же как-то записывать вывод. Каждая система вывода порождает множество деревьев вывода.

[epros]

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

Мне показалось, вы считаете, что горизонтальная черта обозначает отношение в метатеории? Я считаю, это символ в метатеории, символ языка описания систем вывода. Горизонтальная черта не обозначает отношения.

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

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

Для тех, кто пишет доказательства на формальных языках, это как раз обычная форма. Надо же как-то записывать вывод. Каждая система вывода порождает множество деревьев вывода.

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

[arseniiv]

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

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

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

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

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

Но это не то же отношение, что выводимость из нескольких правил вывода за произвольное число шагов. Поэтому некоторые могут для выводимости за один шаг и, возможно, по ровно одному правилу, использовать только черту, а для выводимости за произвольное — $\vdash$. Даже если использовать $\vdash$ для обеих вещей, это на деле будут два омонима.

-- Чт авг 31, 2017 19:21:07 --

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

Можете считать линейную форму просто видом записи дерева

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

[epros]

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

Но это не то же отношение, что выводимость из нескольких правил вывода за произвольное число шагов. Поэтому некоторые могут для выводимости за один шаг и, возможно, по ровно одному правилу, использовать только черту, а для выводимости за произвольное — $\vdash$. Даже если использовать $\vdash$ для обеих вещей, это на деле будут два омонима.

Угу, выводимое за один шаг и выводимое вообще - не одно и то же. Если хочется подчеркнуть различие между ними, то ничто не мешает для первого ввести отдельный предикатный символ. Но с учётом того, что второе является транзитивным замыканием первого, можно этим не заморачиваться.

[beroal]

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

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

Надо уточнить, удобнее для чего: для теории или для практики.

Насчёт практики. Мне иногда приходится читать и писать доказательства в виде списка. Если элемент этого списка есть применение правила вывода, то ссылки на посылки обозначаются числами, и я должен искать строки с этими числами в списке выше. Это отвлекает от смысла доказательства и отнимает время. Если доказательство изображено в виде дерева, я веду глазами по линиям дерева. Пример из другой области: программы. Хотя программы записываются текстом, программисты лепят из них деревья с помощью отступов. Целые религии из этого возникли: синтаксис Лисп, на какой строке ставить открывающие фигурные скобки в Си. «Миллионы леммингов не могут ошибаться». Ну, не буду давить. Это просто разница предпочтений.

Насчёт теории. Можно делать рекурсию по натуральному числу, по списку, по дереву (структурная рекурсия).

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

Можете считать линейную форму просто видом записи дерева, так же как формулы и термы—строки видами записи соответствующих деревьями.

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

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

Угу, выводимое за один шаг и выводимое вообще - не одно и то же.

Вот, это я подразумевал.

-- Fri Sep 01, 2017 13:20:51 --

Насчёт того, всё ли в порядке с правилом Gen.

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

Когда гильбертовская система изучается с помощью метатеории, вводится понятие «вывод с гипотезами». Тогда возникает вопрос, какую логически общезначимую формулу или выводимую формулу он обосновывает. Если ничего не обосновывает, тогда почему он позволен? В логике высказываний любой вывод с гипотезами транслируется в выводимую формулу с помощью теоремы дедукции. Теорема дедукции для логики предикатов, цитата из учебника Мендельсона (6-е английское издание):

Цитата:

Предположим, что в некотором выводе, показывающем, что \(\Gamma,\mathscr{B}\vdash\mathscr{C} \), никакое применение Gen к формуле, которая зависит от \(\mathscr{B}\), не связывает квантором никакую свободную переменную формулы \(\mathscr{B}\). Тогда \(\Gamma\vdash\mathscr{B}\Rightarrow\mathscr{C} \).

Например, вывод \([A(x), \forall x A(x)]\) не годится для этой теоремы, потому что \(\forall x A(x)\) выведен с помощью Gen из \(A(x)\), и это правило связало квантором переменную \(x\), которая свободна в гипотезе \(A(x)\), и \(A(x)\), разумеется, зависит от \(A(x)\). Не проблема, выведем гипотезу \(A(x)\) с помощью аксиомы instantiation: \([\forall x A(x), A(x)]\). То есть гипотеза \(A(x)\) исчезла, возникла гипотеза \(\forall x A(x)\). Этот модифицированный вывод пригоден для теоремы дедукции. Применяя её, находим формулу, которую обосновывает модифицированный вывод.

То есть, если обернуть в квантор всеобщности все свободные переменные гипотез, которые связываются квантором при применении Gen, то получится выводимая формула даже из негодного вывода. Даже трудно сказать, что с выводом не в порядке.

[arseniiv]

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

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

Если бы все правила вывода имели по одной посылке, то чуть сложнее — надо сначала объединить отношения выводимости за шаг всех правил вывода, а уж потом замыкать, притом не только транзитивно, но и рефлексивно. А если разное число посылок, тут ещё придётся и дальше пилить.

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

потому что напечатан всё-таки текст, техника пока не дошла до печати деревьев

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

[gefest_md]

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

Почему недостаточно одого правила modus ponens?

Информация: в книге Мендельсона, в упражнении 2 на странице 71 приводится пример теории первого порядка, у которой из правил вывода есть только modus ponens. И эта теория имеет такие же теоремы, как и обычная теория с правилами MP и Gen.