Помогите доказать правило

[natalk20]

Доказать, что правило удаления дизъюнкции (Генцена) допустимо в ИВ.
Г1|->(AvB);Г2,A|->C;Г3,B|->C
Г1, Г2, Г3, |->C

Доказываю так:
1. Г2|->A->C (по теореме о дедукции)
2. (AvB) -> (CvB) ( не знаю, как обосновать)
3. Г3|->B->C (по теореме о дедукции)
4. (СvB) -> (CvС) ( не знаю, как обосновать)
5. (AvB) -> (CvC) (по следствию из теоремы о дедукции)
6. (AvB), A -> C, B ->C |-> C (из (5) и свойства идемпотентности CvC <-> C)

Помогите, пожалуйста, разобраться, верна ли схема доказательства? Если да, то как обосновать переходы 2 и 4?

@темы: Математическая логика

Comments

[Adjirranirr]

Аксиомы и правила вывода какие?

[Adjirranirr]

Вроде и у Гильберта, и у Клини есть аксиома
⊢ (A → C) → ((B → C) → (A ∨ B → C)).
В данном случае, использовать стоит ее.

Ваша схема не верна, так как формулы (A∨B) → (C∨B) и (C∨B) → (C∨C) не общезначимы. (Контрпримеры соответственно A = 1, B = 0, C = 0 и B = 1, C = 0).

[Гость]

Спасибо, что откликнулись.
А если сделать так:
1. Г2|->A->C (по теореме о дедукции)
2. Г3|->B->C (по теореме о дедукции)
3. (A → C) → ((B → C) → (A ∨ B → C)) (из (1) и аксиомы 8)
4. (B → C) , (B → C) → (A ∨ B → C) ⊢ (A ∨ B → C) ( из (2) и m.p.)
5. Г1 ⊢ A ∨ C (посылка)
6. (A ∨ B) , (A ∨ B) → C) ⊢ C (из (5) и m.p.)

[natalk20]

В п.5 опечатка. Должно быть Г1 ⊢ A ∨ B (посылка)

[Adjirranirr]

Мне кажется, проще будет как-то
1. Г₂ ⊢ A → C
2. Г₃ ⊢ B → C
3. ∅ ⊢ (A → C) → ((B → C) → (A ∨ B → C))
4. A → C ⊢ (B → C) → (A ∨ B → C)
5. Г₂ ⊢ (B → C) → (A ∨ B → C)
6. Г₂, B → C ⊢ A ∨ B → C
7. Г₂, Г₃ ⊢ A ∨ B → C
8. Г₂, Г₃, A ∨ B ⊢ C
9. Г₁ ⊢ A ∨ B
0. Г₁, Г₂, Г₃ ⊢ C

Нагляднее. Ваш вариант, вероятно, тоже сойдет — я не знаю, с какой степенью «формальности» Вы должны написать вывод.

Если, кстати, Вы работаете в рамках натуральной логики (т.е. без аксиом, только с правилами вывода), то доказывать нужно как-то по-другому. Хотя обычно это правило входит в стандартный набор как аксиоматическое утверждение.

[natalk20]

Огромное спасибо!
Поясните, пожалуйста, перенос справа налево через знак ⊢ проходит по теореме о дедукции?
Переход 8,9 - 0 это подстановка?

[Adjirranirr]

Поясните, пожалуйста, перенос справа налево через знак ⊢ проходит по теореме о дедукции?

Да.

Переходы 4-5, 6-7 и 8-0, это переходы Г₁, A ⊢ B, Г₂ ⊢ A ⇒ Г₁, Г₂ ⊢ B, на основе правила удаления импликации Г₁ ⊢ A → B, Г₂ ⊢ A ⇒ Г₁, Г₂ ⊢ B. Можно и подстановкой назвать, суть не изменится.

[natalk20]

Спасибо, Adjirranirr, очень помогли.