HOL Light

HOL Light is a particularly simple version of Higher Order Logic that only takes equality as the primitive notion of the logical fragment.

Rules

The following are a rationalized set of rules for the logical fragment of HOL light.

Γ∣Ψ⊢t=tabsentprovesconditionalΓΨ𝑡𝑡\displaystyle\frac{}{\Gamma\mid\Psi\vdash t=t}
Γ∣Ψ⊢s=tΓ∣Ψ⊢t=uΓ∣Ψ⊢s=uprovesconditionalΓΨ𝑠𝑡conditionalΓΨproves𝑡𝑢provesconditionalΓΨ𝑠𝑢\displaystyle\frac{\Gamma\mid\Psi\vdash s=t\qquad\Gamma\mid\Psi\vdash t=u}{% \Gamma\mid\Psi\vdash s=u}
Γ∣Ψ⊢f=gΓ∣Ψ⊢x=yΓ∣Ψ⊢f⁢(x)=g⁢(y)provesconditionalΓΨ𝑓𝑔conditionalΓΨproves𝑥𝑦provesconditionalΓΨ𝑓𝑥𝑔𝑦\displaystyle\frac{\Gamma\mid\Psi\vdash f=g\qquad\Gamma\mid\Psi\vdash x=y}{% \Gamma\mid\Psi\vdash f(x)=g(y)}
Γ,x∣Ψ⊢s=tΓ∣Ψ⊢(λx.s)=(λx.t)\displaystyle\frac{\Gamma,x\mid\Psi\vdash s=t}{\Gamma\mid\Psi\vdash(\lambda x.% s)=(\lambda x.t)}
Γ∣Ψ⊢(λx.t1)t2=t1[t2/x]\displaystyle\frac{}{\Gamma\mid\Psi\vdash(\lambda x.t_{1})t_{2}=t_{1}[t_{2}/x]}
p∈ΨΓ∣Ψ⊢p𝑝ΨprovesconditionalΓΨ𝑝\displaystyle\frac{p\in\Psi}{\Gamma\mid\Psi\vdash p}
Γ∣Ψ⊢p=qΓ∣Ψ⊢pΓ∣Ψ⊢qprovesconditionalΓΨ𝑝𝑞conditionalΓΨproves𝑝provesconditionalΓΨ𝑞\displaystyle\frac{\Gamma\mid\Psi\vdash p=q\qquad\Gamma\mid\Psi\vdash p}{% \Gamma\mid\Psi\vdash q}
Γ∣Ψ,p⊢qΓ∣Ψ,q⊢pΓ∣Ψ⊢p=qprovesconditionalΓΨ𝑝𝑞conditionalΓΨ𝑞proves𝑝provesconditionalΓΨ𝑝𝑞\displaystyle\frac{\Gamma\mid\Psi,p\vdash q\qquad\Gamma\mid\Psi,q\vdash p}{% \Gamma\mid\Psi\vdash p=q}

Note that HOL light also has a pair of instantiation rules used to substitute for type and term variables, but these are just Substitution rules, so we omit them.