Доказать,что формула является теоремой формализованного исчисления высказываний

@whiphy · Регистрация: 24.03.2019

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

Доказать,используя при необходимости теорему дедукции и производные правила вывода(modus poneus), что следующая формула является теоремой формализованного исчисления высказываний(дистрибутивный закон):
((a ∧ b) ∨ c) → ((a ∨ c) ∧ (b ∨ c))

@3D Homer · 06.04.2019, 17:53

См. замечание в этом сообщении.

@whiphy · 06.04.2019, 18:05 **[ТС]**

согласен,нужно использовать аксиомы ,метод дедукции ,но у меня не вышло

@3D Homer · 06.04.2019, 18:16

Наш диалог похож на следующий.

— Помогите мне написать программу, находящую кратчайший путь в графе.
— На каком языке программирования?
— Согласен: нужно использовать синтаксис, набор библиотек и другие особенности языка программирования. Я пробовал написать программу, но у меня не вышло.

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

@whiphy · 09.04.2019, 10:43 **[ТС]**

Каковы бы ни были формулы A, B, C, следующие формулы называют аксиомами исчисления высказываний:

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

(1) A → (B → A);
(2) (A → (B → C)) → ((A → B) → (A → C));
(3) (A ∧ B) → A;
(4) (A ∧ B) → B;
(5) A → (B → (A ∧ B));
(6) A → (A ∨ B);
(7) B → (A ∨ B);
(8) (A → C) → ((B → C) → (A ∨ B → C));
(9) ¬A → (A → B);
(10) (A → B) → ((A → ¬B) → ¬A);
(11) A ∨ ¬A.

«modus ponens» (MP): разрешает получить (вывести) из формул A и (A → B) формулу B.
Выводом в исчислении высказываний называется конечная последовательность формул, каждая из которых есть аксиома или получается из предыдущих по правилу modus ponens.
Также можно использовать следующие свойства:

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

