HOL Light

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

Logical foundations

HOL Light is based on a formulation of type theory with equalityas the only primitive concept. The primitive rules of inferenceare 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,t\_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\; [\; au\_1,ldots,\; au\_n]\; vdash\; p\; [\; au\_1,ldots,\; au\_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 Harvtxt|Lambek|Scott|1986.

References

cite book
last = Lambek
first = J
coauthors = P. J. Scott
title = Introduction to Higher Order Categorical logic
publisher = Cambridge University Press
date = 1986

External links

* [http://www.cl.cam.ac.uk/users/jrh/hol-light/ HOL Light] .