Несовершенная система аксиом исчисления высказываний

[SomePupil]

(1a) $A\to (B\to A)$

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

(2a)$A \wedge B \to A$

(2b)$A \wedge B \to B$

(2c) $(C \to A)\to ((C\to B)\to(C \to A\wedge B))$

(3a) $A \to A \vee B$

(3b) $B \to A \vee B$

(3c) $(A \to C) \to ((B \to C)\to(A \vee B \to C))$

(4a) $(A \to B) \to (\neg B \to \neg A)$

(4b) $A \to \neg \neg A$

(4c) $\neg \neg A \to A$

Вот уже полсеместра мы пользуемся этой системой аксиом. И я до сих пор не доказал около половины семинарских выводимостей, только потому что в системе отсутствуют такие штуки, как закон исключенного третьего, третья аксиома Мендельсона (я про аксиому из его учебника) или $\neg A \to (A \to B)$. Из-за этого я не могу вывести даже такие банальные вещи, как $(\neg A \to A)\to A.$ Я нахожусь в том же положении, что и знахарь из фильма "Знахарь" (нет инструмента,

инструмента для вывода отрицаний высказываний)

Как можно вывести из системы закон исключенного третьего или какую-нибудь его альтернативу, дабы получить удобные правила вывода?

P. S. Закон снятия двойного отрицания совсем не помогает. У меня даже есть подозрения, что он слабее закона исключенного третьего.

[george66]

$A\to(B\to A)$
$(B\to A)\to(\neg A\to\neg B)$
поэтому
$A\to(\neg A\to\neg B)$

Но да, по таким системам научиться трудно.

[arseniiv]

(Припоздал.)

SomePupil в сообщении #1316530 писал(а):

P. S. Закон снятия двойного отрицания совсем не помогает. У меня даже есть подозрения, что он слабее закона исключенного третьего.

Зависит от контекста. Если взять интуиционистскую логику, добавление $\neg\neg A\to A$ равносильно добавлению $A\vee\neg A$. Так что если ваша система без аксиомы снятия двойного отрицания не слабее интуиционистской логики, всё будет OK. Это можно увидеть, получив аксиому, в указанной статье (чуть выше, чем раздел, на который ссылка) названную NOT-2 (одну из указанных там альтернатив NOT-1 легко получить из контрапозиции), что нетрудно: $\neg A\to(\neg B\to\neg A)$, потом используем это вместе с $(\neg B\to\neg A)\to(A\to B)$, тоже легко получаемому из контрапозиции.

То есть задача решаема, вот может после вывода разных приведённых там фактов об отрицании вам станет даже понятно, что делать для вывода исключенного третьего.

[Sinoid]

SomePupil в сообщении #1316530 писал(а):

(1a) $A\to (B\to A)$

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

(2a)$A \wedge B \to A$

(2b)$A \wedge B \to B$

(2c) $(C \to A)\to ((C\to B)\to(C \to A\wedge B))$

(3a) $A \to A \vee B$

(3b) $B \to A \vee B$

(3c) $(A \to C) \to ((B \to C)\to(A \vee B \to C))$

(4a) $(A \to B) \to (\neg B \to \neg A)$

(4b) $A \to \neg \neg A$

(4c) $\neg \neg A \to A$

Не знаю, ИМХО, вполне себе употребляемая аксиоматика. В задачнике Лаврова, Максимовой с успехом употребляется и аксиоматика такого же содержания, только на аксиому меньше. Помнится, я тогда не мог (конкретно) вывести формулу $(A\supset B)\equiv(\neg A\vee B)$, так это сделал mihaild в одной из моих тем. А так (с несколькими подсказками на форуме) у меня, как будто, все задачи на выводимость в ИВ из того сборника получились. Помнится, я в черновиках, ну, очень не слабо использовал теорему о дедукции, а потом в чистовике исключал ее. Попробуйте для начала порешать тот задачник.

[george66]

Тут даже нет аксиомы $A\to A$, попробуйте её вывести из первых двух. Вообще, учиться надо натуральному выводу.

