HOL Light - Logical Foundations

Logical Foundations

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:

	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 ( must not be free in )
$\cfrac{\qquad}{\vdash (\lambda x. t) x = t}$	BETA	connection of abstraction and function application
$\cfrac{\qquad }{ \{p\} \vdash p}$	ASSUME	assuming, prove
$\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 \vdash p} {\Gamma \vdash p}$	INST	instantiate variables in assumptions and conclusion of theorem
$\cfrac{\Gamma \vdash p} {\Gamma \vdash p}$	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).

Famous quotes containing the words logical and/or foundations:

“A picture whose pictorial form is logical form is called a logical picture.”
—Ludwig Wittgenstein (1889–1951)

“Honorable Senators: My sincerest thanks I offer you. Conserve the firm foundations of our institutions. Do your work with the spirit of a soldier in the public service. Be loyal to the Commonwealth and to yourselves and be brief; above all be brief.”
—Calvin Coolidge (1872–1933)