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

[arseniiv]

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

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

Не, ни в каком смысле.

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

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

Ну тогда выведите сначала все аксиомы Клини

Схемы аксиом для исчисления высказываний писал(а):

\begin{gather} F\to(G\to F) \\ (F\to G)\to((F\to(G\to H))\to(F\to H)) \\ F\to(G\to F\wedge G) \\ F\to F\vee G \\ F\to G\vee F \\ F\wedge G\to F \\ F\wedge G\to G \\ (F\to G)\to((H\to G)\to(F\vee H\to G)) \\ (F\to G)\to((F\to\neg G)\to\neg F) \\ \neg\neg F\to F \end{gather}

из ваших.

Эти аксиомы дают серию полезных выводимостей $F,G\vdash F\wedge G$, $F\vdash F\vee G$ и т. д., которые можно использовать для «собирания» формул (введения связок, как в указанном) и их «разбирания» (удаления связок, как в $F\wedge G\vdash F$).

(Оффтоп)

Вообще я бы убрал скобки в $a\to(b\to(c\to\ldots))$ и написал так:

\begin{gather} F\to G\to F \\ (F\to G)\to(F\to G\to H)\to F\to H \\ F\to G\to F\wedge G \\ F\to F\vee G \\ F\to G\vee F \\ F\wedge G\to F \\ F\wedge G\to G \\ (F\to G)\to(H\to G)\to F\vee H\to G \\ (F\to G)\to(F\to\neg G)\to\neg F \\ \neg\neg F\to F \end{gather}

Если обращение с формулами освоено хорошо, такое дополнительное соглашение о расстановке скобок может помогать чтению.

[warlock66613]

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

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

Да.

-- 27.03.2015, 20:47 --

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

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

В общем, булева алгебра является точной моделью исчисления высказываний. Тавталогии исчесления высказываний - это тождества булевой алгебры. Поэтому проверить выводимость формулы очень легко - надо просто проверить тождественность соотвествующей формулы булевой алгебры.
Более того, алгоритм, вычисляющий формулу булевой алгебры для определённых значений входящих переменных, несложно превратить в алгоритм, доказывающий соответствующую формулу в исчислении высказываний. Например, как вы будете проверять тождественность $A \to A$?. Возьмёте сначала $A = 1$, подставите и посчитаете эту импликацию - получится истина ($1$). Потом возьмёте $A=0$ - получится опять истина. Всё, все варианты перебрали - значит тождество. Как её доказывать? Да то же самое. Сначала доказываем из гипотезы $A$ - это элементарно делается. Потом из гипотезы $\neg A$ - опять элементарно. Всё, можно считать, что мы доказали эту формулу, поскольку с помощью дедукции эти два доказательства просто превращаются в искомое полное доказательство.

[Kosat]

arseniiv в сообщении #996549 писал(а):

Ну тогда выведите сначала все аксиомы Клини
Схемы аксиом для исчисления высказываний
писал(а):
...
из ваших.

Я не понимаю алгоритма и при выводе на бумаге. Делаю наугад. Такие дела.

-- 27.03.2015, 23:11 --

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

Более того, алгоритм, вычисляющий формулу булевой алгебры для определённых значений входящих переменных, несложно превратить в алгоритм, доказывающий соответствующую формулу в исчислении высказываний. Например, как вы будете проверять тождественность $A \to A$?. Возьмёте сначала $A = 1$, подставите и посчитаете эту импликацию - получится истина ($1$). Потом возьмёте $A=0$ - получится опять истина. Всё, все варианты перебрали - значит тождество. Как её доказывать? Да то же самое. Сначала доказываем из гипотезы $A$ - это элементарно делается. Потом из гипотезы $\neg A$ - опять элементарно. Всё, можно считать, что мы доказали эту формулу, поскольку с помощью дедукции эти два доказательства просто превращаются в искомое полное доказательство.

Меня интересует вот этот момент: "Сначала доказываем из гипотезы $A$ - это элементарно делается. Потом из гипотезы $\neg A$ - опять элементарно." В алгоритмической плоскости, для любых входных формул. Не ясно...

[warlock66613]