[Sinoid]

george66 в сообщении #1316608 писал(а):

Тут даже нет аксиомы $A\to A$, попробуйте её вывести из первых двух.

А ее обычно и не приводят, она выводится так, как вы сказали и она служит для иллюстрации простейшего вывода (в ИВ).

[SomePupil]

Sinoid в сообщении #1316589 писал(а):

Помнится, я в черновиках, ну, очень не слабо использовал теорему о дедукции, а потом в чистовике исключал ее.

+ Я тоже так делаю)
У нас тоже запрещено пользоваться леммой о дедукции. Поэтому непонятно, как из $\neg A \to (\neg \neg A \to \neg \neg B)$ получить $\neg A \to (A \to B).$

Почитаю ссылки, подумаю, может, придумаю что-нибудь.

[arseniiv]

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

[SomePupil]

Кстати, препод разрешила пользоваться другой системой аксиом, так что проблема разрешилась сама по себе.

P. S. Но осадок остался. В теме я все-таки проведу доказательство.

[SomePupil]

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

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

Именно так.

Простая заметка: если $A -$ теорема, то $B \to A$ тоже теорема, так как по первой аксиоме $A \to (B \to A).$

По-видимому, начать надо с вывода $(\neg B \to \neg A) \to (A \to B).$ Если он и не даст сразу закон исключенного третьего, то все равно к нему приблизит.

$(\neg \neg A \to \neg \neg B) \to (A \to (\neg \neg A \to \neg \neg B)) -$ по аксиоме 1а.

$(\neg B \to \neg A) \to ((\neg \neg A \to \neg \neg B) \to (A \to (\neg \neg A \to \neg \neg B))) -$ см. заметку.

Эта формула имеет структуру, подходящую для аксиомы 1б. После применения оной получаем:

$(\neg B \to \neg A) \to (A \to (\neg \neg A \to \neg \neg B)).$

Далее:

$(\neg B \to \neg A)\to((A \to (\neg \neg A \to \neg \neg B))\to((A \to \neg \neg A)\to (A \to \neg \neg B))) -$ тут в правой части аксиома 1б.

Эта формула опять имеет удобную структуру, при этом один из составляющих этой формулы получен строкою выше. После применения аксиомы получаем:

$(\neg B \to \neg A) \to ((A \to \neg \neg A)\to (A \to \neg \neg B)).$

Применяем аксиому 1б второй раз:

$(\neg B \to \neg A) \to (A \to \neg \neg B).$

Дальше $(A \to (\neg \neg B \to B))\to((A\to \neg \neg B) \to (A \to B)),$ откуда
$(A \to \neg \neg B) \to (A \to B) -$ вот тут и пригодился закон снятия двойного отрицания.

Остается трафаретом приложить теорему
$(\neg B \to \neg A) \to ((A \to \neg \neg B) \to (A \to B))$

к аксиоме 1б и получить необходимую импликацию:
$(\neg B \to \neg A) \to (A \to B).$

Далее из теоремы
$\neg A \to ((\neg B \to \neg A)\to(A \to B))$
легко получить
$\neg A \to (A \to B).$

Отсюда уже, наверное, близко до исключенного третьего.

-- 01.06.2018, 15:39 --

$\neg (A \vee \neg A) \to (\neg\neg A\to(\neg A \to B))$
$\neg (A \vee \neg A) \to (\neg A \to B)$
$\neg (A \vee \neg A) \to B$
$\neg B \to \neg\neg(A \vee \neg A)$
Вместо $B$ ставим отрицание любой теоремы: $B = \neg (A \to A)$ и после очевидных преобразований получаем $A \vee \neg A.$
Ура-а!

[warlock66613]

А я как раз для такой или почти для такой аксиоматики когда-то давно писал автопруфер — Haskell изучал. Правда, доказательство $A \to A$ туда жёстко зашито, так как служит одним из базовых элементов.

-- 02.06.2018, 02:31 --

А, нет, всё-таки не совсем для такой: (4b) и (4c) я доказывал.