Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next 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 16:04] vkuncak |
||
|---|---|---|---|
| Line 24: | Line 24: | ||
| We define naive substitution recursively, first for terms: | We define naive substitution recursively, first for terms: | ||
| - | + | \[\begin{array}{rcl} | |
| - | $subst(\sigma)( x ) = \sigma( x ),\ \sigma {\rm defined at } x $ | + | subst(\sigma)( x ) &=& \sigma( x ),\ \sigma \mbox{ d{}efined at } x \\ |
| - | + | subst(\sigma)( x ) &=& x,\ \sigma \mbox{ not d{}efined 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)) |
| - | + | \end{array}\] | |
| - | $subst(\sigma)(f(t_1,\ldots,t_n)) = f(subst(\sigma)(t_1),\ldots,subst(\sigma)(t_n))$ | + | |
| and then for formulas: | and then for formulas: | ||