The following statement made me realize that variable binding can be defined in first-order logic:
The same holds for λ terms to define functions. There is no reason that they could not be included in first-order theories, and in fact they sometimes are, but most presentations have no use for them.
Now "λ terms" include both variable binding and substitution. Ebbinghaus et al. defined the notation for substitution as $\varphi\frac{t_0\ldots t_r}{x_0\ldots x_r}$ and well explained its "meaning". I'm looking for a similar definition for variable binding, including both notation and "meaning". Here are my ideas how it could be defined:
- $\exists x=t\;.\,\varphi$ as abbreviation for $\exists x(x=t\land \varphi)$
- $x:=t\;.\,\varphi$ as abbreviation for $\exists x'(x'=t\land \varphi\frac{x'}{x})$ where $x'\notin\operatorname{var}(t)\cup\operatorname{free}(\varphi)$
- $x:=t\;.\,\varphi$ as abbreviation for $\forall x'(x'=t\rightarrow \varphi\frac{x'}{x})$ where $x'\notin\operatorname{var}(t)\cup\operatorname{free}(\varphi)$
- $\forall x=t\;.\,\varphi$ as abbreviation for $\forall x(x=t\rightarrow \varphi)$
- $x=t:\varphi$ as notation for variable binding, i.e. an abbreviation for $\forall x=t\;.\,\varphi$
In case $x\notin\operatorname{var}(t)$, all these definitions should be equivalent. My initial impression was that the definitions with $x:=t\;.\,\varphi$ (they are equivalent) make most sense, but then I wondered whether it wouldn't be better to simply ignore the case $x\in\operatorname{var}(t)$. After all, it only complicates the definition without offering anything comparable to the "lexical scoping" of normal substitution or λ terms. The definition with $\exists x=t\;.\,\varphi$ would behave a bit unintuitive for variable binding in case there is more than one $x$ satisfying $x=t$. However, the definition with $\forall x=t\;.\,\varphi$ seems to behave well for variable binding, similar to the intuitive "assume $x=t$ then $\varphi$". Hence $x=t:\varphi$ could refer to this definition.
Question 1:
Are there authors that define a notation for variable binding (in first-order logic)? Is this notation normally just λ terms, because of the "additional power" provided by "lexical scoping" and the possibility to use λ terms at arbitrary places (for example even inside terms)?
Question 2:
I noticed that the self-reference capabilities of $x=t:\varphi$ (if interpreted as $\forall x=t\;.\,\varphi$) can be used to carry out the deductions of Curry's paradox in first-order logic. This yields the "tautology" $X=(X\rightarrow Y):Y$. Does this speaks in favor of using $x=t:\varphi$ instead of $x:=t\;.\,\varphi$ as definition for variable binding in first-order logic? (Especially considering that λ terms are more useful than variable binding by $x:=t\;.\,\varphi$ anyway.)
