Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:intuition_for_hol [2008/05/27 23:44] vkuncak created |
sav08:intuition_for_hol [2009/03/05 12:54] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Intuition for Higher-Order Logic ====== | + | ====== Intuition for 'Higher-Order' Logic ====== |
| - | In first, order logic, formulas contain | + | In [[exercise01|first-order logic]] formulas contain |
| * variables | * variables | ||
| * function symbols | * function symbols | ||
| Line 20: | Line 20: | ||
| \forall R. \forall f. \forall x. \lnot R(x,f(x)) | \forall R. \forall f. \forall x. \lnot R(x,f(x)) | ||
| \] | \] | ||
| - | The last two formulas cannot be written in FOL, because they involve quantification over functions and relations. However, these formulas can be written in HOL. Moreover, in HOL we can write more complex conditions that cannot be described directly in terms of validity or satisfiability, such as | + | The last two formulas cannot be written in FOL, because they involve quantification over functions and relations. However, these formulas can be written in HOL. Moreover, in HOL we can write more complex conditions that cannot be described directly in terms of validity or satisfiability of FOL formulas, such as |
| \[ | \[ | ||
| \forall R. \exists f. \forall x. \lnot R(x,f(x)) | \forall R. \exists f. \forall x. \lnot R(x,f(x)) | ||
| Line 46: | Line 46: | ||
| D_{\tau_1} \times \ldots \times D_{\tau_n} | D_{\tau_1} \times \ldots \times D_{\tau_n} | ||
| \] | \] | ||
| + | In multisorted FOL, we have disjoint countable sets of variables for each sort. We interpreted $\forall x_\tau F(x)$ as bounded quantification $\forall d \in D_\tau. F(d)$. | ||
| + | |||
| + | **Relation to standard FOL:** | ||
| + | Multisorted FOL can be represented as the standard FOL by using unary predicate $P_\tau$ for each sort $\tau$, adding axioms that these predicate interpretations are disjoint, and replacing quantification such as $\forall x_\tau. F(x)$ with bounded quantification | ||
| + | \[ | ||
| + | \forall x. P_\tau(x) \rightarrow F(x) | ||
| + | \] | ||
| + | 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, 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. | ||