Вывести формулу в гильбертовском исчислении высказываний

[Viktoriya12]

Помогите вывести формулу: $ (A \to \neg B) \to (\neg A \lor \neg B) $
в гильберстовском исчислении высказываний. У меня аксиомы не совсем такие, как в этой статье в википедии, но будет нелохо, если и с помощью их будет построен вывод)

[Maslov]

А правилами введения-удаления логических связок можно пользоваться?

[Viktoriya12]

Нет, разрешено пользоваться только аксиомами и правилом вывода. Еще у меня только 10 аксиом, 5-ой, которая описана в статье, в википедии, нет.
Я уже не знаю, что делать. Вроде не так много аксиом можно применить, чтобы получить конкретно данную формулу, но ничего в итоге не получается.

[Maslov]

Если бы было можно пользоваться теоремой о дедукции, то все было бы понятно:
1. $\vdash A \to ((A \to \neg B) \to (\neg A \lor \neg B))$
2. $\vdash \neg A \to ((A \to \neg B) \to (\neg A \lor \neg B))$
3. $A_8: (A \to C) \to ((B \to C) \to (A \lor B \to C))$
А без теоремы о дедукции даже не знаю, что сказать...

Т. е., конечно, можно взять доказательство теоремы о дедукции и с его помощью явно построить вывод 1. и 2., но там шагов получится несколько десятков :(

[Viktoriya12]

Извините, я не совсем понимаю. Теорема о дедукции это же "если $ H, A \vdash B $, то $ H \vdash A \to B $ , где H - это гильбертовские аксиомы" ?. Не могли бы вы поподробней объяснить как при применении теоремы о дедукции получить формулы 1. и 2.?

[Maslov]

Viktoriya12 в сообщении #576983 писал(а):

Теорема о дедукции это же "если $ H, A \vdash B $, то $ H \vdash A \to B $ , где H - это гильбертовские аксиомы" ?

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

Что же касается формул 1 и 2, то схема такая.

Даказываем простенькую выводимость

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

потом 2 раза применяем теорему о дедукции, в результате получаем формулу 1.

Аналогичным образом получаем формулу 2.

[Viktoriya12]

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

[Viktoriya12]

На всякий случай, я правильно понимаю, что $ A, A \to \neg B \vdash \neg A \lor \neg B$ получается из акисомы 2: $ ((A \to (B \to C)) \to ((A \to B) \to (A \to C))) $ подстановкой вместо $ B $ формулы $ \neg B $ и вместо $ C $ формулы $ \neg A \lor \neg B $, а $ \neg A, A \to \neg B \vdash \neg A \lor \neg B$ можно сразу получить из аксиомы 6: $ \neg A \to ( \neg A \lor \neg B) $ ?

[Maslov]

Viktoriya12 в сообщении #577437 писал(а):

я правильно понимаю, что $ A, A \to \neg B \vdash \neg A \lor \neg B$ получается из акисомы 2: $ ((A \to (B \to C)) \to ((A \to B) \to (A \to C))) $ подстановкой вместо $ B $ формулы $ \neg B $ и вместо $ C $ формулы $ \neg A \lor \neg B $,

$A, A \to \neg B \vdash \neg A \lor \neg B$
получается последовательным применением modus ponens и аксиомы 7: $B \to A \lor B$

Viktoriya12 в сообщении #577437 писал(а):

а $ \neg A, A \to \neg B \vdash \neg A \lor \neg B$ можно сразу получить из аксиомы 6: $ \neg A \to ( \neg A \lor \neg B) $

Да.