Формальное доказательство пропозициональной логики

Я пытаюсь формально доказать следующее уравнение в качестве практики перед экзаменом по логике. Однако у меня возникли небольшие трудности с выполнением шагов. Вот правила, которые я использую;

A ∧ A ≡ A, A ∨ A ≡ A idempotence
A ∧ B ≡ B ∧ A, A ∨ B ≡ B ∨ A commutativity
A ∧ (B ∧ C ) ≡ (A ∧ B) ∧ C , A ∨ (B ∨ C ) ≡ (A ∨ B) ∨ C associativity
A ∧ (A ∨ B) ≡ A, A ∨ (A ∧ B) ≡ A absorption
A ∧ (B ∨ C ) ≡ (A ∧ B) ∨ (A ∧ C ) distributivity
A ∨ (B ∧ C ) ≡ (A ∨ B) ∧ (A ∨ C ) distributivity
A ∧ (¬A) ≡ false, A ∨ (¬A) ≡ true negation
¬(¬A) ≡ A double negation
¬(A ∧ B) ≡ (¬A) ∨ (¬B), ¬(A ∨ B) ≡ (¬A) ∧ (¬B) de Morgan
A ⇒ B ≡ (¬A) ∨ B implication
A ⇔ B ≡ (A ⇒ B) ∧ (B ⇒ A) bi-implication

И это уравнение;

 (p⇒r) ∧ (q⇒r) ≣ (p∨q) ⇒ r

Я полагал, что использую, Implication, Commuatability и Distributivity, но я застрял на этом этапе. Ценю любую помощь!


logic proof
person Community    schedule 15.04.2016    source источник
comment
Я голосую за то, чтобы закрыть этот вопрос как не по теме, потому что он касается логики и математики, а не программирования или разработки программного обеспечения.   -  person Pang    schedule 30.04.2016

Ответы (1)


arrow_upward
2
arrow_downward

вот формальное доказательство

(p∨q) ⇒ r ≣ ¬(p∨q) ∨ r          implication
          ≣ (¬p∧¬q) ∨ r         de Morgan
          ≣ (¬p∨r) ∧ (¬q∨r)     distributivity and commutativity
          ≣ (p⇒r) ∧ (q⇒r)       implication

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

ПОЯСНЕНИЕ

  1. Учитывая, что p ⇒ (p∨q), из (p∨q) ⇒ r, мы получаем p ⇒ (p∨q) ⇒ r и, следовательно, p ⇒ r. Поскольку тот же аргумент действителен для q, мы также получаем q ⇒ r. Итак, (p ⇒ r) ∧ (q ⇒ r).

  2. И наоборот, если (p ⇒ r) ∧ (q ⇒ r), то r должно быть истинным всякий раз, когда любое из p и q оказывается истинным. Другими словами, всякий раз, когда (p∨q) истинно. Следовательно (p∨q) ⇒ r.

person Leandro Caniglia    schedule 16.04.2016