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

[Kosat]

Как из системы схем аксиом Клини:
\begin{gather} A\to(B\to A) \\ (A\to B)\to((A\to(B\to C))\to(A\to C)) \\ A\to(B\to A\wedge B) \\ A\to A\vee B \\ A\to B\vee A \\ A\wedge B\to A \\ A\wedge B\to B \\ (A\to B)\to((C\to B)\to(A\vee C\to B)) \\ (A\to B)\to((A\to\neg B)\to\neg A) \\ \neg\neg A\to A \end{gather}$

вывести вторую схему аксиом Гильберта:

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

?

Заранее спасибо всем откликнувшимся.

Моя попытка решения. Я полагаю, что различные схемы аксиом в двух наборах (Гильберта и Клини) должны выводить друг друга. Я посмотрел на те три схемы аксиом Гильберта, которые отсутствуют у Клини, и остановил свой выбор на второй, весьма похожей на выводимую. Я сделал подстановки, чтобы это походило на то, что нужно вывести и применил ещё первую схему аксиом и правило modus ponens. Но, хоть полученное и похоже на то, что нам нужно, что дальше делать, не знаю.

$$1: A = A \to B$$ $$2: C = A \to C$$ $$3: ((A \to B) \to A) \to ((A \to B) \to (A \to (A \to C)) \to ((A \to B) \to (A \to C)))\eqno{(A2)}$$ $$4: A \to (B \to A)\eqno{(A1)}$$ $$5: ((A \to B) \to (A \to (A \to C))) \to ((A \to B) \to (A \to C))\eqno{(m.p. 4, 3)}$$

Deggial: эта - подзадача на для решения другой задачи

[gefest_md]

Kosat, доказательство теоремы дедукции позволяет быстро находить, как мне кажется, любой вывод, где есть главный знак импликации. В Вашем примере можно легко построить вывод $A\to(B\to C),\ A\to B\vdash A\to C$ с помощью второй аксиомы Клини. Затем можно применить приём, изложенный в доказательстве теоремы дедукции.

[Kosat]

gefest_md, дело в том, что доказательство теоремы дедукции, на которое я смотрю, как раз и использует вторую схему аксиом Гильберта. А мне надо - Клини. Должно же быть просто...

[gefest_md]

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

gefest_mdдоказательство теоремы дедукции, на которое я смотрю, как раз и использует вторую схему аксиом Гильберта. А мне надо - Клини.

У Клини тоже можно посмотреть теорему дедукции. Там, конечно, система аксиом Клини используется.

[Kosat]

У меня нет его книги и мне кажется, есть более простой способ.

[gefest_md]

Сомневаюсь, что кто-то возьмётся искать более простой формальный вывод.

[Kosat]

А что это за доказательство? Чего? И что такое "regula"?

[gefest_md]

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

А что это за доказательство? Чего? И что такое "regula"?

Это формальное доказательство последней, 13-ой, формулы в списке. Regula 2 переводится как правило 2 (modus ponens).

[arseniiv]

gefest_md в сообщении #1005004 писал(а):

Сомневаюсь, что кто-то возьмётся искать более простой формальный вывод.

Я возьмусь. Тут у нас (точнее, у Клини) есть конъюнкция, вот ею и надо пользоваться.

Как видно, аксиома (2) Клини и аксиома из набора Гильберта имеют вид соответственно $A\to(B\to C)$ и $B\to(A\to C)$. Перейти от одного к другому можно через $A\wedge B\to C$, эквивалентное обоим. Дополнительные подсказки нужны?

[Kosat]

gefest_md в сообщении #1005052 писал(а):

то формальное доказательство последней, 13-ой, формулы в списке.

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

[arseniiv]

(Оффтоп)

По-моему всё-таки человекоудобнее через конъюнкцию. Может оказаться вдруг и длиннее (но не верится) — но будет всяко понятным: видна идея, остаётся немного техники.

[gefest_md]

arseniiv, если я правильно понял Вы хотите использовать импортацию, экспортацию и, тогда, и "транзитивность". Мне кажется так намного длиннее получится: надо включить в главный блок формальные доказательства всех этих принципов.

[arseniiv]

Хм, чего-то длинновато пока получается, или не туда смотрю.

-- Сб апр 18, 2015 00:25:04 --

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

[gefest_md]

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

чего-то длинновато пока получается

13 строк - много или мало для этой формулы? Наверное надо смотреть и на её сложность. Таблица этой формулы имеет восемь строк. Доказательство же формулы $A\supset A$ имеет пять строк, - а её таблица одну строку. $\frac{8}{13}$ ближе к $1$, чем $\frac{1}{5}$.

[arseniiv]

(А какая таблица? Analytic tableau которая?)

В общем, дело-то в том, что этот вывод излишен, задача была (см. пометку Deggial) в изменении доказательства теоремы о дедукции так, чтобы оно прокатило с аксиомами Клини вместо используемой в образце системе Гильберта.