Filter
Top Products
5.4. DEFINITIONS 53
Γ[x
1
, .. . ,x
n
] p[x
1
, .. . ,x
n
]
Γ[t
1
, .. . ,t
n
] p[t
1
, .. . ,t
n
]
INST
This rule expresses the fact that variables are to be interpreted as schematic,
i.e. if p is true for variables x
1
, .. . ,x
n
, then we can replace those variables by any
terms of the same type and still get something true. Note that the substitution is
also applied to all hypotheses.
Γ[α
1
, .. . ,α
n
] p[α
1
, .. . ,α
n
]
Γ[γ
1
, .. . ,γ
n
] p[γ
1
, .. . ,γ
n
]
INST TYPE
This is the same, but for substitution of type variables rather than term vari-
ables.
5.4 Definitions
All theorems in HOL are deduced using just the above rules, starting from a small
set of axioms, which we will discuss shortly. Mathematics in HOL is derived just
from these very basic axioms. However there is a special rule of definition, which
allows the addition of new constants and corresponding new axioms provided they
are purely definitional in character.
1
If t : τ is any term without free (term or type)
variables, and c : τ an unused constant, then c : τ may be added to the stock of
constants, and the axiom c = t included as a theorem.
One can also define new types and type constructors in HOL. Given any subset
of a type γ, marked out by its characteristic predicate P : γ → bool, then given a
theorem asserting that P is nonempty, one can define a new type δ (or type operator
if γ contains type variables) in bijection with this set.
✬
✫
✩
✪
✬
✫
✩
✪
✬
✫
✩
✪
new
type
δ
existing
type
γ
✛
bijections
✲
P
Both these definitional principles give a way of producing new mathematical
theories without compromising soundness: one can easily prove that these principles
are consistency-preserving. Effectively, constant definitions could be avoided simply
by writing the definitional expansion out in full, while type definitions could be
avoided by incorporating appropriate set constraints into theorems: rather than
saying ∀x : δ. . . . one could say ∀y : γ. P (y) ⇒ .. ., with the appropriate isomorphic
mappings.
2
1
From a logical point of view, we may say that HOL is actually an evolving sequence of logical
systems, each a conservative extension of previous ones.
2
In general, the logical core of HOL is reasonably intuitionistic, with classical principles intro-
duced later as axioms. However the above definitional principle jars slightly with this since one of
the type bijections is a total function γ → δ. This is at least weakly nonconstructive, allowing us
for example to pass from p ⇒ ∃x. q[x] to ∃x. p ⇒ q[x].