Skip to content

Instantly share code, notes, and snippets.

@infiniteregrets
Created October 4, 2021 23:00
Show Gist options
  • Save infiniteregrets/29cc3ef3889de168b13450703add0b00 to your computer and use it in GitHub Desktop.
Save infiniteregrets/29cc3ef3889de168b13450703add0b00 to your computer and use it in GitHub Desktop.
Proof:
p ⇒ (q ⇒ r)
≡⟨ “Material implication” ⟩
¬ p ∨ (q ⇒ r)
≡⟨ “Material implication” ⟩
¬ p ∨ (¬ q ∨ r)
≡⟨ “Distributivity of ∨ over ∨” ⟩
(¬ p ∨ ¬ q) ∨ (¬ p ∨ r)
≡⟨ “Definition of ¬ from ≡” ⟩
(¬ p ∨ (q ≡ false)) ∨ (¬ p ∨ r)
≡⟨ “Distributivity of ∨ over ≡” ⟩
((¬ p ∨ q) ≡ (¬ p ∨ false)) ∨ (¬ p ∨ r)
≡⟨ “Identity of ∨” ⟩
((¬ p ∨ q) ≡ ¬ p ) ∨ (¬ p ∨ r)
≡⟨ “Distributivity of ∨ over ≡” ⟩
(¬ p ∨ q) ∨ (¬ p ∨ r) ≡ ¬ p ∨ ¬ p ∨ r
≡⟨ “Idempotency of ∨” ⟩
(¬ p ∨ q) ∨ (¬ p ∨ r) ≡ ¬ p ∨ r
≡⟨ ? ⟩
¬ (¬ p ∨ q) ∨ (¬ p ∨ r)
≡⟨ ? ⟩
(p ⇒ q) ⇒ (p ⇒ r)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment