Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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$?

share|improve this question
    
I'm curious: in which context is this a real problem? –  user2035 Oct 11 '11 at 18:53
add comment

5 Answers

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!)

share|improve this answer
add comment

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.

share|improve this answer
add comment

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$.

share|improve this answer
1  
You can find an explicit construction of this in Muchnick's "Advanced Compiler Design & Implementation" in the section on static single-assignment form (SSA). –  Chad Musick Oct 12 '11 at 1:16
add comment

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.

share|improve this answer
    
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. –  Carl Mummert Oct 11 '11 at 21:23
add comment

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.