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:

    “Philosophy aims at the logical clarification of thoughts. Philosophy is not a body of doctrine but an activity. A philosophical work consists essentially of elucidations.”
    —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)