• English only

# Differences

This shows you the differences between two versions of the page.

sav08:axioms_of_hol [2008/05/28 03:06]
vkuncak
sav08:axioms_of_hol [2015/04/21 17:30] (current)
Line 1: Line 1:
-====== Axioms of Classical HOL ======+====== Axioms ​and Inference Rules of Classical HOL ======

Axiom system that is sound (but necessarily incomplete with respect to standard semantics) is the following: Axiom system that is sound (but necessarily incomplete with respect to standard semantics) is the following:
Line 8: Line 8:

Inference rule: Inference rule:
-$+\begin{equation*} ​\frac{C\ \ ; \ \ A=B} ​\frac{C\ \ ; \ \ A=B} {C[A:=B]} {C[A:=B]} -$+\end{equation*}
which replaces one occurrence of $A$ in $C$ with $B$ (we cannot replace variables under $\lambda$) which replaces one occurrence of $A$ in $C$ with $B$ (we cannot replace variables under $\lambda$)