2014 dxdy logo

Научный форум dxdy

Математика, Физика, Computer Science, Machine Learning, LaTeX, Механика и Техника, Химия,
Биология и Медицина, Экономика и Финансовая Математика, Гуманитарные науки


Правила форума


Посмотреть правила форума



Начать новую тему Ответить на тему На страницу Пред.  1, 2, 3  След.
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение27.08.2017, 23:01 
Аватара пользователя


01/12/06
697
рм
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$ не должен быть в одном варианте и не быть в другом.

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение28.08.2017, 11:14 
Заслуженный участник
Аватара пользователя


28/09/06
10414
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$

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

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение28.08.2017, 14:58 
Заслуженный участник


27/04/09
28128
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)$. А то у вас от опечатки метауровни смешались.

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение28.08.2017, 20:39 
Заслуженный участник
Аватара пользователя


28/09/06
10414
arseniiv в сообщении #1243624 писал(а):
По-моему, это не особо обоснованно. Аксиома — это то же правило вывода с нулём посылок.

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

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

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

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение28.08.2017, 21:58 
Заслуженный участник


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

-- 28.08.2017, 22:01 --

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

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение28.08.2017, 22:39 
Заслуженный участник


27/04/09
28128
epros в сообщении #1243692 писал(а):
Думаете, есть разница? Вроде бы, если перед $\vdash$ пусто, то $\vdash$ можно смело выкидывать. Да, это понижает уровень "мета" на единицу.
И, значит, разница есть. Ибо формулы теории принадлежат к множеству, которое даже не может пересекаться с множеством формул метатеории, потому что. Ну, вы должны понимать.

epros в сообщении #1243692 писал(а):
Если мета-теория считает, что нечто "выводимо" без всяких условий, значит она принимает это нечто за свою собственную аксиому.
Это бессмысленно и/или неверно (выбирайте на вкус). У вас же был вроде неплохой такой уровень, куда он делся? :|

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение29.08.2017, 01:56 
Заслуженный участник


31/12/15
922
Объясняю через соответствие Галуа. Для каждого конечного списка переменных $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$

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение29.08.2017, 12:21 
Заслуженный участник
Аватара пользователя


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

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

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

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение29.08.2017, 12:50 
Заслуженный участник
Аватара пользователя


06/10/08
6422
Semantic consistency это же $(T\vdash A) \to (\vDash A)$.

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение29.08.2017, 14:44 
Заслуженный участник
Аватара пользователя


28/09/06
10414
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 и вижу, что авторы статьи разделяют моё мнение (о том, что данный символ лишний).

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение29.08.2017, 15:29 
Заслуженный участник
Аватара пользователя


06/10/08
6422
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$
Это может быть неверно, см. теорему Лёба.

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение30.08.2017, 11:25 
Заслуженный участник
Аватара пользователя


28/09/06
10414
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$.

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение30.08.2017, 11:39 
Заслуженный участник
Аватара пользователя


06/10/08
6422
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)$

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение30.08.2017, 22:38 
Аватара пользователя


17/04/11
658
Ukraine
Цитата:
Формула \(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\).

 Профиль  
                  
 
 Re: Почему обобщение определяется правилом вывода?
Сообщение31.08.2017, 11:01 
Заслуженный участник
Аватара пользователя


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

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

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

beroal в сообщении #1244002 писал(а):
То есть \(\vdash\) обозначает отношение в метатеории.
Это понятно. Вопрос в том, что это отношение (выводимости) может пониматься по-разному в зависимости от того, какие правила вывода приняты.

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

beroal в сообщении #1244002 писал(а):
В учебникe Верещагина и Шеня система вывода гильбертовская, в ней нет гипотез. Я думаю, правило Gen кажется странным именно потому, что оно корректно только в такой «неестественной» системе вывода.
Не просто нет гипотез, а нет дедукции как явления. Потому что с правилом обобщения в такой формулировке теорема дедукции, как я понимаю, становится недоказуемой. А чтобы она стала доказуемой необходимо накладывать ограничения на условный вывод с участием правила обобщения.

beroal в сообщении #1244002 писал(а):
В учебнике Мендельсона (который я сейчас читаю), в учебнике Колмогорова и Драгалина правило Gen изложено так же.
У Колмогорова и Драгалина под выводом понимается некое дерево, что является довольно необычной формой изложения логики и некоторым образом меня отпугивает. К тому же я не хочу ничего слышать про семантику, по крайней мере до тех пор, пока не станет всё ясно с синтаксисом.

 Профиль  
                  
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 37 ]  На страницу Пред.  1, 2, 3  След.

Модераторы: Модераторы Математики, Супермодераторы



Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group