• 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) Both sides previous revision Previous revision 2009/03/05 13:05 vkuncak 2008/05/28 03:06 vkuncak 2008/05/28 02:44 vkuncak 2008/05/27 17:25 vkuncak created Next revision Previous revision 2009/03/05 13:05 vkuncak 2008/05/28 03:06 vkuncak 2008/05/28 02:44 vkuncak 2008/05/27 17:25 vkuncak created 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$) 