Как доказать невыводимость используя правила вывода?

[creative]

Есть вопрос по аксиоматическому методу. В § 10 первой главы (исчисление высказываний) в книге Гильберта, Аккермана "Основы теоретической логики" даны следующие аксиомы исчисления высказываний:

$ a) X \vee X \rightarrow X $
$ b) X \rightarrow X \vee Y $
$ c) X \vee Y \rightarrow Y \vee X $
$ d) (X \rightarrow Y) \rightarrow [Z \vee X \rightarrow Z \vee Y] $

Правила вывода новых формул:

$ \alpha) $ Правило подстановки

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

$ \beta) $ Схема заключения

Из двух формул $\mathfrak{A}$ и $\mathfrak{A} \rightarrow \mathfrak{B}$ получаем новую формулу $\mathfrak{B}$.

(это Modus ponens)

Эта система аксиом непротиворечива (доказательство в § 12), каждая аксиома независима (доказательство в § 13) и полна (доказательство в § 13).

Вопрос: Как можно только с помощью этих аксиом и правил вывода показать невыводимость какой либо формулы? Например, как показать только с помощью аксиом и этих правил вывода, что $X$ или $\neg (\neg X \vee \neg Y)$ или $X \vee Y$ невыводимы? Если это показать невозможно используя только эти аксиомы и правила вывода, то как доказать точно, что это невозможно в общем случае для этой системы?

[Xaositect]

Хм.
С помощью аксиом и правил вывода выводят формулы. А содержательные теоремы доказывают, исследуя аксиомы и правила вывода.
Например, можно построить интерпретацию, где все выводимые формулы относятся к одному классу, а наша формула - к другому.
В данном случае, понятное дело, можно взять классическую булеву интерпретацию - любая аксиома у нас является тавтологией, подстановка и MP тавтологичность сохраняют, а $X$ или $X\vee Y$ тавтологиями не являются.

[epros]

Хм. Как вообще можно утверждать непротиворечивость этой системы, если в ней нет символа отрицания? Тут явно чего-то не хватает в постановке задачи...

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

[creative]

Xaositect

Если я правильно понял Вас, то одна из таких интерпретаций это приведение к совершенной конъюнктивной нормальной форме следствия и всех аксиом (отдельная СКНФ следствия и отдельная СКНФ всех аксиом). И если СКНФ следствия содержит конъюнктивный член, который не встречается в СКНФ всех аксиом (аксиомы приводим к СКНФ предварительно записывая всех их через $\wedge$), то получается возможной та ситуация, когда СКНФ аксиом истинно, а СКНФ следствия ложно, что по определению импликации является ложью. Из чего можно сделать вывод, что следствие невыводимо из этих аксиом. Этот метод был дан в § 9 "Систематический обзор всех следствий из данных посылок".
А приведение к СКНФ как было показано в § 11 можно выполнить используя эти аксиомы.

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

epros

Там есть отрицание, $X \rightarrow Y$ есть краткая запись формулы $\neg X \vee Y$. Об этом специально упоминается § 10.

[epros]

creative в сообщении #408230 писал(а):

epros

Там есть отрицание, $X \rightarrow Y$ есть краткая запись формулы $\neg X \vee Y$. Об этом специально упоминается § 10.

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

[creative]

epros

У Гильберта, Аккермана даны только эти аксиомы, а символы $\wedge$, $\rightarrow$ являются лишь чисто символически сокращенной записью формул с использованием символов $\vee$ и $\neg$. То есть подразумевается как если бы я на бумаге писал и для какой-то комбинации символов внес бы новый символ.
Считайте, что эти аксиомы записаны первоначально только с $\vee$ и $\neg$.

[epros]

Подразумевать можно что угодно. Например, я могу подразумевать, что у нас двоичная логика, откуда автоматически следуют все тавтологии классического исчисления высказываний, так что приведённые Вами четыре аксиомы и два правила вывода становятся вообще излишними. Но Вы же определяете формальную систему, а поэтому все аксиомы и правила должны быть определены явно. Ибо во многих формальных системах (например, в интуиционистском исчислении высказываний) $\neg A \lor B$ и $A \rightarrow B$ отнюдь не эквивалентны.

[Maslov]

creative в сообщении #408213 писал(а):

Например, как показать только с помощью аксиом и этих правил вывода, что $X$ или $\neg (\neg X \vee \neg Y)$ или $X \vee Y$ невыводимы?

Я думаю, можно предположить, что формула выводима, и попробовать придти к противоречию.

Например, допустим, что из исходных аксиом выводима формула $X$

Подставим вместо $X$ формулу $\lnot (X \lor X \to X)$:
$\vdash \lnot (X \lor X \to X)$

В то же время, по аксиоме 1
$\vdash X \lor X \to X$

Т. о., предположив выводимость $X$, мы в нашей теории вывели некоторую формулу и её отрицание. Другими словами, наша исходная теория противоречива. Но она непротиворечива, а значит формула $X$ невыводима.

-- Ср фев 02, 2011 16:50:40 --

А ещё проще, предположив выводимость $X$, подставить вместо $X$ формулу $\lnot X$.

[creative]

Maslov

Но так же мы на словах неявно используем правило вывода reductio ad absurdum:

$( \neg P \rightarrow (R \wedge \neg R) ) \vdash P$

