HOL Light

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

${\displaystyle {\cfrac {\qquad }{\vdash t=t}}}$	REFL	reflexivity of equality
${\displaystyle {\cfrac {\Gamma \vdash s=t\qquad \Delta \vdash t=u}{\Gamma \cup \Delta \vdash s=u}}}$	TRANS	transitivity of equality
${\displaystyle {\cfrac {\Gamma \vdash f=g\qquad \Delta \vdash x=y}{\Gamma \cup \Delta \vdash f(x)=g(y)}}}$	MK_COMB	congruence of equality
${\displaystyle {\cfrac {\Gamma \vdash s=t}{\Gamma \vdash (\lambda x.s)=(\lambda x.t)}}}$	ABS	abstraction of equality (${\displaystyle x}$ must not be free in ${\displaystyle \Gamma }$)
${\displaystyle {\cfrac {\qquad }{\vdash (\lambda x.t)x=t}}}$	BETA	connection of abstraction and function application
${\displaystyle {\cfrac {\qquad }{\{p\}\vdash p}}}$	ASSUME	assuming ${\displaystyle p}$, prove ${\displaystyle p}$
${\displaystyle {\cfrac {\Gamma \vdash p=q\qquad \Delta \vdash p}{\Gamma \cup \Delta \vdash q}}}$	EQ_MP	relation of equality and deduction
${\displaystyle {\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
${\displaystyle {\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 ,t_{n}]}}}$	INST	instantiate variables in assumptions and conclusion of theorem
${\displaystyle {\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).

• Lambek, J; Scott, P. J. (1986), Introduction to Higher Order Categorical logic, Cambridge University Press, ISBN 9780521356534

• Freek Wiedijk (December 2008), "Formal Proof — Getting Started" (PDF), Notices of the American Mathematical Society, 55 (11): 1408–1414, retrieved 2008-12-14

• HOL Light