Почему нам нужно доказать оба предложения, чтобы применить устранение дизъюнкции в Изабель?

Question

Я видел правило доказательства для устранения дизъюнкции и заметил, что мы должны доказать ОБА утверждения, чтобы использовать его:

?P ∨ ?Q ⟹ (?P ⟹ ?R) ⟹ (?Q ⟹ ?R) ⟹ ?R

почему это так? Как и в обычной логике c, если бы я знал, что ОДНА правда, тогда я знал бы, что все это правда, так кого волнует, какова истинная ценность другой. Точно так же, если я могу хотя бы один раз доказать, почему я не могу устранить дизъюнкцию / или?

Для контекста я пытался доказать:

proof (prove)
goal (1 subgoal):
 1. ∀s. P s ∨ Q s ⟹ ∀s. P s ⟶ R s ⟹ ∀s. Q s ⟶ R s ⟹ ∀s. R 

, но в итоге я застрял в циклах и я не знаю почему:

 apply (rule allI)
  apply (rule_tac P="λs. P s ∨ Q s" in allE)
   apply assumption
  apply (erule_tac P="λs. P s ⟶ R s" in allE)
  apply (erule_tac P="λs. Q s ⟶ R s" in allE)
  apply (erule impE)
   defer
   apply assumption
  apply auto
  apply (erule allE)
  apply (erule disjE)

доказательство кажется очевидным, но не может заставить Изабель подчиниться ...

Answer 1

Правило, которое вы хотите применить, а именно устранение дизъюнкции (disjE), позволяет устранить дизъюнкцию P ∨ Q в помещениях, не зная априори P или Q верно. В этой ситуации вам необходимо рассмотреть оба случая отдельно (т.е. предположить, что P - это истина, и предположить, что Q - это истина), чтобы безопасно устранить дизъюнкцию. Точнее, если вы можете доказать заключение R в обоих случаях, тогда вы можете устранить дизъюнкцию P ∨ Q и сделать вывод R. Когда вы говорите: «Если бы я знал, что ОДНА правда, тогда я знал бы, что все это правда, поэтому кого волнует, какова истина другой стороны», я думаю, что вы на самом деле имеете в виду дизъюнкцию введение (disjI1 и disjI2 соответственно ?P ⟹ ?P ∨ ?Q и ?Q ⟹ ?P ∨ ?Q).

Answer 2

Использование auto в середине написанного от руки подробного доказательства применения очень странно. Ваша проблема в том, что вы применили disjE слишком поздно: вам нужно применять его до impE, а не после (это проблема -> vs ==>: с impE вы делаете выбор P).

lemma ‹∀s. P s ∨ Q s ⟹ ∀s. P s ⟶ R s ⟹ ∀s. Q s ⟶ R s ⟹ ∀s. R s›
 apply (rule allI)
  apply (rule_tac P="λs. P s ∨ Q s" in allE)
   apply assumption
  apply (erule_tac P="λs. P s ⟶ R s" in allE)
  apply (erule_tac P="λs. Q s ⟶ R s" in allE)
  apply (erule disjE) 
  apply (erule impE)
    apply assumption+ 
  apply (rotate_tac 2)
  apply (erule impE)
    apply assumption+
  done

Вот еще одно рабочее доказательство, которое ближе к тому, что вы хотите на бумаге:

lemma ‹∀s. P s ∨ Q s ⟹ ∀s. P s ⟶ R s ⟹ ∀s. Q s ⟶ R s ⟹ ∀s. R s›
  apply (rule allI)
  apply (drule_tac x=s in spec)
  apply (elim disjE)
  apply (drule_tac x=s in spec)
   apply (erule impE)
    apply assumption+
  apply (rotate_tac)
  apply (drule_tac x=s in spec)
   apply (erule impE)
    apply assumption+
  done

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

Answer 3

Я думаю, что объяснение правил OrE и AndE и сравнение их является продуктивным. Давайте начнем с Or (дизъюнкция):

Устранение дизъюнкции

Напомним правило: disjE = OrE: ⟦ P ∨ Q; P ⟹ R; Q ⟹ R ⟧ ⟹ R. Чтобы объяснить это, рассмотрим следующую историю:

Вы знаете P или Q, но не знаете, какая именно. Предположим, это утверждение означает, что под этой чашкой P или чашкой Q стоит купюра в 10 долларов. Если вы хотите заключить R, используя этот факт (например, R = Купить обед), то вы должны убедиться, что вы действительно получите счет в 10 долларов. Поскольку вы НЕ знаете, какой из них имеет счет в 10 долларов, вам нужно создать инструмент (то есть), который поднимает ОБА чашки, чтобы гарантировать, что вы получите счет в 10 долларов. Таким образом, чтобы использовать этот факт в своем доказательстве, вам нужно построить доказательство как для P => R, так и для Q => R, потому что вы не знаете, какое из них истинно.

Теперь давайте сравним его с устранением конъюнкции / AndE.

Устранение конъюнкции

Напомним различные способы express Правило:

• AndEL [|P /\ Q; P=>R |] => R
• AndER [|P/\ Q; Q=>R|] => R
• conjE: ⟦ P ∧ Q; ⟦ P; Q ⟧ ⟹ R ⟧ ⟹ R

Для объяснения рассмотрим следующую историю:

Аналогия с 10-долларовым счетом. Если у нас есть P / \ Q, то мы знаем, что под P cup И Q the cup находится купюра в 10 долларов. Таким образом, нам нужен только инструмент (то есть доказательство), чтобы поднять один, чтобы прийти к R (скажем, купить обед). Таким образом, для этого правила, поскольку мы знаем, что ОБА имеют 10-долларовые банкноты, нам нужно только построить инструмент (доказательство), чтобы поднять 1 из чашек. Следовательно, именно поэтому нам нужно иметь только одно из утверждений для правила And E. На самом деле Изабель сжимает правило и говорит: «Если вы поднимаете любую чашку (то есть ⟦P; Q⟧, что означает, что вы можете использовать любое предположение), тогда вы можете заключить R».

примечание: обратите внимание, что ⟦ P; Q ⟧ ⟹ R фактически означает просто наличие одного из предположений P или Q для заключения R. Таким образом, это сжатый способ объединить оба AndE в один (потому что вы можете использовать любое из допущений для заключения R).

Бонус: allE & exE

allE

• всеЕ [| ∀x. ? P x; (? P? X ⟹? R) |] ⟹? R
  • это неограниченное «соединение» / AND. В основном, чтобы удалить данные, нам нужен только один конкретный пример c (точно так же, как мы исключаем конкретный c AND).
  • [| ∀x. ? P x; (? P? X ⟹? R) |] ⟹? R
    • Специфический c x, который нам нужен для «удаления неограниченного И», равен? X.

exE

• exE [| ∃x.? P x; (⋀x.? P x ⟹? Q) |] ⟹? Q
  • это неограниченное «соединение» / ИЛИ. В основном, чтобы удалить, нам нужно было бы доказать это для всех случаев. Таким образом, причина, по которой мы используем метафорал с мета-абстракцией / \ (и, конечно, fre sh экземпляр переменной!) Потому что он должен храниться для всех из них независимо от того, что является заданным термином c (пока мы не ссылаемся на термин уже).
  • [| ∃x .? P x; (⋀x.? P x ⟹? Q) |] ⟹? Q
    • Введенная переменная fre sh - это ⋀x для удаления неограниченного ИЛИ.