Filter
Top Products
54 CHAPTER 5. PRIMITIVE BASIS OF HOL LIGHT
5.5 Derived rules
HOL’s logic is then built up by including constants for the usual logical operations.
An attractive feature is that these do not need to be postulated: it has been known
since Henkin (1963) how to define all logical constants in terms of equality, at least
from a classical point of view. We do things in an ‘intuitionistic’ manner, giving
useful deductive rules before we later assert the Law of the Excluded Middle, i.e.
that every Boolean term is either true or false. While it is more typical (Prawitz
1965) to take a few additional logical constants such as ∀ and ⇒ as primitive, our
approach is very similar to the usual definitions of the internal logic of a topos; see
e.g. Lambek and Scott (1986).
We will now show how all the logical constants are defined. These are (true),
∧ (and), ⇒ (implies), ∀ (for all), ∃ (there exists), ∨ (or), ⊥ (false) ¬ (not) and ∃!
(there exists a unique). Recall that what we write as ∀x.P[x] is a syntactic sugaring
of ∀(λx. P[x]). Using this technique, quantifiers and the Hilbert ε operator can be
used as if they bound variables, but with all binding implemented in terms of λ-
calculus. There are several examples in this book.
= (λx. x) = (λx. x)
∧ = λp. λq. (λf. f p q) = (λf. f )
⇒ = λp. λq. p ∧ q = p
∀ = λP. P = λx.
∃ = λP. ∀Q. (∀x. P(x) ⇒ Q) ⇒ Q
∨ = λp. λq. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊥ = ∀P. P
¬ = λt. t ⇒ ⊥
∃! = λP. ∃P ∧ ∀x. ∀y. P x ∧ P y ⇒ (x = y)
While these might look puzzling at first sight, a little thought will convince
the reader that they express what is intended. For example ∀x. P[x], or without
sugaring ∀(λx. P[x]), says that for any a, P[a], or equivalently (λx. P[x]) a, is true.
This is exactly the same as saying that λx. P[x] is a constant function that always
returns (true), which is how ∀ is defined.
From the above definitions and the primitive rules, it is then possible to define
derived inference rules that give convenient ways of manipulating logical formulas
without explicitly taking everything back to the definitions. Because HOL is a
programmable system in the LCF style, these can all be encapsulated as CAML
functions that look to the user the same as primitive rules.
5.6 Classical axioms
That concludes the logic proper, and in fact quite a bit of interesting mathematics,
e.g. infinitary inductive definitions, can be developed just from that basis (Harrison
1995). But for general use we adopt three more axioms.
• First, there is an axiom of extensionality, which we encode as an η-conversion
theorem: (λx. t x) = t.
• Secondly, we introduce one new primitive logical constant ε, of polymorphic
type (α → bool) → α, the so-called Hilbert choice operator. It is accompanied
by a new axiom giving the basic property of ε, namely that it picks out
something satisfying P whenever there is something to pick: