Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:substitutions_for_first-order_logic [2008/03/19 10:39] vkuncak |
sav08:substitutions_for_first-order_logic [2008/03/19 15:59] vkuncak |
||
---|---|---|---|
Line 25: | Line 25: | ||
We define naive substitution recursively, first for terms: | We define naive substitution recursively, first for terms: | ||
- | $subst(\sigma)( x ) = \sigma( x ),\ \sigma {\rm defined at } x $ | + | $ subst(\sigma)( x ) = \sigma( x ),\ \sigma {\rm defined at } x $ |
- | $subst(\sigma)( x ) = x,\ \sigma {\rm not defined at } x $ | + | $ subst(\sigma)( x ) = x,\ \sigma {\rm not defined at } x $ |
$subst(\sigma)(f(t_1,\ldots,t_n)) = f(subst(\sigma)(t_1),\ldots,subst(\sigma)(t_n))$ | $subst(\sigma)(f(t_1,\ldots,t_n)) = f(subst(\sigma)(t_1),\ldots,subst(\sigma)(t_n))$ |