Вывести высказывание из системы аксиом

@el_razor · Регистрация: 11.12.2013

Author24 — интернет-сервис помощи студентам

собственно надо вывести вот это высказывание:
!A -> (A -> B)

из системы аксиом
ну у нас были даны вот эти аксиомы:
A->(B->A)
(A->(B->C))->((A->B)->(A->C))
(!A->!B)->((!A->B)->A)
и еще modus ponens

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

Psilon · 03.06.2015, 14:36

el_razor, на самом деле алгоритм есть, тот же метод резолюций, но в вашем случае да, нужно творчески.

Да и с точки простейшей логики !A -> (A -> B) == A || !A || B == TRUE

Для начала стоит использовать первую формулу, обозначив A = !A, B = !B тогда получим
!A -> (!B -> !A)
Теперь третью применим:

!A -> ((!B -> !A) -> ((!B -> !A) -> !B)))

Теперь попробуем вторую:

!A -> ((!B -> !A) -> ((!B -> !A) -> !B)))

!A -> ((!B -> !A) -> ((!B -> !A) -> !B))) -> !A -> (!B -> !A) -> !A -> ((!B -> !A) -> !B))

Тут я уже запутался

Но смысл примерно такой.

@Mysterious Light · 03.06.2015, 19:53

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

Итак, предположим, что справедливо одновременно A и -A как аксиомы. Наша задача показать, что такая система является противоречивой, то есть выводимо любое суждение B. По лемме о дедукции это эквивалентно выводу !A -> (A -> B) в «чистой» системе без двух дополнительных аксиом. Доказываемое суждение является своеобразной (более простой) формой закона о несовместимости A и !A.

Самописная программа мне выдала такой результат для этой системы аксиом:

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

1. Однобуквенные формулы
1.1. за 3 шага доказуемо
1.1.1. a -> a
1.1.2. (-a -> a) -> a
1.2. за 4 шага доказуемо
1.2.1. (-a -> --a) -> a
1.3. за 5 шагов доказуемо
1.3.1. ((-a -> -a) -> (-a -> --a)) -> a
1.3.2. (-a -> (-a -> a)) -> a
1.3.3. (-a -> (-a -> --a)) -> a

2. Двухбуквенные формулы
2.1. за 2 шага
2.1.1. ((a -> b) -> (a -> a))
2.1.2. ((-a -> -[b -> -a]) -> a)
2.2. за 3 шага
2.2.1. (a -> (a -> c)) -> (a -> c)
2.3. за 4 шага
2.3.1. (a -> ((-b -> -a) -> b))
2.3.2. ((-a -> b) -> ((-a -> --a) -> a))
2.3.3. (a -> (b -> b))
2.3.4. (a -> ((-b -> b) -> b))
2.3.5 ((-a -> a) -> (c -> a))
2.3.6 (-[a -> -b] -> b)
2.3.7. ((-a -> -b) -> ((-a -> b) -> a))
2.4. за 5 шагов
2.4.1. ((a -> (-b -> -a)) -> (a -> b))
2.4.2. ((-a -> -[(-b -> --a) -> b]) -> a)
2.4.3. ((-a -> -[b -> b]) -> a)
2.4.4. (a -> ((-b -> --b) -> b))
2.4.5. ((-a -> (-a -> -[c -> -a])) -> a)
2.4.6. ((a -> (-b -> b)) -> (a -> b))
2.4.7. ((-a -> -[(-b -> b) -> b]) -> a)
2.4.8. ((-[a -> -b] -> -b) -> (a -> -b))
2.4.9. (-a -> ((-b -> a) -> b))
2.4.10. ((a -> -a) -> ((-c -> a) -> c))
2.4.11. (((a -> a) -> c) -> c)
2.4.12. ((a -> (-b -> --b)) -> (a -> b))
2.4.13. ((-a -> -[(-b -> --b) -> b]) -> a)
2.4.14. ((-a -> --a) -> (c -> a))
2.4.15. ((-[a -> b] -> b) -> (a -> b))
2.4.16. ((-a -> ((b -> -a) -> a)) -> a)
2.4.17. ((((-a -> a) -> a) -> d) -> d)
2.4.18. ((-a -> a) -> ((-c -> -a) -> c))
2.4.19. ((--[a -> -b] -> -[a -> -b]) -> b)
.......................

За 6 шагов выводимо --a -> a (закон снятия двойного отрицания), но не выводимо a -> (-a -> b)

@el_razor · 03.06.2015, 21:46 **[ТС]**

Сообщение от Psilon

на самом деле алгоритм есть

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

@Mysterious Light · 03.06.2015, 22:22

Зашибись! Оно таки выводится!

Итак, привожу вывод того, что при следующих аксиомах (A1-4) теория противоречива:
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(A1) \qquad a\to b \to a$
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(A2) \qquad (\neg a \to \neg b) \to (\neg a \to b) \to a$
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(A3) \qquad X$
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(A4) \qquad \neg X$
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(T1: A1, A4) \qquad b \to \neg X$
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(T2: A1, A3) \qquad b \to X$
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(T3: T1, A2) \qquad (\neg c\to X)\to c$
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(T4: T2, T3) \qquad c$
a, b, c — символы, которые могут быть заменены на произвольные формулы.
Скобки расставляются по ассоциативности вправо.