(A → (B → С)|-B→(A→C)
(A → (B → С)|-(B ∧ A)→C)
(A ∧ B) → C|-A→(B→C)
|--значок означает выводима
Пример:
Формула (X∧Y)→(Y∧X) выводима.

Доказательство. Приведем вывод:
(1) (X→Y)→((X→Z)→(X→(Y∧Z)));
(2) ((X∧Y)→Y)→(((X∧Y)→Z)→((X∧Y)→(Y∧Z)));
(3) ((X∧Y)→Y)→(((X∧Y)→X)→((X∧Y)→(Y∧X)));
(4) (X∧Y)→Y;
(5) ((X∧Y)→X)→((X∧Y)→(Y∧X));
(6) (X∧Y)→X
(7) (X∧Y)→(Y∧X).

Добавлено через 13 минут
Формула A называется выводимой , если существует вывод, в котором
присутствует формула A. Запись `A означает, что формула A является теоремой.
Чтобы доказать, что формула является выводимой, удобно использовать вывод
из гипотез и лемму о дедукции.
Вывод гипотез-конечная последовательность формул,
каждая из которых или является аксиомой или является формулой из множества гипотез или выводится из некоторых предыдущих формул последовательности по правилу modus ponens.(Γ |- A ,где Г множество гипотез)("|-"-значок означает формула выводима)
лемма о дедукции-. Γ |- A → B тогда и только тогда, когда Γ, A |- B

@3D Homer · 09.04.2019, 14:00

Указанным исчислением тяжело пользоваться напрямую. В книге

Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. 4-е изд. М.: МЦНМО, 2012

рекомендуется доказать допустимость нескольких правил (правило допустимо, если его использование не увеличивает количество выводимых формул). Во-первых, это теорема о дедукции $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}$ (её у вас использовать разрешено), а также
$https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma,A,B\vdash C}{\Gamma,A\wedge B\vdash C}$ , $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma,A\vdash C\qquad\Gamma,B\vdash C}{\Gamma,A\vee B\vdash C}$ , $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma\vdash A}{\Gamma\vdash A\vee B}$ , $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma\vdash B}{\Gamma\vdash A\vee B}$ , $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma\vdash A\qquad\Gamma\vdash B}{\Gamma\vdash A\wedge B}$

Попробуйте построить вывод $https://www.cyberforum.ru/cgi-bin/latex.cgi?\vdash (a\wedge b)\vee c\to (a \vee c) \wedge (b \vee c)$ . Он строится снизу вверх с помощью этих правил. Сначала, естественно, применяется теорема о дедукции. Утверждение $https://www.cyberforum.ru/cgi-bin/latex.cgi?\Gamma\vdash A$ является заведомо выводимым, если $https://www.cyberforum.ru/cgi-bin/latex.cgi?A\in\Gamma$ .

@whiphy · 14.04.2019, 07:31 **[ТС]**

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

((a ∧ b) ∨ c) → ((a ∨ c) ∧ (b ∨ c))
1) (a ∧ b) ∨ c) |- (a ∨ c) ∧ (b ∨ c)
2) (a ∧ b) |- (a ∨ c) ∧ (b ∨ c)
c |- (a ∨ c) ∧ (b ∨ c)
3) a,b |- (a ∨ c) ∧ (b ∨ c)

не могу понять как дальше выходит

@3D Homer · 14.04.2019, 13:24

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

В шаге 3 вам нужно использовать последнее правило из сообщения 6 (введение конъюнкции), а после него — второе и третье с конца (введение дизъюнкции). С секвенцией c |- (a ∨ c) ∧ (b ∨ c) поступать аналогично.

@whiphy 0 / 0 / 0 Регистрация: 24.03.2019 Сообщений: 24
		1
	Доказать,что формула является теоремой формализованного исчисления высказываний 06.04.2019, 17:46. Показов 5157. Ответов 7 Метки нет (Все метки) Доказать,используя при необходимости теорему дедукции и производные правила вывода(modus poneus), что следующая формула является теоремой формализованного исчисления высказываний(дистрибутивный закон): ((a ∧ b) ∨ c) → ((a ∨ c) ∧ (b ∨ c)) 0

@3D Homer $Эксперт по математике/физике$ 4768 / 3412 / 1088 Регистрация: 01.09.2014 Сообщений: 9,335
	06.04.2019, 17:53	2
	См. замечание в этом сообщении. 0

@whiphy 0 / 0 / 0 Регистрация: 24.03.2019 Сообщений: 24
	06.04.2019, 18:05 [ТС]	3
	согласен,нужно использовать аксиомы ,метод дедукции ,но у меня не вышло 0

@3D Homer $Эксперт по математике/физике$ 4768 / 3412 / 1088 Регистрация: 01.09.2014 Сообщений: 9,335
	06.04.2019, 18:16	4
	Наш диалог похож на следующий. — Помогите мне написать программу, находящую кратчайший путь в графе. — На каком языке программирования? — Согласен: нужно использовать синтаксис, набор библиотек и другие особенности языка программирования. Я пробовал написать программу, но у меня не вышло. Ну что ж, пробуйте написать программу неизвестно на каком языке программирования (построить вывод формулы в неизвестно каком исчислении). Может, выйдет. 0

@whiphy 0 / 0 / 0 Регистрация: 24.03.2019 Сообщений: 24
	09.04.2019, 10:43 [ТС]	5
	Каковы бы ни были формулы A, B, C, следующие формулы называют аксиомами исчисления высказываний: Кликните здесь для просмотра всего текста (1) A → (B → A); (2) (A → (B → C)) → ((A → B) → (A → C)); (3) (A ∧ B) → A; (4) (A ∧ B) → B; (5) A → (B → (A ∧ B)); (6) A → (A ∨ B); (7) B → (A ∨ B); (8) (A → C) → ((B → C) → (A ∨ B → C)); (9) ¬A → (A → B); (10) (A → B) → ((A → ¬B) → ¬A); (11) A ∨ ¬A. «modus ponens» (MP): разрешает получить (вывести) из формул A и (A → B) формулу B. Выводом в исчислении высказываний называется конечная последовательность формул, каждая из которых есть аксиома или получается из предыдущих по правилу modus ponens. Также можно использовать следующие свойства: Кликните здесь для просмотра всего текста (A → (B → С)\|-B→(A→C) (A → (B → С)\|-(B ∧ A)→C) (A ∧ B) → C\|-A→(B→C) \|--значок означает выводима Пример: Формула (X∧Y)→(Y∧X) выводима. Доказательство. Приведем вывод: (1) (X→Y)→((X→Z)→(X→(Y∧Z))); (2) ((X∧Y)→Y)→(((X∧Y)→Z)→((X∧Y)→(Y∧Z))); (3) ((X∧Y)→Y)→(((X∧Y)→X)→((X∧Y)→(Y∧X))); (4) (X∧Y)→Y; (5) ((X∧Y)→X)→((X∧Y)→(Y∧X)); (6) (X∧Y)→X (7) (X∧Y)→(Y∧X). Добавлено через 13 минут Формула A называется выводимой , если существует вывод, в котором присутствует формула A. Запись `A означает, что формула A является теоремой. Чтобы доказать, что формула является выводимой, удобно использовать вывод из гипотез и лемму о дедукции. Вывод гипотез-конечная последовательность формул, каждая из которых или является аксиомой или является формулой из множества гипотез или выводится из некоторых предыдущих формул последовательности по правилу modus ponens.(Γ \|- A ,где Г множество гипотез)("\|-"-значок означает формула выводима) лемма о дедукции-. Γ \|- A → B тогда и только тогда, когда Γ, A \|- B 0

@3D Homer $Эксперт по математике/физике$ 4768 / 3412 / 1088 Регистрация: 01.09.2014 Сообщений: 9,335
	09.04.2019, 14:00	6
	Указанным исчислением тяжело пользоваться напрямую. В книге Верещагин Н. К., Шень А. Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления. 4-е изд. М.: МЦНМО, 2012 рекомендуется доказать допустимость нескольких правил (правило допустимо, если его использование не увеличивает количество выводимых формул). Во-первых, это теорема о дедукции $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}$ (её у вас использовать разрешено), а также $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma,A,B\vdash C}{\Gamma,A\wedge B\vdash C}$ , $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma,A\vdash C\qquad\Gamma,B\vdash C}{\Gamma,A\vee B\vdash C}$ , $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma\vdash A}{\Gamma\vdash A\vee B}$ , $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma\vdash B}{\Gamma\vdash A\vee B}$ , $https://www.cyberforum.ru/cgi-bin/latex.cgi?\frac{\Gamma\vdash A\qquad\Gamma\vdash B}{\Gamma\vdash A\wedge B}$ Попробуйте построить вывод $https://www.cyberforum.ru/cgi-bin/latex.cgi?\vdash (a\wedge b)\vee c\to (a \vee c) \wedge (b \vee c)$ . Он строится снизу вверх с помощью этих правил. Сначала, естественно, применяется теорема о дедукции. Утверждение $https://www.cyberforum.ru/cgi-bin/latex.cgi?\Gamma\vdash A$ является заведомо выводимым, если $https://www.cyberforum.ru/cgi-bin/latex.cgi?A\in\Gamma$ . 1

