Как из схем аксиом Клини вывести схему аксиом Гильберта №2?

[gefest_md]

Две строки имеет таблица формулы $A\supset A$. Всё равно меньше.

[arseniiv]

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

[Anton_Peplov]

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

так и не разобрался, какая таблица

Вероятно, таблица истинности. В обсуждаемой формуле три переменных - $A, B, C$. Таблица истинности задает значения этой формулы для всех возможных наборов значений $A, B, C$, каковых наборов $2^3 = 8$ ($A$ ложно, $B$ ложно, $C$ ложно; $A$ ложно, $B$ ложно, $C$ истинно;...). В формуле $A \subset A$ одна переменная, и в таблице две строки - значения формулы для истинного и ложного $A$.

[arseniiv]

А ведь точно, спасибо.

[Kosat]

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

Что лень с людьми делает — увяз в попытках доказательства!

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

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

Между тем, глянул теперь упоминаемое в теме-прародительнице доказательство теоремы о дедукции и вижу, что искомая вами выводимость совершенно не нужна. Просто замените формулу $(\alpha+\beta+1)$ в том месте на формулу, соответствующую аксиоме Клини, и применяйте MP к ней не с формулой $(\alpha+\beta)$, а с формулой $(\alpha)$, а к результату применяйте MP, соответственно, с формулой $(\alpha+\beta)$, а не с формулой $(\alpha)$. Результирующая формула $(\alpha+\beta+3)$ получится та же самая. Доказательство поправлено для нашей аксиомы, всё.

Фантастика! Вроде работает - одним выстрелом двух зайцев! Спасибо!

[arseniiv]

Не за что! Вот если бы я вчитался в тот ваш пост вовремя!

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

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

Построеня выводов в исчислении высказываний или вообще (включая результаты о выводимости типа теоремы о дедукции)? А что насчёт соображений, приведённых warlock66613? Другие соображения насчёт системы Клини и использования теоремы о дедукции (которая у нас теперь есть) я где-то приводил, но, наверно, действительно в туманной форме. Ещё о том же писал Xaositect, но не помню, насколько полно и где.

Построение вывода по шагам и построение вывода из других выводов с помощью теоремы о дедукции, теоремы о $F,\Gamma\vdash G,G,\Gamma\vdash H\Rightarrow F,\Gamma\vdash H$ и прочих «метатеорем» можно поставить в аналогию написанию программы в машинных кодах и её компиляции с какого-нибудь более человекопонятного языка высокого уровня. В обоих вторых случаях для получения конкретного вывода надо знать построения из доказательств теорем и алгоритмы компилятора, для получения же факта выводимости достаточно знать только утверждения теорем или иметь компилятор; обычно интересует только факт выводимости.

[Kosat]

Ага.

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

Построения выводов в исчислении высказываний или вообще (включая результаты о выводимости типа теоремы о дедукции)?

Построение выводов в исчислении высказываний (из аксиом). Что на бумаге, что (затем) в ПК.

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

А что насчёт соображений, приведённых warlock66613
А что насчёт соображений, приведённых warlock66613? Другие соображения насчёт системы Клини и использования теоремы о дедукции (которая у нас теперь есть) я где-то приводил, но, наверно, действительно в туманной форме. Ещё о том же писал Xaositect, но не помню, насколько полно и где.

Я не знаю, как сделать доказательства для каждой строки таблиц истинности, и даже если б знал, не понимаю, как именно "пошагово обрабатывать" наше синтаксическое дерево операций.

[arseniiv]

Хм, пока я особо в них не вглядывался…

Вот возьмём в пример доказательство $\vdash F\equiv\neg A\vee B\to(A\to B)$. Для этого покажем всяческие $[\neg]A,[\neg]B\vdash F$ и покажем, что из всех их это следует.

1‒2. $[\neg]A,B\vdash F$. Теоремой о дедукции получаем $[\neg]A,B,\neg A\vee B,A\vdash B$, что верно, потому что $B\vdash B$.

3. $A,\neg B\vdash F$. Теоремой о дедукции получаем $A,\neg B,\neg A\vee B\vdash B$. Тут так просто не отделаешься. Посмотрим на аксиому (8). С любезной помощью теоремы о дедукции она превращается в выводимость $M\to P,N\to P,M\vee N\vdash P$, так что если мы покажем $\Gamma\vdash M\to P$, $\Gamma\vdash N\to P$, то получим $\Gamma,M\vee N\vdash P$, то есть, через теорему о дедукции, $\Gamma,M\vdash P;\Gamma,N\vdash P\Rightarrow \Gamma,M\vee N\vdash P$. У нас есть способ доказательства с дизъюнкцией в гипотезах! Применим его.

