Пусть $%A \vdash B$%, причём существует вывод формулы $%B$% из гипотезы $%A$% длины $%n$% (длина вывода — количество формул в выводе). Требуется доказать, что существует вывод $%A \to B$% длины не больше $%3n+4$%.

задан 5 Сен '15 21:39

изменен 9 Сен '15 22:53

Аксиом всего три, а правилом вывода является modus ponens.

(5 Сен '15 21:41) Poncho
10|600 символов нужно символов осталось
2

Мне кажется, здесь можно $%3n+4$% заменить на $%3n+2$%.

Если $%n=1$%, то $%B$% совпадает с $%A$%. Согласно Лемме 1.7 из учебника Мендельсона, существует вывод тавтологии $%A\to A$% за 5 шагов. Далее по индукции доказываем, что для любого вывода $%B_1$%, ... , $%B_n$% формулы $%B$% из $%A$%, существует вывод длиной не более $%3n+2$%, содержащий все формулы вида $%A\to B_i$%, где $%1\le i\le n$%.

Используя соображения из доказательства теоремы дедукции, рассмотрим переход от $%n$% к $%n+1$%, и покажем, что он требует не более трёх дополнительных формул для вывода импликации $%A\to B_{n+1}$%. Пусть далее $%B_{n+1}=B$% для краткости.

Вывод формулы $%A\to A$% у нас уже имеется, поэтому случай $%B=A$% можно не рассматривать. Если $%B$% является аксиомой, то добавляем $%B$% в наш вывод, а также добавляем следствие схемы аксиом (A1) вида $%B\to(A\to B)$%. По modus ponens отсюда получается $%A\to B$%; это третья добавляемая формула.

Пусть $%B$% следует по modus ponens из каких-то предыдущих формул исходного вывода. Они имеют вид $%C$% и $%C\to B$%. Преобразованный вывод содержит формулы $%A\to C$% и $%A\to(C\to B)$% в силу предположения индукции. По схеме аксиом (A2), добавляем в вывод формулу $%(A\to(C\to B))\to((A\to C)\to(A\to B))$%. Далее дважды применяем modus ponens, выводя $%A\to B$%, что требует добавления ещё двух формул. В итоге получается то, что требовалось.

ссылка

отвечен 5 Сен '15 22:53

10|600 символов нужно символов осталось
Ваш ответ

Если вы не нашли ответ, задайте вопрос.

Здравствуйте

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

Присоединяйтесь!

отмечен:

×664
×28
×24

задан
5 Сен '15 21:39

показан
1030 раз

обновлен
9 Сен '15 22:53

Отслеживать вопрос

по почте:

Зарегистрировавшись, вы сможете подписаться на любые обновления

по RSS:

Ответы

Ответы и Комментарии

Дизайн сайта/логотип © «Сеть Знаний». Контент распространяется под лицензией cc by-sa 3.0 с обязательным указанием авторства.
Рейтинг@Mail.ru