Итак, доказано
$https://www.cyberforum.ru/cgi-bin/latex.cgi?X,\neg X\vdash B$
Два раза применяем лемму о дедукции:
$https://www.cyberforum.ru/cgi-bin/latex.cgi?\neg X\vdash X\to B$
$https://www.cyberforum.ru/cgi-bin/latex.cgi?\vdash \neg X\to X\to B$
исходное суждение доказано.

Без леммы о дедукции вывод выглядит более громоздким. Проще всего предварительно доказать теорему
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(C) \qquad (b \to c) \to (d \to b) \to (e \to d) \to (a \to e) \to a \to c$
или хотя бы
$https://www.cyberforum.ru/cgi-bin/latex.cgi?(b\to c) \to ((a\to b)\to (a\to c))$
Затем поочерёдно применить (т.е. сделать MP) теорему (C) к аксиомам в такой последовательности: A2, A1, A3, A1, где A1-3 — это три аксиомы в том порядке, в котором они указаны в первом посте.
Далее взять аксиому A2 и применить её к тому, что получилось в прошлом пункте, и затем применить полученное к $https://www.cyberforum.ru/cgi-bin/latex.cgi?a\to b \to c \to b$ (получается из A2 и A2).
Применить (A->B) к A значит использовать Modus Ponens, в результате которого получается B.

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

@el_razor 2 / 2 / 0 Регистрация: 11.12.2013 Сообщений: 58
		1
	Вывести высказывание из системы аксиом 02.06.2015, 17:36. Показов 1447. Ответов 4 Метки нет (Все метки) собственно надо вывести вот это высказывание: !A -> (A -> B) из системы аксиом ну у нас были даны вот эти аксиомы: A->(B->A) (A->(B->C))->((A->B)->(A->C)) (!A->!B)->((!A->B)->A) и еще modus ponens какого то алгоритма насколько я знаю нет, задание почти творческое... повезет/не повезет подобрать такую последовательность аксиом чтобы вывести необходимое высказывание... ну вот мне как то не везет 0

Psilon Master of Orion 6100 / 4956 / 905 Регистрация: 10.07.2011 Сообщений: 14,522 Записей в блоге: 5
	03.06.2015, 14:36	2
	el_razor, на самом деле алгоритм есть, тот же метод резолюций, но в вашем случае да, нужно творчески. Да и с точки простейшей логики !A -> (A -> B) == A \|\| !A \|\| B == TRUE Для начала стоит использовать первую формулу, обозначив A = !A, B = !B тогда получим !A -> (!B -> !A) Теперь третью применим: !A -> ((!B -> !A) -> ((!B -> !A) -> !B))) Теперь попробуем вторую: !A -> ((!B -> !A) -> ((!B -> !A) -> !B))) !A -> ((!B -> !A) -> ((!B -> !A) -> !B))) -> !A -> (!B -> !A) -> !A -> ((!B -> !A) -> !B)) Тут я уже запутался Но смысл примерно такой. 0

@Mysterious Light $Эксперт по математике/физике$ 4300 / 2091 / 431 Регистрация: 19.07.2009 Сообщений: 3,163 Записей в блоге: 24
	03.06.2015, 19:53	3
	Первые две аксиомы необходимы и достаточны для того, чтобы использовать лемму о дедукции. С её помощью вывод становится более естественным и понятным. Последняя же аксиома является своеобразной комбинацией привычной нам аксиомы и закона снятия двойного отрицания. В какой-то книге я встречал такую систему аксиом, но там, вроде, ещё какая-то аксиома с отрицанием присутствовала. Итак, предположим, что справедливо одновременно A и -A как аксиомы. Наша задача показать, что такая система является противоречивой, то есть выводимо любое суждение B. По лемме о дедукции это эквивалентно выводу !A -> (A -> B) в «чистой» системе без двух дополнительных аксиом. Доказываемое суждение является своеобразной (более простой) формой закона о несовместимости A и !A. Самописная программа мне выдала такой результат для этой системы аксиом: Кликните здесь для просмотра всего текста 1. Однобуквенные формулы 1.1. за 3 шага доказуемо 1.1.1. a -> a 1.1.2. (-a -> a) -> a 1.2. за 4 шага доказуемо 1.2.1. (-a -> --a) -> a 1.3. за 5 шагов доказуемо 1.3.1. ((-a -> -a) -> (-a -> --a)) -> a 1.3.2. (-a -> (-a -> a)) -> a 1.3.3. (-a -> (-a -> --a)) -> a 2. Двухбуквенные формулы 2.1. за 2 шага 2.1.1. ((a -> b) -> (a -> a)) 2.1.2. ((-a -> -[b -> -a]) -> a) 2.2. за 3 шага 2.2.1. (a -> (a -> c)) -> (a -> c) 2.3. за 4 шага 2.3.1. (a -> ((-b -> -a) -> b)) 2.3.2. ((-a -> b) -> ((-a -> --a) -> a)) 2.3.3. (a -> (b -> b)) 2.3.4. (a -> ((-b -> b) -> b)) 2.3.5 ((-a -> a) -> (c -> a)) 2.3.6 (-[a -> -b] -> b) 2.3.7. ((-a -> -b) -> ((-a -> b) -> a)) 2.4. за 5 шагов 2.4.1. ((a -> (-b -> -a)) -> (a -> b)) 2.4.2. ((-a -> -[(-b -> --a) -> b]) -> a) 2.4.3. ((-a -> -[b -> b]) -> a) 2.4.4. (a -> ((-b -> --b) -> b)) 2.4.5. ((-a -> (-a -> -[c -> -a])) -> a) 2.4.6. ((a -> (-b -> b)) -> (a -> b)) 2.4.7. ((-a -> -[(-b -> b) -> b]) -> a) 2.4.8. ((-[a -> -b] -> -b) -> (a -> -b)) 2.4.9. (-a -> ((-b -> a) -> b)) 2.4.10. ((a -> -a) -> ((-c -> a) -> c)) 2.4.11. (((a -> a) -> c) -> c) 2.4.12. ((a -> (-b -> --b)) -> (a -> b)) 2.4.13. ((-a -> -[(-b -> --b) -> b]) -> a) 2.4.14. ((-a -> --a) -> (c -> a)) 2.4.15. ((-[a -> b] -> b) -> (a -> b)) 2.4.16. ((-a -> ((b -> -a) -> a)) -> a) 2.4.17. ((((-a -> a) -> a) -> d) -> d) 2.4.18. ((-a -> a) -> ((-c -> -a) -> c)) 2.4.19. ((--[a -> -b] -> -[a -> -b]) -> b) ....................... За 6 шагов выводимо --a -> a (закон снятия двойного отрицания), но не выводимо a -> (-a -> b) 0

@el_razor 2 / 2 / 0 Регистрация: 11.12.2013 Сообщений: 58
	03.06.2015, 21:46 [ТС]	4
	Сообщение от Psilon на самом деле алгоритм есть я к тому что нет никаких критериев в каком порядке использовать аксиомы то о чем вы говорите это вы просто показываете как это делается, это я знаю а вот в каком порядке их применять... это не выходит 0

@Mysterious Light $Эксперт по математике/физике$ 4300 / 2091 / 431 Регистрация: 19.07.2009 Сообщений: 3,163 Записей в блоге: 24
	03.06.2015, 22:22	5
	Зашибись! Оно таки выводится! Итак, привожу вывод того, что при следующих аксиомах (A1-4) теория противоречива: $https://www.cyberforum.ru/cgi-bin/latex.cgi?(A1) \qquad a\to b \to a$ $https://www.cyberforum.ru/cgi-bin/latex.cgi?(A2) \qquad (\neg a \to \neg b) \to (\neg a \to b) \to a$ $https://www.cyberforum.ru/cgi-bin/latex.cgi?(A3) \qquad X$ $https://www.cyberforum.ru/cgi-bin/latex.cgi?(A4) \qquad \neg X$ $https://www.cyberforum.ru/cgi-bin/latex.cgi?(T1: A1, A4) \qquad b \to \neg X$ $https://www.cyberforum.ru/cgi-bin/latex.cgi?(T2: A1, A3) \qquad b \to X$ $https://www.cyberforum.ru/cgi-bin/latex.cgi?(T3: T1, A2) \qquad (\neg c\to X)\to c$ $https://www.cyberforum.ru/cgi-bin/latex.cgi?(T4: T2, T3) \qquad c$ a, b, c — символы, которые могут быть заменены на произвольные формулы. Скобки расставляются по ассоциативности вправо. Итак, доказано $https://www.cyberforum.ru/cgi-bin/latex.cgi?X,\neg X\vdash B$ Два раза применяем лемму о дедукции: $https://www.cyberforum.ru/cgi-bin/latex.cgi?\neg X\vdash X\to B$ $https://www.cyberforum.ru/cgi-bin/latex.cgi?\vdash \neg X\to X\to B$ исходное суждение доказано. Без леммы о дедукции вывод выглядит более громоздким. Проще всего предварительно доказать теорему $https://www.cyberforum.ru/cgi-bin/latex.cgi?(C) \qquad (b \to c) \to (d \to b) \to (e \to d) \to (a \to e) \to a \to c$ или хотя бы $https://www.cyberforum.ru/cgi-bin/latex.cgi?(b\to c) \to ((a\to b)\to (a\to c))$ Затем поочерёдно применить (т.е. сделать MP) теорему (C) к аксиомам в такой последовательности: A2, A1, A3, A1, где A1-3 — это три аксиомы в том порядке, в котором они указаны в первом посте. Далее взять аксиому A2 и применить её к тому, что получилось в прошлом пункте, и затем применить полученное к $https://www.cyberforum.ru/cgi-bin/latex.cgi?a\to b \to c \to b$ (получается из A2 и A2). Применить (A->B) к A значит использовать Modus Ponens, в результате которого получается B. Самому это делать не хочется, слишком трудоёмко, но к ответу приведёт. 2

Опции темы