1
$\begingroup$

Often in logic, you want to define a formula $\phi(x)$ which "says something about $x$". For example, $\phi(x)$ may say that $x$ is a prime. In order to form $\phi$, you may need internal bound variables, for example $\phi(x)$ may have the form $\phi(x) = \exists y \alpha(x,y)$.

Unfortunately, you cannot apply this formula $\phi(x)$ to the variable $y$, as this will create a collision with respect to the internal bound variable $y$. This is really a pain because you want to allow the substitution of any term $t$ to substitute for $x$, and the resulting formula $\phi(t)$ should express some property of $t$. But now you have to worry about whether the term $t$ contains the variable $y$ or not. You would really like $y$ to be a local variable, which is renamed in case the substituted term $t$ contains a copy of $y$.

An analogous situation in computer programming is local vs global namespaces for variables. In most programming languages, a function may have local variables. You can pass any argument, including variables, to the function, and not have to worry about collisions between the local variables and global variables. In the standard treatment of first-order logic, all of the variables are global variables.

Is there any way to define a formula $\phi(x)$, in such a way that any term may be substituted for $x$?

Improve this question
$\endgroup$
1
  • $\begingroup$ I'm curious: in which context is this a real problem? $\endgroup$
    – user2035
    Commented Oct 11, 2011 at 18:53

5 Answers 5

Reset to default
5
$\begingroup$

I don't think there is any solution to the problem as you pose it. Neil and Carl have mentioned the standard approach, which is to rename bound variables, whenever you perform a substitution, to avoid variable capture. This works, but it is tedious and error-prone if you have to write it down or implement it explicitly; for this reason I have heard it said that "variable binding is one of the most annoying aspects of formalizing anything." But you may be interested in some of the workarounds that smart people have come up with:

(People who know more about the subject than I do, please add and comment!)

Improve this answer
$\endgroup$
4
$\begingroup$

This kind of issue is handled carefully in mathematical treatments of lambda calculus (which is just the abstract version of Lisp). The Wikipedia page on lambda calculus has some discussion of this under 'capture-avoiding substitutions'. I've not worked through it in detail but I don't think that anything very subtle comes up, you just need a rigorous formulation of what it means for a variable to be bound and the sense in which bound variables can harmlessly be renamed.

Improve this answer
$\endgroup$
4
$\begingroup$

One elegant solution is to apply the following theorem from Enderton's logic book (Theorem 24I):

Let $\phi$ be a formula, $t$ a term, and $x$ a variable. There is a formula $\phi'$ such that $\vdash \phi \leftrightarrow \phi'$ and $t$ is substitutable for $x$ in $\phi'$.

Using this, we can (re)define $\phi(t)$ to mean $\phi'[t/x]$ where $\phi'$ is as in the theorem and $[t/x]$ is the syntactical substitution of $t$ for $x$. Then $\phi(t)$ is well defined up to provable equivalence for any formula $\phi(x)$ and any term $t$.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ You can find an explicit construction of this in Muchnick's "Advanced Compiler Design & Implementation" in the section on static single-assignment form (SSA). $\endgroup$
    – Chad Musick
    Commented Oct 12, 2011 at 1:16
  • $\begingroup$ So would this be a good illustration of how to use this in practice: you have defined $x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y)$ so generalizing $\forall x\forall y(x=y\leftrightarrow\forall z(z\in x\leftrightarrow z\in y))$ but then you can't substitute $x$ or $y$ in for $z$ (even if you're trying to prove something as simple as $z=z$) so instead you first prove that $\forall x\forall y(x=y\leftrightarrow\forall t(t\in x\leftrightarrow t\in y))$ (which is logically equivalent to the first WFF) and you are now free to substitute in for $z$ and prove things like $z=z$ $\endgroup$
    – Pineapple Fish
    Commented Dec 17, 2021 at 16:11
  • $\begingroup$ It seems to be that the way in Enderton's book is much more practical when supplemented with extension by definition; en.wikipedia.org/wiki/Extension_by_definitions . Because Enderton's solution still doesn't allow you to arbitrarily substitute (and it shouldn't), but what you can do is make a new predicate variable, then use this theorem in Enderton's book, and voila, using metatheory you can prove you now have a WFF/expression with the same meaning into which you can substitute anything! $\endgroup$
    – Pineapple Fish
    Commented Dec 17, 2021 at 16:20
2
$\begingroup$

Yet another approach is to have distinct sets of symbols for free variables and bound variables. This is the approach used by Takeuti in Proof Theory, but it probably originates from earlier than that.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I considered this in my answer, but it has the same renaming problem in a different place. In this approach, if you begin with $(\exists x)\phi$ and want to remove the quantifier, you have to do a variable substitution to replace $x$ with a variable that can be free in order to obtain a well formed formula. $\endgroup$
    – Carl Mummert
    Commented Oct 11, 2011 at 21:23
1
$\begingroup$

If you define $\phi(x) = \exists y \alpha(x, y)$ and then later in your paper you talk about $\phi(y)$ then this is fine. I'm not going to think that the two $y$s have to be the same.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .