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).

Read more about this topic:  HOL Light

Famous quotes containing the words logical and/or foundations:

    “Opera, next to Gothic architecture, is one of the strangest inventions of Western man. It could not have been foreseen by any logical process.”
    —Kenneth MacKenzie Clark, Baron of Saltwood (1903–1983)

    “The objects of a financier are, then, to secure an ample revenue; to impose it with judgment and equality; to employ it economically; and, when necessity obliges him to make use of credit, to secure its foundations in that instance, and for ever, by the clearness and candour of his proceedings, the exactness of his calculations, and the solidity of his funds.”
    —Edmund Burke (1729–1797)