Не опираясь на теорему о полноте, докажите выводимость формулы (¬A ∨ B ∨ ¬C) ↔ ((A → C) → ((B →C) → (A → B))) в исчислении высказываний.

Скажите, пожалуйста, как это сделать?

$$\begin{array}{l} A \to (B\to A), \\ (A \to (B \to C)) \to ((A \to B) \to (A \to C)), \\ A \wedge B \to A, \\ A \wedge B \to B, \\ A \to (B \to (A \wedge B)), \\ A \to A \vee B, \\ B \to A \vee B, \\ (A \to C) \to ((B \to C) \to (A \vee B \to C)), \\ (A \to B) \to ((A \to \neg B) \to \neg A), \\ \neg\neg A \to A. \end{array}$$

задан 15 Окт 22:08

изменен 16 Окт 2:21

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

(15 Окт 22:42) falcao

@falcao, в том то и дело, что я не забыл указать, это полное условие задачи. Следовательно, можно выбрать любую версию исчисления высказываний.

(15 Окт 22:56) Pointer

@Pointer: так не бывает, и я выбирать ничего не должен. Вы изучаете курс, в рамках которого Вам дают одну или несколько версий ИВ. Потом в контексте этого даются задачи с таким вот "полным" условием. Но в предположении, что слушатель знает контекст. Который всегда нужно давать вместе с формулировкой.

Если я сам вправе задавать любое исчисление, то я объявлю данную формулу аксиомой, и вуаля! :)

(15 Окт 23:34) falcao

@falcao, я ни в коем случае не хотел вызвать данную реакцию на мой комментарий, но я правда не знаю в какой версии исчисления высказываний нужно доказывать выводимость этой формулы.

(16 Окт 0:07) Pointer

@Pointer: значит, надо уточнить условие, то есть понять, что же тут изучается :) Как я понимаю, задача не существует сама по себе -- это приложение к какому-то лекционному материалу.

Здесь очень часто спрашивают про исчисление L из учебника Мендельсона, но там дизъюнкция не используется. Не говоря о том, что дизъюнкция трёх выражений -- это не формула, и так далее. Там должен быть строгий язык, как в программировании.

(16 Окт 0:54) falcao

@falcao, я уточню и обращусь повторно.

(16 Окт 1:12) Pointer

@falcao, рискну предположить, что имеется ввиду теория N

(16 Окт 1:27) haosfortum

@haosfortum: что это?

(16 Окт 1:59) falcao

@falcao, кажется, я Вас ввел в заблуждение. Так называлась на моем курсе теория, содержащая 11 определенных схем аксиом. Я подумал, что это название общеупотребительное, но, по всей видимости, так ее называли только в лекционных материалах моего курса, видимо, для краткости.

(16 Окт 2:06) haosfortum

@falcao, @haosfortum, прав, я уточнил и прикрепил систему аксиом, которой сказали пользоваться, там правда их 10, но имеется ввиду 11, не дописал одну.

(16 Окт 2:23) Pointer

@Pointer: наверное, их и есть 10. И ещё правило вывода modus ponens.

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

(16 Окт 2:46) falcao

11-ой аксилмой обычно служит $%A\rightarrow\neg\neg A$%

(16 Окт 9:24) haosfortum

@haosfortum: а зачем? Эту формулу ведь можно вывести. Если принять A, то not(A) влечёт противоречие, и по (9) получается вывод not(not(A)). Это исчисление в ряде задач уже встречалось, хотя оно не самое удобное.

(16 Окт 13:18) falcao
показано 5 из 13 показать еще 8
10|600 символов нужно символов осталось
2

Для начала, нужно уточнить, что дизъюнкция трёх формул есть сокращённая запись формулы (X V Y) V Z, а равносильность, то есть X<->Y, есть сокращённая запись конъюнкции двух импликаций: (X->Y) & (Y->X).

