Filter
Top Products
52 CHAPTER 5. PRIMITIVE BASIS OF HOL LIGHT
5.3 Primitive inference rules
The HOL formal system allows the deduction of arbitrary sequents of the form
φ
1
, .. . ,φ
n
ψ (read as ‘if φ
1
and .. .and φ
n
then ψ’) where the terms involved
have type bool. (Where there are no assumptions it is customary to write just ψ.)
There are no additional logical constants involved in the basic deductive system.
The derivable sequents are those that can be generated by the following inference
rules. Each rule is written with the conclusion below a line and the hypotheses
above, and with the standard name for the inference rule, corresponding in fact to
a CAML identifier in HOL, at the right.
t = t
REFL
This rule says that equality is reflexive.
Γ s = t ∆ t = u
Γ ∪ ∆ s = u
TRANS
This rule says that equality is transitive. It is of course necessary to include in
the conclusion theorem any assumption that may have played a role in deducing
the top two theorems.
Γ s = t ∆ u = v
Γ ∪ ∆ s(u) = t(v)
MK COMB
This says that equal functions applied to equal arguments give equal results.
We have assumed without comment that the types agree, e.g. s : σ → τ, t : σ → τ,
u : σ and v : σ.
Γ s = t
Γ (λx. s) = (λx. t)
ABS
This rule requires that x is not a free variable in any of the assumptions Γ. It says
that if, without using any special properties of x, we deduced that two expressions
involving x are equal, then the functions that take x to those values are equal.
(λx. t)x = t
BETA
This expresses the fact that combination and abstraction are converse opera-
tions, i.e. ‘the function that takes an argument x to t’, applied to an argument x,
gives t.
{p} p
ASSUME
This says simply that from any p we can deduce p. Of course, p must have type
bool.
Γ p = q ∆ p
Γ ∪ ∆ q
EQ MP
This connects equality with deduction, saying that if p and q are equal, and we
can deduce p, then we can deduce q (from the appropriately combined assumptions).
Γ p ∆ q
(Γ − {q}) ∪ (∆ − {p}) p = q
DEDUCT ANTISYM RULE
This rule also connects equality and deduction, effectively saying that equality
on the boolean type represents logical equivalence. Ignoring extra hypotheses for
a moment, it says that if we can deduce p from q and q from p, then p and q are
equal, under the accumulated assumptions.