HOL Light

HOL Light is a member of the HOL theorem prover family. Like the other members, it is a proof assistant for classical higher order logic. Compared with other HOL systems, HOL Light is intended to have relatively simple foundations.

Logical foundations

HOL Light is based on a formulation of type theory with equality as the only primitive concept. The primitive rules of inference are the following:

${\cfrac {\qquad }{\vdash t=t}}$	REFL: reflexivity of equality
${\cfrac {\Gamma \vdash s=t\qquad \Delta \vdash t=u}{\Gamma \cup \Delta \vdash s=u}}$	TRANS: transitivity of equality
${\cfrac {\Gamma \vdash f=g\qquad \Delta \vdash x=y}{\Gamma \cup \Delta \vdash f(x)=g(y)}}$	MK_COMB: congruence of equality
${\cfrac {\Gamma \vdash s=t}{\Gamma \vdash (\lambda x.s)=(\lambda x.t)}}$	ABS: abstraction of equality
${\cfrac {\qquad }{\Gamma \vdash (\lambda x.t)x=t}}$	BETA: connection of abstraction and function application
${\cfrac {\qquad }{\{p\}\vdash p}}$	ASSUME: assuming $p$, prove $p$
${\cfrac {\Gamma \vdash p=q\qquad \Delta \vdash p}{\Gamma \cup \Delta \vdash q}}$	EQ_MP: relation of equality and deduction
${\cfrac {\Gamma \vdash p\qquad \Delta \vdash q}{(\Gamma -\{q\})\cup (\Delta -\{p\})\vdash p=q}}$	DEDUCT_ANTISYM_RULE: deduce equality from 2-way deducibility
${\cfrac {\Gamma [x_{1},\ldots ,x_{n}]\vdash p[x_{1},\ldots ,x_{n}]}{\Gamma [t_{1},\ldots ,t_{n}]\vdash p[t_{1},\ldots ,p_{n}]}}$	INST: instantiate variables in assumptions and conclusion of theorem
${\cfrac {\Gamma [\alpha _{1},\ldots ,\alpha _{n}]\vdash p[\alpha _{1},\ldots ,\alpha _{n}]}{\Gamma [\tau _{1},\ldots ,\tau _{n}]\vdash p[\tau _{1},\ldots ,\tau _{n}]}}$	INST_TYPE: instantiate type variables in assumptions and conclusion of theorem

This formulation of type theory is very close to the one described in section II.2 of Lambek & Scott (1986).

References

Lambek, J (1986). Introduction to Higher Order Categorical logic. Cambridge University Press. {{cite book}}: Unknown parameter |coauthors= ignored (|author= suggested) (help)

External links

• HOL Light.