(а) $A,\neg B,\neg A\vdash B$. Тут нам поможет факт $M,\neg M\vdash\text{что угодно}$ [*].

(б) $A,\neg B,B\vdash B$. Это верно уже ясно почему.

Раз (а) и (б), то и с 3 мы разобрались.

4. $\neg A,\neg B\vdash F$. Теоремой о дедукции получаем $\neg A,\neg B,\neg A\vee B, A\vdash B$. Почему это верно, уже разобрано.

Теперь нам надо показать, что 1‒4 вообще имеют какое-то отношение к $\vdash F$. Для этого сначала покажем $\Gamma,M\vdash P;\Gamma,\neg M\vdash P\Rightarrow\Gamma\vdash P$. Это можно показать, имея $\vdash M\vee\neg M$ [**] и ту штуку, которую мы получили в 3 из аксиомы (8).

Теперь ясно, что если мы можем показать $A\vdash P$ и $\neg A\vdash P$, то получим и $\vdash P$. Если $A$ — переменная, только и встречающаяся в $P$, этого достаточно (и, если доказать первые два в какой-то комбинации не получается, мы параллельно можем попытаться доказать $A\vdash\neg P$, $\neg A\vdash\neg P$, чтобы убедиться, что и не получится; но почему это должно быть убедительным, вопрос отдельный). Если же в $P$ встречается две переменные, тогда имеем $A,[\neg]B\vdash P;\neg A,[\neg]B\vdash P\Rightarrow[\neg]B\vdash P$ и, если все четыре вывода у нас есть, в конце мы получим $\vdash P$. Если переменных больше, «собираем» их аналогично до победного конца.

[*] и [**] сейчас доказвать не хочу, так что можете попробовать сами.

-- Сб апр 18, 2015 23:45:29 --

(Оффтоп)

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

[Kosat]

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

3. $A,\neg B\vdash F$. Теоремой о дедукции получаем $A,\neg B,\neg A\vee B\vdash B$. Тут так просто не отделаешься. Посмотрим на аксиому (8). С любезной помощью теоремы о дедукции она превращается в выводимость $M\to P,N\to P,M\vee N\vdash P$, так что если мы покажем $\Gamma\vdash M\to P$, $\Gamma\vdash N\to P$, то получим $\Gamma,M\vee N\vdash P$, то есть, через теорему о дедукции, $\Gamma,M\vdash P;\Gamma,N\vdash P\Rightarrow \Gamma,M\vee N\vdash P$.

Сплошная теорема о дедукции. На уровне кругов Эйлера это понятно. Правильно ли я понял, что как только мы видим дизъюнкцию в гипотезах, мы запускаєм эту последовательность? Похоже на метод резолюций.

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

У нас есть способ доказательства с дизъюнкцией в гипотезах! Применим его.

Как это вообще записать?.. У меня против каждой строки должен слоять номер схемы аксиом или modus ponens. Здесь так всё включено одно в другое...

Извините за глупые вопросы.

[arseniiv]

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

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

Видимо, да. Особо не задумывался и подводных камней не нашёл.

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

Похоже на метод резолюций.

И не только! Упомянутые мной ни к селу ни к городу выше analytic tableaux тоже чем-то похожи. Правда, там ещё эквивалентности применяются для избавления от $\to,\leftrightarrow$ и протаскивания отрицаний к переменным. Этот метод основан чисто на значениях формул — без вывода из аксиом и MP, потому тут я его описывать не буду.

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

Как это вообще записать?.. У меня против каждой строки должен слоять номер схемы аксиом или modus ponens. Здесь так всё включено одно в другое...

Да, как я и говорил, тут мы получаем не вывод, а «программу построения вывода». Сам вывод получится, если смотреть, что там теорема о дедукции, применённая к конкретным выводам, даёт, начиная с упомянутых очевидных выводов в три/одну строку.

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

Извините за глупые вопросы.

Уверяю, вполне нормальные вопросы. Скорее, у меня нет нормальных (точных) ответов — я особо автоматическим построением вывода в исчислении высказываний/исчислении предикатов не интересовался. (Надеюсь, от текущих какая-то польза есть?)

[Kosat]

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

Уверяю, вполне нормальные вопросы. Скорее, у меня нет нормальных (точных) ответов — я особо автоматическим построением вывода в исчислении высказываний/исчислении предикатов не интересовался. (Надеюсь, от текущих какая-то польза есть?)

Есть (хотя повсеместная замена импликации через теорему о дедукции (?) и применение к дизъюнктам недо-метода резолюций (??) и вызывают у меня определённые сомнения). Но учитывая то, что мне нужно решить любые три из первых четырёх задач, я наверно решу четвёртую, а не третью (с самого начала склонялся к этому же).