А у здесь у нас в распоряжении только modus ponens.

[Maslov]

creative в сообщении #408286 писал(а):

Но так же мы на словах неявно используем правило вывода reductio ad absurdum:

Во-первых, правило reducio ad absurdum выводимо из аксиом с помощью MP, поэтому использовать его можно.

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

Но, честно говоря, это всё равно не строгое (в Вашем смысле) доказательство: мы существенно пользуемся непротиворечивостью, которая доказывается с использованием интерпретации. А если можно пользоваться интерпретацией, то для доказательства невыводимости некоторой формулы проще убедиться, что она не является тавтологией (Xaositect об этом писал здесь: post408224.html#p408224)

[creative]

Maslov

Да они похожи, а как именно выводится reductio ad absurdum с помощью modus ponens?
Просто тут возникает вопрос, чем именно отличаются правила вывода от аксиом (интуитивно понятно, что для вывода новых формул, но это не строгое поонимание)?

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

[Dialectic]

creative в сообщении #408286 писал(а):

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

При помощи аксиом и правил вывода мы можем только выводить строчки. Вот какие выведем - такие и выведем.
А вот если мы хотим "обозреть" данную систему как некое "единое целое", включая её правила вывода, мы должны "выпрыгнуть" из языка системы, в другую область - в метаязык. Мы рассуждаем о системе, на другом языке - на метаязыке, в данном случае - на русском.
Так вот: если мы говорим об исчислении высказываний, то там резрешающий алгоритм - довольно прост: чтобы узнать какая формула там выводима, нужно взять эту формулу и проверить: является ли она тавтологией алгебры высказываний или нет. Если является, то несомненно она и выводима. Это значит, что тупо строча по этим правилам - мы несомненно на неё наткнёмся рано или поздно, поскольку все тавтологии выводимы, и не одна не тавтология - не выводима. А что касается "ипосльзую только эти аксиомы" - то эти "только эти аксиомы" - просто тупые правила, за рамки которых выходить никогда нельзя. ТОлько расуждая о самих правилах из вне - мы можем что-то доказать или опровергнуть касательно свойств самих этих аксиом или правил вывода. Лично я так понимаю дело.

-- Ср фев 02, 2011 20:38:52 --

creative в сообщении #408308 писал(а):

Maslov
Да они похожи, а как именно выводится reductio ad absurdum с помощью modus ponens?

Если reductio ad absurdum - тавтология, то она выводится. А как ... это уже другой вопрос... Вы вот попробуйте вывести формулу: A-->A. Из этих аксиом...

creative в сообщении #408308 писал(а):

[b]
Просто тут возникает вопрос, чем именно отличаются правила вывода от аксиом (интуитивно понятно, что для вывода новых формул, но это не строгое поонимание)?

Вcе те аксиомы а-d - аксиомами не являются. Эта схема которая "штампует" нам аксиомы, некий "шаблон" по которому делается аксиома. Так что в вашей системе - аксиом - бесконечное множество. Правило вывода, это просто механическое правило, как по одним формулам штамповать другие. Последние именуются в этом случае "теоремами".

creative в сообщении #408308 писал(а):

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

ДаГ в том то и дело - что можно. Но "суждение" - это не есть тупое, бездумное "штампование" .Это Вы уже начинаете смотреть на аксиомы как бы из вне, и тем самым уже они существуют у Вас (лично у вас) в сознании - вместе с некоторым значением. А сами по себе - они ничего не значат, кроме тупых сцеплений знаков. У нас и аксиом та никаких в вашем понимании - нет .У нас есть только сцепления знаков, более - ничего. Аксиома - эт отоже чистой воды сцепление знаков, оно бессодержательное само по себе. Каждая аксиома нечет столько же смысла сколько например строчка: "HKkhh*&6899;ds/x'@!24%". И правила вывода, тоже в некотором роде - нечто "техническое", способное реализовываться на компе.

[Xaositect]

Dialectic в сообщении #408310 писал(а):

Вcе те аксиомы а-d - аксиомами не являются. Эта схема которая "штампует" нам аксиомы, некий "шаблон" по которому делается аксиома. Так что в вашей системе - аксиом - бесконечное множество. Правило вывода, это просто механическое правило, как по одним формулам штамповать другие. Последние именуются в этом случае "теоремами".

Эти аксиомы как раз являются аксиомами, "штамповка" здесь обеспечивается правилом подстановки.

[Dialectic]

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

Dialectic в сообщении #408310 писал(а):

Вcе те аксиомы а-d - аксиомами не являются. Эта схема которая "штампует" нам аксиомы, некий "шаблон" по которому делается аксиома. Так что в вашей системе - аксиом - бесконечное множество. Правило вывода, это просто механическое правило, как по одним формулам штамповать другие. Последние именуются в этом случае "теоремами".

Эти аксиомы как раз являются аксиомами, "штамповка" здесь обеспечивается правилом подстановки.

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

[Maslov]

creative в сообщении #408308 писал(а):

а как именно выводится reductio ad absurdum с помощью modus ponens?

Посмотрите доказательство правила введения отрицания в (почти) любом учебнике по мат. логике. В Игошине (издание 2008 г) это теорема 15.9 п. г).

creative в сообщении #408308 писал(а):

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

Честно говоря, не знаю.