6 Prove each of the following laws of Binary Theory using the proof format given in Subsection 1.0.1, and any laws listed in Section 11.4. Do not use the Completion Rule.
(a) §
(b) §
(c) §
(d) §
(e) §
(f) §
(g) §
(h) §
a∧b ⇒ a∨b
a∧b specialization
⇒ a generalization
⇒ a∨b
(a∧b) ∨ (b∧c) ∨ (a∧c) = (a∨b) ∧ (b∨c) ∧ (a∨c)
(a∧b) ∨ (b∧c) ∨ (a∧c) distribute
= (a∨b∨a)∧(a∨b∨c)∧(a∨c∨a)∧(a∨c∨c)∧(b∨b∨a)∧(b∨b∨c)∧(b∨c∨a)∧(b∨c∨c)
= (a∨b) ∧ (a∨b∨c) ∧ (a∨c)
= (a∨b) ∧ (b∨c) ∧ (a∨c)
¬a⇒(a⇒b)
¬a⇒(a⇒b)
= ¬a∧a⇒b
∧ (b∨c)
symmetry and idempotence absorption
portation noncontradiction base
symmetry of = associativity of = symmetry of = and ∨ inclusion
symmetry of = associativity of = symmetry of = inclusion
law of conflation contrapositive law antecedent is law of noncontradiction identity for ⇒
specialization generalization
portation conflation
= ⊥⇒b =⊤
a = (b ⇒ a)
(a = (b ⇒ a)
= ((b ⇒ a) = a
= ((b ⇒ a) =
= ((b ⇒ a) = =⊤
= a ∧ b = a ∧ b)
= ((a⇒b) = a = a ∧ b)
= ((a⇒b) = a = (a ∧ b))
= ((a⇒b) = (a ∧ b) = a) =⊤
= a ∨ b = a ∨ b) = a ∨ b)
a = (a ∨ b)) (b ∨ a) = a)
a = (a ⇒ b)
(a = (a ⇒ b)
(a⇒c) ∧ (b⇒¬c) ⇒ ¬(a∧b)
(a⇒c) ∧ (b⇒¬c) ⇒ a∧b ⇒ c∧¬c
= ¬(c∧¬c) ⇒ ¬(a∧b)
= ⊤ ⇒ ¬(a∧b)
= ¬(a∧b)
a∧¬b⇒a∨b
a ∧ ¬b
⇒ a
⇒ a∨b
(a⇒b) ∧ (c⇒d) ∧ (a∨c) ⇒ (b∨d)
(a⇒b) ∧ (c⇒d) ∧ (a∨c) ⇒ (b∨d)
= (a⇒b) ∧ (c⇒d) ⇒ (a∨c ⇒ b∨d) =⊤
(i) §
(j) §
(k)√
(l) §
a ∧ ¬a ⇒ b
a ∧ ¬a ⇒ b = ⊥⇒b
=⊤
(a⇒b) ∨ (b⇒a)
(a⇒b) ∨ (b⇒a)
= ¬a ∨ b ∨ ¬b ∨ a
= a ∨ ¬a ∨ b ∨ ¬b
= ⊤ ∨ ⊤ =⊤
¬(a ∧ ¬(a∨b))
(¬a⇒¬b) ∧ (a⧧b) ∨ (a∧c ⇒ b∧c)
(¬a⇒¬b) ∧ (a⧧b) ∨ (a∧c ⇒ b∧c)
= (¬a⇒¬b) ∧ (a=¬b) ∨ (a∧c ⇒ b∧c)
= (¬a⇒a) ∧ (a=¬b) ∨ (a∧c ⇒ b∧c)
= a ∧ (a=¬b) ∨ (a∧c ⇒ b∧c)
= a ∧ ¬b ∨ (a∧c ⇒ b∧c)
= ¬(¬a ∨ b) ∨ (a∧c ⇒ b∧c)
= ¬(a⇒b) ∨ (a∧c ⇒ b∧c)
assume a⇒b to simplify the right disjunct; strengthen b to a
noncontradiction base
inclusion, twice symmetry of ∨ excluded middle, twice idempotence of ∨ , or base law
law of exclusion use a=¬b to replace ¬b with a indirect proof context to replace second a by ⊤ , and identity duality and double negation inclusion
(m) §
(n) §
⇐ ¬(a⇒b) ∨ (a∧c ⇒ a∧c) =⊤
Alternative proof:
(¬a⇒¬b) ∧ (a b) ∨ (a∧c ⇒ b∧c) ⇐ (b⇒a) ∧ (a b) ∨ (a⇒b)
= ((b⇒a) ∨ (a⇒b)) ∧ ((a⧧b) ∨ (a⇒b))
= (¬b ∨ a ∨ ¬a ∨ b) ∧ ((a⧧b) ∨ (a⇒b))
= (a ∨ ¬a ∨ b ∨ ¬b) ∧ ((a⧧b) ∨ (a⇒b))
= (a⧧b) ∨ (a⇒b)
= ¬(a=b) ∨ (a⇒b)
= (a=b) ⇒ (a⇒b)
= (a⇒b)∧(b⇒a) ⇒ (a⇒b) =⊤
(a⇒¬a) ⇒ ¬a
(a⇒¬a) ⇒ ¬a
= (¬a ∨ ¬a) ⇒ ¬a
= ¬a ⇒ ¬a =⊤
(a⇒b) ∧ (¬a⇒b) = b
(a⇒b) ∧ (¬a⇒b)
= a∨¬a ⇒ b
= ⊤ ⇒ b =b
OR (a⇒b) ∧ (¬a⇒b) = if a then b else b fi =b
reflexivity and base
contrapositive, monotonicity distributivity material implication twice symmetry and associativity excluded middle twice, base or idempotent generic unequality material implication antisymmetry (double implication) specialization
material implication idempotent reflexive
antidistributive law antecedent is law of excluded middle identity for ⇒
case analysis generic case idempotent
(o) §
(a⇒b)⇒a = a (a⇒b)⇒a (⊥⇒b)⇒a
⊤ ⇒ a
use main consequent to simplify antecedent base identity
=
=
=a
or (a⇒b)⇒a inclusion
= (¬a ∨ b) ⇒ a
= ¬(¬a ∨ b) ∨ a
= (¬¬a ∧ ¬b) ∨ a
= (a ∧ ¬b) ∨ a
= a ∨ (a ∧ ¬b) =a
inclusion duality double negation symmetry of ∨ absorption
identity and reflexive laws for = symmetry and associative laws for = main ∨ distributes over =
(p) §
= = =
a=b∨a=c∨b=c
a=b ∨ a=c ∨ b=c
a=b ∨ a=c ∨ b=((a=a)=c)
(a=b ∨ a=c) ∨ (a=b)=(a=c)
(a=b ∨ a=c ∨ a=b) = (a=b ∨ a=c ∨ a=c)
=
=⊤
Here’s another solution.
symmetry, associativity, and idempotence of ∨ twice = is reflexive
(q) §
(r) §
(s) §
=
= =⊤
=
=
= =⊤
= =⊤
(a=b ∨ a=c) = (a=b ∨ a=c)
a=b ∨ a=c ∨ b=c
= ¬¬(a=b) ∨ a=c ∨ b=c
= ¬(a=b) ⇒ a=c ∨ b=c
= a⧧b ⇒ a=c ∨ b=c
= a=¬b ⇒ a=c ∨ b=c
= a=¬b ⇒ ¬b=c ∨ b=c
= a=¬b ⇒ b⧧c ∨ b=c
= a=¬b ⇒ ¬(b=c) ∨ b=c
= a=¬b ⇒ ⊤
=⊤
a∧b∨a∧¬b =a a∧b ∨ a∧¬b = a a∧(b ∨ ¬b) = a a∧⊤ = a
⊤∧a = a
double negation material implication unequality exclusion context: assume antecedent exclusion unequality symmetry, excluded middle base
factor excluded middle symmetry identity
portation specialization
a⇒(b⇒a) a⇒(b⇒a) a∧b ⇒ a
a⇒a∧b = a⇒b = a∨b⇒b (a⇒a∧b = a⇒b = a∨b⇒b)
distribute ⇒ over ∧ in first part; antidistribute ⇒ over ∨ in last part ((a⇒a)∧(a⇒b) = a⇒b = (a⇒b)∧(b⇒b))
reflexivity of ⇒ and identity of ∧ ((a ⇒ b) = a ⇒ b = (a ⇒ b)) reflexivity of =
(t) §
(u) §
= = = = =
(a ⇒ a∧b) ∨ (b ⇒ a∧b) (a ⇒ a∧b) ∨ (b ⇒ a∧b) a∧b ⇒ a∧b
anti-distributive reflexive
case idempotent law context
case analysis
= =⊤
(a⇒(p=x)) ∧ (¬a⇒p) = p=(x∨¬a) p=(x∨¬a)
if a then p=(x∨¬a) else p=(x∨¬a) fi if a then p=(x∨¬⊤) else p=(x∨¬⊥) fi if a then p=(x∨⊥) else p=(x∨⊤) fi
if a then p=x else p fi (a⇒(p=x)) ∧ (¬a⇒p)