Как доказать общезначимое высказывание с помощью исчисления

[Kosat]

Как доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Например, $x \vee \neg x$? Можно использовать, к примеру, стандартную гильбертову аксиоматику.

Я смотрю на примеры доказательств (они не без помарок, но в общем понятные). Там вывод осуществляется из гипотез (которые неявно объединены в конъюнкцию), есть семантическое следование из них в доказываемое высказывание. Здесь же у нас нет гипотез, нет следования. Я где-то читал что-то в том роде, что мы можем вводить гипотезы - но как? Как конкретно доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний? Я пытаюсь решить (наметить план решения) третье задание следующего содержания (файлы PDF давать запрещено, поэтому перепишу основную его часть):

«Написать программу, строящую доказательство указанного во входном файле высказывания (если оно общезначимо), либо дающую оценку пропозициональных переменных, на которых высказывание ложно (если оно опровержимо).
Входной файл состоит из единственной строки, содержащей формулу исчисления высказываний, которую требуется доказать или опровергнуть. Высказывание удовлетворяет грамматике из первого задания. Выходной файл должен либо содержать доказательство высказывания (в формате доказательства из первого задания)…»

Первое задание (тоже непонятно как решать) задаёт грамматику формами Бэкуса-Наура и его основная часть звучит следующим образом:

«Написать программу, проверяющую доказательства в исчислении высказываний на корректность. Входной файл представляет из себя последовательность высказываний, по высказыванию на строку. ... Результатом работы программы должен быть проаннотированный текст доказательства, касательно каждой строки должно быть указано, из чего и как она получается.»

[warlock66613]

Kosat в сообщении #988573 писал(а):

Как доказать какое-нибудь общезначимое высказывание с помощью исчисления высказываний?

Доказательством называется ряд формул, каждая из которых является либо аксиомой либо выводом (по правилу вывода) из любых предшествующих формул. Соответственно, доказывается именно выписыванием этого ряда формул. При этом надо помнить, что "$11$ аксиом" по ссылке в википедии - это не аксиомы. Это схемы аксиом. Аксиом в логике высказываний бесконечное число и они получаются из схем подстановкой произвольных формул вместо заглавных букв в схемы. Например, $(a \to b \vee \neg a) \rightarrow (b \rightarrow (a \to b \vee \neg a))$ - это аксиома ($A_1$). Ну а чтобы научиться доказывать какие-то конкретные утверждения, надо упражняться.

Kosat в сообщении #988573 писал(а):

Например, $x \vee \neg x$?

Записываем аксиому $x \vee \neg x$ ($A_{11}$ для $A=x$). Ч. и т. д.

Kosat в сообщении #988573 писал(а):

Я где-то читал что-то в том роде, что мы можем вводить гипотезы - но как?

Именно пользуясь схемой $A_{11}$. Для любой гипотезы $H$ мы можем записать $H \vee \neg H$ - это аксиома, а дальше - как обычно.

-- 12.03.2015, 02:22 --

Kosat в сообщении #988573 писал(а):

Я пытаюсь решить (наметить план решения) третье задание отсюда

Вот как узнать является ли формула тавталогией и получить доказательство алгоритмически я не знаю. Но я бы начал с изучения доказательства разрешимости логики высказываний.

[Lia]

Тема перемещена из форума «Помогите решить / разобраться (М)» в форум «Карантин»
по следующим причинам:

- не оформлены ссылки;
- неправильно набраны формулы (краткие инструкции: «Краткий FAQ по тегу [math]» и видеоролик Как записывать формулы): уберите ссылку на pdf-файл, вставьте только требуемое

Исправьте все Ваши ошибки и сообщите об этом в теме Сообщение в карантине исправлено.
Настоятельно рекомендуется ознакомиться с темами Что такое карантин и что нужно делать, чтобы там оказаться и Правила научного форума.

[Lia]

Тема перемещена из форума «Карантин» в форум «Помогите решить / разобраться (М)»

[Kosat]

warlock66613 в сообщении #989080 писал(а):

Kosat в сообщении #988573 писал(а):

Я где-то читал что-то в том роде, что мы можем вводить гипотезы - но как?

Именно пользуясь схемой $A_{11}$. Для любой гипотезы $H$ мы можем записать $H \vee \neg H$ - это аксиома, а дальше - как обычно.

Как именно? Я не вижу ни одной схемы аксиом с дизъюнкцией слева.

warlock66613 в сообщении #989080 писал(а):

Kosat в сообщении #988573 писал(а):

Я пытаюсь решить (наметить план решения) третье задание отсюда

Вот как узнать является ли формула тавталогией и получить доказательство алгоритмически я не знаю. Но я бы начал с изучения доказательства разрешимости логики высказываний.

Я пытался. Возможно, четвёртое задание (теорема дедукции и проверка доказательства в исчислении предикатов средствами С++) будет полегче, но хотелось бы и третье.

[warlock66613]

Kosat в сообщении #990639 писал(а):

Как именно? Я не вижу ни одной схемы аксиом с дизъюнкцией слева.

Посмотрите на $A_8$. Если вывести $H \to C$ (доказательство в предположении справедливости гипотезы) и $\neg H \to C$ (доказательство в преположении отрицания гипотезы), то, с помощью $A_8$ и трижды применённого modus ponens, из $H \vee \neg H$ как раз и получается $C$.

-- 17.03.2015, 00:47 --

Kosat в сообщении #990639 писал(а):

Я пытался.

Есть сильное подозрение, что надо идти от (или к) таблицам истинности. Впрочем, вы, я полагаю, тоже так думаете - не зря же вы заговорили про гипотезы.

[Kosat]

warlock66613 в сообщении #991246 писал(а):

Посмотрите на $A_8$. Если вывести $H \to C$ (доказательство в предположении справедливости гипотезы) и $\neg H \to C$ (доказательство в преположении отрицания гипотезы), то, с помощью $A_8$ и трижды применённого modus ponens, из $H \vee \neg H$ как раз и получается $C$.

Я не понимаю. У нас в левой части $A_8$ импликация, а не дизъюнкция. И как же мы можем "вывести $H \to C$", если у нас не из чего выводить? Нет у нас аксиом, утверждение общезначимое. Надо это доказать.

warlock66613 в сообщении #991246 писал(а):

Есть сильное подозрение, что надо идти от (или к) таблицам истинности. Впрочем, вы, я полагаю, тоже так думаете - не зря же вы заговорили про гипотезы.

Ну для нахождения наборов, на которых функция неверна, наверно нужна таблица истинности. Но доказывать надо с помощью аксиом. Это же совсем другое дело, разве не так? Я смотрю на примеры доказательств (например, 15.8 (д); результат третьего задания должен быть в такой форме, думаю), но общего алгоритмического правила не вижу.

[warlock66613]

Kosat в сообщении #991270 писал(а):

Я не понимаю. У нас в левой части $A_8$ импликация, а не дизъюнкция. И как же мы можем "вывести $H \to C$", если у нас не из чего выводить? Нет у нас аксиом, утверждение общезначимое. Надо это доказать.

Допустим мы хотим доказать некоторое утверждение $C$ (где $C$ - это какая-то сложная формула). И мы думаем, что удобно ввести две взаимоисключающие и исчерпывающие все возможные ситуации гипотезы - $H$ и $\neg H$ (при этом $H$ - это тоже какая-то сложная формула, причём произвольная - от гипотезы не требуется общезначимость).

Тогда на очередном шаге мы записываем в наш ряд (общезначимых) формул $H \vee \neg H$ (пусть это будет "формула номер 0"; это аксиома по схеме $A_{11}$). Далее нам потребуется записать ряд формул, из которого мы получим формулу $H \to C$ (это будет формула номер $1$). Этот ряд и будет первой веткой доказательства - доказательством с гипотезой $H$.

Вторая ветка - доказательство с гипотезой $\neg H$ - должна быть представлена рядом формул, заканчивающимся формулой $\neg H \to C$ (это будет формула номер $2$).

После этого мы пишем формулу $(H \to C) \to ((\neg H \to C) \to ((H \vee \neg H) \to C))$ (формула номер $3$; каковы бы ни были $H$ и $C$, это аксиома по схеме $A_8$). Далее применяем modus ponens к формулам $1$ и $3$. Получаем (и пишем в доказательство) формулу $(\neg H \to C) \to ((H \vee \neg H) \to C)$. Опять применяем modus ponens - теперь к последней формуле и формуле $2$. Получаем $(H \vee \neg H) \to C$. Наконец, применяем modus ponens к последней формуле и формуле $0$. Получем $C$, к чему мы и стремились.

-- 17.03.2015, 02:10 --

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

-- 17.03.2015, 02:19 --

Kosat в сообщении #991270 писал(а):

Ну для нахождения наборов, на которых функция неверна, наверно нужна таблица истинности. Но доказывать надо с помощью аксиом. Это же совсем другое дело, разве не так? Я смотрю на примеры доказательств
(например, 15.8 (д); результат третьего задания должен быть в такой форме, думаю), но общего алгоритмического правила не вижу.

Дело в том, что доказательство любого утверждения - не единственно. Есть более короткие и более длинные доказательства. Вы смотрите на короткие доказательства, так что алгоритмики там не найти. Но вам-то и не требуется получить кратчайшее доказательство. Что касается использования в доказательстве таблиц истинности - каждую строку таблицу истинности можно рассматривать как гипотезу. Как "разложить" доказательство на несколько веток с помощью гипотез я написал выше. Таким образом, осталось только научиться доказывать утверждения вида $x_1 A_1 \to (x_2 A_2 \to (x_3 A_3 \to \dots (x_n A_n \to F(A_1, A_2, A_3, \dots, A_n)\dots)))$, где $x_i$ - либо ничего (если $A_i$ в этой строке - истина) либо значок $\neg$ (если $A_i$ - ложь).

-- 17.03.2015, 02:26 --

Последнее же делается грамматическим разбором $F$. Например, если $F$ имеет вид $F_1 \vee F_2$, то смотрим по таблице истинности, какое именно утверждение из $F_1$ и $F_2$ истинно и доказываем его. Если $F$ имеет вид $F_1 \wedge F_2$, то доказываем оба - сначала $F_1$, затем $F_2$. И т. д.

[warlock66613]

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

[warlock66613]

Хотя нет. Для первой итерации надо взять ещё попроще вариант. $A \to A$ идеально подходит. К тому же это понадобится дальше, при кодировании теоремы дедукции.

[warlock66613]

Вот вам для изучения и раздумий "алгоритмический" вывод формулы $A \vee B \to B \vee A \eqno{(*)}$.
Во-первых докажем вспомогательные формулы для каждой строки таблицы истинности. Их будет $4$ штуки:

$$\neg A \to (\neg B \to (A \vee B \to B \vee A)) \eqno{(1)}$$

$$\neg A \to (B \to (A \vee B \to B \vee A)) \eqno{(2)}$$

$$A \to (\neg B \to (A \vee B \to B \vee A)) \eqno{(3)}$$

$$A \to (B \to (A \vee B \to B \vee A)) \eqno{(4)}$$

Я докажу $(4)$. Остальные ($(1)$, $(2)$ и $(3)$) доказываются аналогично.
Вначале проведём вспомогательный вывод формулы $A \vee B \to B \vee A$ из гипотез $A$, $B$ - то есть считая $A$ и $B$ уже доказанными. Начинаем нисходящий грамматический разбор. Нам надо доказать истиность импликации - для этого надо показать либо ложность посылки, либо истинность следствия. Посылка ($A \vee B$) не ложна, значит будем доказывать истинность следствия ($B \vee A$). Это дизъюнкция. Чтобы доказать дизъюнкцию, надо доказать любой из её операндов. Здесь операнды оба истинны, значит можно доказывать любой. Будем доказывать левый. Но левый операнд - это $B$, а он уже доказан (это гипотеза). Значит получаем такое доказательство:

(Оффтоп)

$$B \to (B \vee A) \eqno{A_6}$$

$$B \vee A \eqno{m. p.}$$

$$B \vee A \to (A \vee B \to B \vee A) \eqno{A_1}$$

$$A \vee B \to B \vee A \eqno{m. p.}$$

Теперь нам надо превратить это доказательство в доказательство утверждения $A \to (B \to (A \vee B \to B \vee A))$ (как бы включить гипотезы $A$ и $B$ в само доказываемое утверждение). Вначале включим $B$. Действуя в соответствии с доказательством теоремы о дедукции, получим такой вывод:

(Оффтоп)

$$B \to (B \vee A) \eqno{A_6}$$

$$(B \to (B \vee A)) \to (B \to (B \to (B \vee A))) \eqno{A_1}$$

$$B \to (B \to (B \vee A)) \eqno{m. p.}$$

(Доказываем $B \to B$)

$$\bigl(B\to ((B\to B)\to B)\bigr)\to \bigl((B\to (B\to B)) \to (B\to B)\bigr)$$

$$B\to \bigl((B\to B)\to B\bigr)$$

$$\bigl(B\to (B\to B)\bigr)\to (B\to B)$$

$$B\to (B\to B)$$

$$B\to B$$

$$(B \to (B \to (B \vee A))) \to ((B \to B) \to (B \to B \vee A)) \eqno{A_2}$$

$$B \to B \vee A \eqno{m. p. \text{дважды}}$$

$$B \vee A \to (A \vee B \to B \vee A) \eqno{A_1}$$

$$(B \vee A \to (A \vee B \to B \vee A)) \to (B \to (B \vee A \to (A \vee B \to B \vee A))) \eqno{A_1}$$

$$B \to (B \vee A \to (A \vee B \to B \vee A)) \eqno{m. p.}$$

$$(B \to (B \vee A \to (A \vee B \to B \vee A))) \to ((B \to B \vee A) \to (B \to (A \vee B \to B \vee A))) \eqno{A_2}$$

$$B \to (A \vee B \to B \vee A) \eqno{m.p. \text{дважды}}$$

Дальше действуя опять аналогично по теореме о дедукции превращаем последнее доказательство в доказательство формулы $(4)$.

Итак мы имеем доказательства формул $(1) - (4)$
Осталось собрать их в одно:

$$A \vee \neg A \eqno{A_{11}}$$

$$(4) \to ((2) \to (A \vee \neg A \to (B \to (*)))) \eqno{A_{8}}$$

$$B \to (*) \eqno{m. p. \text{трижды}}$$

Аналогично, используя $(1)$ и $(3)$, получим $\neg B \to (*)$. Наконец, проворачивая последний трюк с $B$, получаем искомое:

$$B \vee \neg B \eqno{A_{11}}$$

$$(B \to (*)) \to ((\neg B \to (*)) \to (B \vee \neg B \to (*))) \eqno{A_{8}}$$

$$(*) \eqno{m. p. \text{трижды}}$$

Ч. и т. д.

[Kosat]

warlock66613 в сообщении #991281 писал(а):

Далее нам потребуется записать ряд формул, из которого мы получим формулу $H \to C$ (это будет формула номер $1$). Этот ряд и будет первой веткой доказательства - доказательством с гипотезой $H$.

Вторая ветка - доказательство с гипотезой $\neg H$ - должна быть представлена рядом формул, заканчивающимся формулой $\neg H \to C$ (это будет формула номер $2$).

Откуда мы возьмём эти ряды формул?

-

warlock66613 в сообщении #991281 писал(а):

Как "разложить" доказательство на несколько веток с помощью гипотез я написал выше.

Непонятно.

-

warlock66613 в сообщении #991281 писал(а):

Таким образом, осталось только научиться доказывать утверждения вида $x_1 A_1 \to (x_2 A_2 \to (x_3 A_3 \to \dots (x_n A_n \to F(A_1, A_2, A_3, \dots, A_n)\dots)))$, где $x_i$ - либо ничего (если $A_i$ в этой строке - истина) либо значок $\neg$ (если $A_i$ - ложь).

А почему тут импликации, а не конъюнкции?

-

warlock66613 в сообщении #991281 писал(а):

Последнее же делается грамматическим разбором $F$. Например, если $F$ имеет вид $F_1 \vee F_2$, то смотрим по таблице истинности, какое именно утверждение из $F_1$ и $F_2$ истинно и доказываем его. Если $F$ имеет вид $F_1 \wedge F_2$, то доказываем оба - сначала $F_1$, затем $F_2$. И т. д.

Нужна алгоритмика, через аксиомы…

-

warlock66613 в сообщении #991307 писал(а):

Кстати, крайне полезными со всех сторон выглядят теоремы $A \to \neg \neg A$ и $\neg \neg A \to A$, …

Хотя нет. Для первой итерации надо взять ещё попроще вариант. $A \to A$ идеально подходит. К тому же это понадобится дальше, при кодировании теоремы дедукции.

?

-

warlock66613 в сообщении #991333 писал(а):

Вот вам для изучения и раздумий "алгоритмический" вывод формулы $A \vee B \to B \vee A \eqno{(*)}$.
Во-первых докажем вспомогательные формулы для каждой строки таблицы истинности. Их будет $4$ штуки:

$$\neg A \to (\neg B \to (A \vee B \to B \vee A)) \eqno{(1)}$$

$$\neg A \to (B \to (A \vee B \to B \vee A)) \eqno{(2)}$$