Для работы с исчислениями такого типа нужно иметь ряд дополнительных правил, которые выводятся из аксиом, чтобы далее с ними свободно работать. Попробуем их последовательности вывести. Это поможет в случае чего давать ссылки, если появятся новые вопросы на ту же тему (а про это исчисление периодически что-то спрашивают). Теорему дедукции считаем доказанной, и используем её как известный принцип доказательства. Каждый раз общий механизм оговаривать не будем, а просто будем пользоваться тем, что если нужно вывести импликацию X->Y, то принимаем посылку X и выводим заключение Y.

1) Если выведена формула A, то для любой формулы B можно считать выведенной формулу B->A. Это следует из схемы аксиом 1 (при ссылках пишем A1) и правила modus ponens (MP). Этот принцип можно назвать "ослаблением".

2) Из противоречия выводима любая формула. Под противоречие понимается наличие выведенной формулы B вместе с формулой not(B). Пусть мы хотим вывести A. Тогда сначала ослабляем выведенные формулы до not(A)->B и not(A)->not(B). Из A9 и MP получаем not(not(A)). Из A10 и MP выводим A.

3) Закон двойного отрицания: одна его часть уже дана в A10. Вторая часть: надо вывести A->not(not(A)). Принимаем A и выводим заключение. Ввиду того, что not(A) приводит к противоречию, с помощью A9 получаем not(not(A)).

4) Правило рассуждения от противного: для того, чтобы вывести X, достаточно not(X) привести к противоречию. Это следует из A9 и закона двойного отрицания. Также, чтобы вывести not(X), достаточно X привести к противоречию. Это прямо следует из A9.

5) Закон контрапозиции: из X->Y выводимо not(Y)->not(X). Здесь мы принимаем not(Y) и выводим not(X) от противного. Достаточно X привести к противоречию. По MP имеем Y, противоречие налицо.

Варианты того же закона: из not(X)->Y выводится not(Y)->X, и т.п. Здесь работает транзитивность импликации (очевидно!), и закон двойного отрицания.

Начинаем решать собственно задачу. Там нужно вывести две импликации. Сначала берём импликацию -> (слева направо). С учётом A8, для вывода некоторой формулы из дизъюнкции, достаточно вывести её из каждого дизъюнктивного члена -- в том числе когда их три. Под Ф понимаем правую часть формулы из условия, после связки <->.

Из not(A) выводимо Ф. При выводе Ф мы принимаем посылки импликаций: A->C, B->C и A, выводя B. Это же относится и к другим выводам Ф, которые идут ниже. Здесь мы сразу имеем противоречие, из которого выводимо всё.

Из B выводимо A. Здесь B уже дано, выводить ничего не надо (можно также сослаться на ослабление).

Из not(C) выводимо Ф. Здесь мы приняли три посылки (см. выше), из которых по MP выводится C, что даёт противоречие, а из него выводимо всё.

Таким образом, импликация -> установлена. Осталось вывести <-. Там будет дано Ф, и надо вывести дизъюнкцию. Добавим ещё один пункт.

6) Закон де Моргана. Из отрицания дизъюнкции not(X V Y) выводимы как not(X), так и not(Y). С учётом A5, получается и конъюнкция отрицаний, но здесь это не нужно. Здесь not(X) выводится от противного, так как если принять X, то A6 даст X V Y, что является противоречием. Аналогично, если принять Y, то противоречие даст A7.

Теперь мы приняли Ф, и надо доказать дизъюнкцию. Принимаем её отрицание, желая далее получить противоречие. Отрицание дизъюнкции по закону де Моргана даст нам A, not(B) и C, с учётом закона двойного отрицания. Располагая C, ослабляем его до A->C и B->C. Из них и Ф при помощи MP выводим A->B. Имея A, выводим B, а это противоречие.

ссылка

отвечен 16 Окт 21:27

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

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

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

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

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

отмечен:

×911

задан
15 Окт 22:08

показан
96 раз

обновлен
16 Окт 21:27

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

по почте:

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

по RSS:

Ответы

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

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