Definition 1.2.4.  Let b ∈ Bool. We define
b is true
by:
[p] is true  :⇔  p  (p is a proposition)  ⇔  b = ⊤  ⇔  b ≠ ⊥
b is false  :⇔  b is not true
Equivalence.
  • Assume p if b = [p] (p is a proposition). Then b = ⊤:
    Let q be a proposition such that b = [q] and q. Then:
    b = [q] = ⊤:
    We show that [q] = ⊤:
    q.
  • Assume b = ⊤. Then b ≠ ⊥:
    Assume b = ⊥.
    ⇒b = ⊤ ⊤ = ⊥⇒def [true  ⇔  false] ↯
  • Assume b ≠ ⊥.
    Let q be a proposition such that b = [q]. Then q:
    b ≠ ⊥ ⇒b = [q] [q] ≠ ⊥ ⇒def q
References.