Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:intuition_for_hol [2008/05/27 23:54] vkuncak |
sav08:intuition_for_hol [2009/03/05 12:56] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Intuition for Higher-Order Logic ====== | + | ====== Intuition for 'Higher-Order' Logic ====== |
| - | In first, order logic, formulas contain | + | In [[sav09:exercises 01|first-order logic]] formulas contain |
| * variables | * variables | ||
| * function symbols | * function symbols | ||
| Line 55: | Line 55: | ||
| In multisorted logic with equality, we can introduce one binary equality symbol ${=}_\tau$ for each sort $\tau$, whose signature is $\tau \times \tau$. | In multisorted logic with equality, we can introduce one binary equality symbol ${=}_\tau$ for each sort $\tau$, whose signature is $\tau \times \tau$. | ||
| - | In HOL we generalize the type system to have function types. This idea build on simply typed lambda calculus. | + | In HOL we generalize the type system to have function types, and we use functions with different types to represent functions and predicates, allowing quantification over variables of arbitrary types. This starting point for such system is simply typed lambda calculus. |