# Differences

This shows you the differences between two versions of the page.

 sav08:substitutions_for_first-order_logic [2008/03/19 16:04]vkuncak sav08:substitutions_for_first-order_logic [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/03/19 22:31 damien 2008/03/19 16:04 vkuncak 2008/03/19 15:59 vkuncak 2008/03/19 10:39 vkuncak 2008/03/19 10:31 vkuncak 2008/03/19 10:30 vkuncak 2008/03/19 10:27 vkuncak 2008/03/19 08:39 vkuncak 2008/03/19 00:12 vkuncak 2008/03/19 00:11 vkuncak 2008/03/19 00:07 vkuncak 2008/03/18 23:44 vkuncak 2008/03/18 23:30 vkuncak 2008/03/18 18:41 vkuncak 2008/03/18 18:36 vkuncak created Next revision Previous revision 2008/03/19 22:31 damien 2008/03/19 16:04 vkuncak 2008/03/19 15:59 vkuncak 2008/03/19 10:39 vkuncak 2008/03/19 10:31 vkuncak 2008/03/19 10:30 vkuncak 2008/03/19 10:27 vkuncak 2008/03/19 08:39 vkuncak 2008/03/19 00:12 vkuncak 2008/03/19 00:11 vkuncak 2008/03/19 00:07 vkuncak 2008/03/18 23:44 vkuncak 2008/03/18 23:30 vkuncak 2008/03/18 18:41 vkuncak 2008/03/18 18:36 vkuncak created Line 6: Line 6: It is important to be precise about substitutions in first-order logic. ​ For example, we would like to derive from formula $\forall x.F(x)$ formula $F(t)$, denoted $subst(\{x \mapsto t\})(F)$ that results from substituting a term $t$ instead of $x$.  For example, from $\forall x. x < x + 5$ we would like to derive $y - 1 < (y - 1) + 5$.  Consider, however formula It is important to be precise about substitutions in first-order logic. ​ For example, we would like to derive from formula $\forall x.F(x)$ formula $F(t)$, denoted $subst(\{x \mapsto t\})(F)$ that results from substituting a term $t$ instead of $x$.  For example, from $\forall x. x < x + 5$ we would like to derive $y - 1 < (y - 1) + 5$.  Consider, however formula - $+ \begin{equation*} \forall x. \exists y. x < y \forall x. \exists y. x < y -$ + \end{equation*} Consider an interpretation in integers. ​ This formula is true in this domain. ​ Now substitute instead of x the term y+1.  We obtain Consider an interpretation in integers. ​ This formula is true in this domain. ​ Now substitute instead of x the term y+1.  We obtain - $+ \begin{equation*} \exists y. y + 1 < y \exists y. y + 1 < y -$ + \end{equation*} This formula is false. ​ We say that the variable $y$ in term $y+1$ was captured during substitution. ​ When doing substitution in first-order logic we must avoid variable capture. ​ One way to do this is to rename bound variables. ​ Suppose we want to instantiate the formula ​ \$\forall x. \exists y. x