@whiphy 0 / 0 / 0 Регистрация: 24.03.2019 Сообщений: 24
	14.04.2019, 07:31 [ТС]	7
	Кликните здесь для просмотра всего текста ((a ∧ b) ∨ c) → ((a ∨ c) ∧ (b ∨ c)) 1) (a ∧ b) ∨ c) \|- (a ∨ c) ∧ (b ∨ c) 2) (a ∧ b) \|- (a ∨ c) ∧ (b ∨ c) c \|- (a ∨ c) ∧ (b ∨ c) 3) a,b \|- (a ∨ c) ∧ (b ∨ c) не могу понять как дальше выходит 0

@3D Homer $Эксперт по математике/физике$ 4768 / 3412 / 1088 Регистрация: 01.09.2014 Сообщений: 9,335
	14.04.2019, 13:24	8
	Вы пишете вывод сверху вниз, хотя, как я сказал, лучше снизу вверх, чтобы отдельные правила были так, как в сообщении 6, а не перевёрнуты. На форуме, правда, это сделать тяжело даже в редакторе формул. Можно попробовать в тегах CODE, которые используют моноширинный шрифт, что делает возможным выравнивание. В шаге 3 вам нужно использовать последнее правило из сообщения 6 (введение конъюнкции), а после него — второе и третье с конца (введение дизъюнкции). С секвенцией c \|- (a ∨ c) ∧ (b ∨ c) поступать аналогично. 0

Опции темы