Kosat, алгоритм проверки формулы по таблице истинности представляете? Когда сначала для каждой буквы устанавливается - истинна она или ложна, затем для выражений, образованных из этих букв, затем для выражений из выражений и так далее, пока до формулы не дойдём.
Например, та же $A \vee B \to B \vee A$. Начинаем с четырёх стартовых позиций - четырёх строк таблицы истинности. Например, для случая $A=0$, $B=1$. Вычисляем $A$: $A=0$. Вычисляем $B$: $B=1$. Затем вычисляем $A \vee B = 0 \vee 1 = 1$. Затем вычисляем $B \vee A = 1 \vee 0 = 1$. Наконец вычисляем всё выражение $A \vee B \to B \vee A = 1 \to 1 = 1$. А откуда мы знаем, что $0 \vee 1 = 1$, $1 \to 1 = 1$ и т. д.? А у нас должны быть забиты в программу таблички, в которых все возможные варианты записаны.

Доказательство производится также. Только вместо "рассчитать значение подвыражения $X$ - $1$ или $0$" для каждой подформулы $X$ нужно написать доказательство - либо доказательство $X$, либо доказательство $\neg X$. Например, для случая $\neg A$, $B$. Доказываем $\neg A$: $\neg A$. Доказываем $B$: $B$. Затем доказываем $A \vee B$. Как? А у нас должны быть забиты в программу таблички, в которых все возможные варианты записаны. Только теперь это должны быть таблички функций. В предыдущем случае у нас для дизъюнкции была табличка из четырёх строк, так?
Вот такая:

x | y | x V y
0 | 0 |   0
0 | 1 |   1 
1 | 0 |   1
1 | 1 |   1

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

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

Видите - всё очень просто, надо только накодить эти таблички функций. Всего функций будет 14 штук - две для отрицания и по четыре для остальных операций.

Если эта идея понятна, можете начинать писать функцию для первой строки таблицы импликации. Я вам помогу.

[Kosat]

Идея мне понятна довольно приблизительно. Как ваши нынешние слова соотносятся с предыдущим доказательством/выводом (опустим необходимость «вклинить» доказательство $A \to A$ непосредственно в тело основного вывода)? Дело в том, что я по-прежнему слаб даже в доказательствах на бумаге. Я понимаю, что нам сейчас нужно доказать $\neg A \to (\neg B \to \neg (A \to B))$, но как это сделать? И даже когда мы докажем парочку формул, как их скомбинировать? Например, $A \to \neg \neg A$? Извините за задержки в общении - я пытался разобраться в сказанном вами и у меня есть и другие задания.

Вот эти схемы аксиом, похоже, у нас используются (судя по примерам входных данных):

$$1: A \to (B \to A)$$ $$2: (A \to B) \to ((A \to B \to C) \to (A \to C))$$ $$3: A \wedge B \to A$$ $$4: A \wedge B \to B$$ $$5: A \to (B \to A \wedge B)$$ $$6: A \to A \vee B$$ $$7: B \to A \vee B$$ $$8: (A \to Q) \to ((B \to Q) \to (A \vee B \to Q))$$ $$9: (A \to B) \to ((A \to \neg B) \to \neg A)$$ $$10: \neg \neg A \to A$$

Хотя, наверно, можна брать и другие. Суть же не в этом...

Благодарен за помощь.

[Deggial]

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

[arseniiv]

(Оффтоп)

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

Хотя, наверно, можна брать и другие. Суть же не в этом...

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

[Kosat]

(Оффтоп)

arseniiv в сообщении #998209 писал(а):

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

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

[arseniiv]

(Оффтоп)

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

Все наборы схем аксиом имеют одинаковую выразительную мощность.

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

[Kosat]

Вторая схема аксиом, из тех, которые, похоже, у нас используются (судя по примерам входных данных), звучит не

$$2: (A \to B) \to ((A \to B \to C) \to (A \to C))$$

, а

$$2: (A \to B) \to ((A \to (B \to C)) \to (A \to C))$$

[Kosat]

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

Если эта идея понятна, можете начинать писать функцию для первой строки таблицы импликации. Я вам помогу.

Вот доказательство первой строки таблицы импликации по аксиоматике в Википедии:

$$\neg A, \neg B \vdash A \to B$$

$$\Box \neg A \to (\neg A \to B) \eqno{A}_{9}$$

$$\neg A \to B \eqno{m. p.}\blacksquare$$

Вторая доказывается абсолютно аналогично. Вот она:

$$\neg A, B \vdash A \to B$$

Доказать же третью в данной аксиоматике я не знаю как. Внушает надежды десятая схема аксиом, но проблема в том, что последовательному применению modus ponens мешает наличие В и его отрицания в последовательных импликациях. Вот третья строка, как я её понимаю:

$$A, \neg B \vdash \neg (A \to B)$$

Четвёртую вы уже доказали:

$$A, B \vdash A \to B$$

Хуже складывается дело с аксиоматикой, которая дана мне в одной из задач (Клини?). Там вообще не густо с отрицаниями, есть только всё та же схема аксиом (только здесь она не десятая, а девятая), всё с теми же проблемами. Как доказать все четыре строки таблицы истинности для импликации я не знаю.

Пока делаю остальные задачи - дошёл уже до эффективного формирования ПОЛИЗа. Смотрю и смотрю на самые начальные строки доказательства вашего примера. Должна быть связь с рекомендованным вами "последовательным сниманием кожуры" с выражения, но я её плохо вижу. Но, по внимательному прочтению разнообразных источников, начинаю осознавать ваш способ как единственно возможный. Помогите, пожалуйста - я же сделал доказательство первой (и второй) строк таблицы импликации по аксиоматике в Википедии.

[Kosat]

Я сделал первую задачу (всё-таки приложу файл pdf), теперь думаю над второй. Подробно растолкованный пользователем warlock66613 способ включал теорему о дедукции, которая находится под номеро 15.4 по моей ссылке Формализованное исчисление высказываний. Но там используется не та система схем аксиом, что мне нужно. Как из системы схем аксиом Клини (см. выше в теме) вывести вторую схему аксиом Гильберта??? Заранее спасибо всем откликнувшимся.

[Kosat]

Я решил и вторую задачу. При рассмотрении четвёртой я столкнулся с трудностью осуществления шага 1б в доказательстве теоремы о дедукции 15.4. Вот удачные и неудачные примеры реализации схем аксиом и правил вывода исчисления предикатов, которые мне удалось вычленить из примеров к четвёртому заданию. Они настолько отличаются от того, что дано в Википедии, и настолько странно выглядят, что я в затруднении (да и с имеющимся в Википедии я не знаю, как сделать этот шаг). Особенно надеюсь и смиренно уповаю на помощь уважаемого arseniiv и других интересующихся (конструктивной?) логикой пользователей.

[arseniiv]

Выглядят, действительно, чуть странно. Видимо, @ и ? обозначают кванторы и, видимо, это соответственно $\forall,\exists$. Формулы видны из чистого исчисления предикатов, его же с равенством, и всего этого с арифметикой. Судя по всему, вы должны написать программу, которая проверяет, правильны ли выводы или нет (это не то же самое, что получать выводы данных формул или показывать, что вывода нет; проще). Чего ещё сказать, не придумал пока.

На всякий случай переведу все небуквенные символы из формул в том файле, если что-то ещё непонятно:

( ) , -> & ! @ ? = 0 ' + *

$${(}\;{)}\;{,}\qquad{\to}\;{\wedge}\;{\neg}\;{\forall}\;{\exists}\qquad{=}\qquad{0}\;{'}\;{+}\;{\cdot}$$

Первые две группы вам знакомы; дальше идёт двуместный предикатный символ для обозначения равенства; потом идут чисто арифметические: константа (или нульместный функциональный символ) для обозначения нуля, одноместный ф. символ для обозначения следующего числа ($n'$ — это $n$ плюс 1), двуместные ф. символы для сами знаете чего.

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

При рассмотрении четвёртой я столкнулся с трудностью осуществления шага 1б в доказательстве теоремы о дедукции 15.4.

Ничего напоминающего 16 там не нашёл.

UPD: Если имеется в виду следствие 15.6, там математической индукцией по числу гипотез.

(Оффтоп)

Я так всё расписал только лишь на случай, если где-то дыра. Не ругайте за замещение К. О..

[Kosat]

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