Disjunction

Exercises

Video examples

• Weak distributivity of ∧ over ∨: A, B, C; A && (B || C) |- A && B || C

Easy

• Left introduction: A, B; A |- A || B
• Right introduction: A, B; B |- A || B
• Elimination: A, B, C; A || B, A -> C, B -> C |- C

Medium

• Distributivity of ⇒ over ∨: A, B, C; (A -> B) || (A -> C) |- A -> B || C
• Weak distributivity of ∨ over ⇒: A, B, C; (A -> B) || C |- A -> (B || C)

Advanced

• Associativity: A, B, C; |- (A || (B || C)) <-> ((A || B) || C)
• Antidistributivity of ⇒ over ∨: A, B, C; |- (A || B -> C) <-> ((A -> C) && (B -> C))
• Distributivity of ∨ over ∧: A, B, C; |- (A || B && C) <-> ((A || B) && (A || C))