$$A \to (\neg B \to (A \vee B \to B \vee A)) \eqno{(3)}$$

$$A \to (B \to (A \vee B \to B \vee A)) \eqno{(4)}$$

Так почему самый левый оператор каждого из четырёх выражений – импликация, а не конъюнкция?..

-

warlock66613 в сообщении #991333 писал(а):

Я докажу $(4)$. Остальные ($(1)$, $(2)$ и $(3)$) доказываются аналогично.
Вначале проведём вспомогательный вывод формулы $A \vee B \to B \vee A$ из гипотез $A$, $B$ - то есть считая $A$ и $B$ уже доказанными. Начинаем нисходящий грамматический разбор. …

Теперь нам надо превратить это доказательство в доказательство утверждения $A \to (B \to (A \vee B \to B \vee A))$ (как бы включить гипотезы $A$ и $B$ в само доказываемое утверждение). Вначале включим $B$.

Захватывающе... Но как это соотносится с последующим? Мы же уже доказали истинность $A \vee B \to B \vee A$, разве не так?

-

warlock66613 в сообщении #991333 писал(а):

Действуя в соответствии с доказательством теоремы о дедукции, получим такой вывод:

Очень интересно. Мне и это надо будет – во втором задании моей длинной домашней работы (из вывода до применения теоремы дедукции сделать вывод после применения теоремы дедукции).

-

warlock66613 в сообщении #991333 писал(а):

$$(B \to (B \to (B \vee A))) \to ((B \to B) \to (B \to B \vee A)) \eqno{A_2}$$

$$B \to B \vee A \eqno{m. p. \text{дважды}}$$

Откуда мы знаем, что $B \to B$ (самый важный мой вопрос)?

-

Можно как-то эти невообразимые/безумные выверты объяснить проще? Мне их ещё программировать… И какое вообще мы право имеем рассматривать строки таблицы истинности, при которых формула правдива? Что будет, если мы рассмотрим другие строки?

Но вообще, конечно, очень круто. Только не очень понятно.

[Nemiroff]

Kosat в сообщении #996187 писал(а):

Откуда мы знаем, что $B \to B$ (самый важный мой вопрос)?

Ну по вашей ссылке же пример 15.2 есть.

[warlock66613]

Kosat в сообщении #996187 писал(а):

Откуда мы возьмём эти ряды формул?

Придумаем, в разных случаях по-разному. Главное, что если нам удалось их так или иначе придумать - результат у нас в кармане. Суть в том, что для произвольной формулы $C$ часто можно так удачно подобрать $H$, что доказать $H \to C$ и $\neg H \to C$ гораздо проще чем доказать непосредственно само $C$ - и надо этим пользоваться.

Kosat в сообщении #996187 писал(а):

А почему тут импликации, а не конъюнкции?

Можно было бы и конъюнкции (ведь формулы $A \wedge B \to C$ и $A \to (B \to C)$ с обычной, неформальной, человеческой точки зрения - это одно и то же), но гильбертова система аксиом не любит конъюнкций - с ними затруднительно работать - и поэтому я везде где есть альтернатива пишу импликации.

Kosat в сообщении #996187 писал(а):

Нужна алгоритмика, через аксиомы…

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

Kosat в сообщении #996187 писал(а):

Так почему самый левый оператор каждого из четырёх выражений – импликация, а не конъюнкция?..

То же самое что и выше: конъюнкция и вложенная импликация - это одно и то же.

Kosat в сообщении #996187 писал(а):

Но как это соотносится с последующим? Мы же уже доказали истинность $A \vee B \to B \vee A$, разве не так?

Нет, не доказали. Мы доказали $A \vee B \to B \vee A$ из гипотез $A$, $B$. А нужно доказать без гипотез. Поэтому нам нужно ещё трижды доказать $A \vee B \to B \vee A$ - из гипотез $A$, $\neg B$, из гипотез $\neg A$, $B$ и из гипотез $\neg A$, $\neg B$. Затем каждый из этих выводов с помощью теоремы о дедукции превращаем в вывод без гипотез, но при этом они превращаются в выводы уже не $A \vee B \to B \vee A$, а $A \to (B \to (A \vee B \to B \vee A))$, $A \to (\neg B \to (A \vee B \to B \vee A))$ и т. д. соответственно. И только соединив затем все эти четыре вывода в один, получится доказать искомое $A \vee B \to B \vee A$.

Kosat в сообщении #996187 писал(а):

Очень интересно. Мне и это надо будет – во втором задании моей длинной домашней работы (из вывода до применения теоремы дедукции сделать вывод после применения теоремы дедукции).

Здесь это тоже понадобится (это примерно третья часть всей программы навскидку).

Kosat в сообщении #996187 писал(а):

Откуда мы знаем, что $B \to B$ (самый важный мой вопрос)?

Nemiroff в сообщении #996200 писал(а):

Ну по вашей ссылке же пример 15.2 есть.

И именно с загоняния этого примера в программу я и рекомендую начать, потому что доказательство $B \to B$ нужно для теоремы дедукции.

Kosat в сообщении #996187 писал(а):

Но вообще, конечно, очень круто. Только не очень понятно.

Это от незнания теории. Например, я уверен, что вы не сможете объяснить как соотносятся друг с другом булева алгебра и исчисление высказываний. Но, по-моему, это не showstopper - можно и без этого нужные программы написать. Почитать ещё раз материал по вашей ссылке (или эквивалентный) (там кстати система аксиом и само построение теории отличается от той, что в википедии, но во многих случах это не сказывается - вывод $B \to B$ и доказательство теоремы о дедукции подходят к википедийным аксиомам. Разница только там, где есть что-то кроме импликации, так что $B \to \neg \neg B$ и наоборот придётся доказать самому, но если вы освоите теорему о дедукции и трюк с гипотезами, то легко их докажите).

Kosat в сообщении #996187 писал(а):

И какое вообще мы право имеем рассматривать строки таблицы истинности, при которых формула правдива? Что будет, если мы рассмотрим другие строки?

А много ли будет таких строк, учитывая, что общезначимые высказывания в теории высказываний - это тавталогии и только тавталогии? Вы знаете, что такое "тавталогия"?

[Kosat]

warlock66613 в сообщении #996259 писал(а):

Kosat в сообщении #996187 писал(а):
Откуда мы возьмём эти ряды формул?
Придумаем, в разных случаях по-разному.

Мне нужен алгоритм………

-

warlock66613 в сообщении #996259 писал(а):

Главное, что если нам удалось их так или иначе придумать - результат у нас в кармане. Суть в том, что для произвольной формулы $C$ часто можно так удачно подобрать $H$, что доказать $H \to C$ и $\neg H \to C$ гораздо проще чем доказать непосредственно само $C$ - и надо этим пользоваться.

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

-

warlock66613 в сообщении #996259 писал(а):

Kosat в сообщении #996187 писал(а):
А почему тут импликации, а не конъюнкции?
Можно было бы и конъюнкции (ведь формулы $A \wedge B \to C$ и $A \to (B \to C)$ с обычной, неформальной, человеческой точки зрения - это одно и то же), но гильбертова система аксиом не любит конъюнкций - с ними затруднительно работать - и поэтому я везде где есть альтернатива пишу импликации.

Да, действительно. Значит, наверно, мы можем так заменять (хотя «человеческая точка зрения» и аксиомы –не одно и то же).

-

warlock66613 в сообщении #996259 писал(а):

Kosat в сообщении #996187 писал(а):
Нужна алгоритмика, через аксиомы…
Не путайте аксиоматический вывод доказываемой формулы (результат работы программы) с самой программой, которая строит этот вывод. В самой программе можно и нужно пользоваться булевой алгеброй, таблицами истинности.

Хорошо.

-

warlock66613 в сообщении #996259 писал(а):

Kosat в сообщении #996187 писал(а):
Но вообще, конечно, очень круто. Только не очень понятно.
Это от незнания теории. Например, я уверен, что вы не сможете объяснить как соотносятся друг с другом булева алгебра и исчисление высказываний.

«Булева алгебра» – подмножество «исчисления высказываний»?

-

warlock66613 в сообщении #996259 писал(а):

если вы освоите теорему о дедукции и трюк с гипотезами, то легко их докажите).

Трюк – это из всех строк сделать одну?

-

warlock66613 в сообщении #996259 писал(а):

Kosat в сообщении #996187 писал(а):
И какое вообще мы право имеем рассматривать строки таблицы истинности, при которых формула правдива? Что будет, если мы рассмотрим другие строки?
А много ли будет таких строк, учитывая, что общезначимые высказывания в теории высказываний - это тавталогии и только тавталогии? Вы знаете, что такое "тавталогия"?

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