The rules of inference for quantifiers in first order logic involve replacing variables in expressions with other terms. One way to define the substitution $\phi[t/x]$ is that $\phi[t/x]$ arises from $\phi$ by replacing all occurrences of $x$ with $t$. For example:
$$
\phi \equiv Pxy \implies Qxyz
$$
Then
$$
\phi[t/x] \equiv Pty \implies Qtyz
$$
This simple definition of substitution however gives rise to the issues of the "capture" of variables within the substitution terms by quantifiers in the original expression. For example
$$
\phi \equiv (\forall y)Qxy
$$
Suppose $t=y$ then
$$
\phi[t/x] \equiv \phi [y/x] \equiv (\forall y)Qyy
$$
Which is not an equivalent logical statement. The replacement is valid by the definition above because $x$ \textit{is} free in $\phi$. The problem is that the $y$ in $t$ is captured by the $(\forall y)$ quantifier in $\phi$.
When writing down proof systems we can deal with this in one of two ways.
The first option is we can redefine the substitution operation so that substitution is invalid whenever such a capture would occur. To do this we would define $\phi[t/x]$ as arising from $\phi$ by replacing all occurrences of $x$ by $t$ provided that $x$ does not appear in $\phi$ within the scope of any quantifiers over any variables that appear in $t$. In this case the inference rules can use the replacement notation directly since there is no concern about variable capture.
The second option is to keep the definition of substitution simple, and add the corresponding proviso to the rules of inference to ensure we don't make any invalid inferences. In this approach we define a concept of substitutability. We say that $x$ is free for $t$ in $\phi$, or $t$ is substitutable for $x$ in $\phi$ if for any variable $y$ that appears in $t$ it is not the case that $x$ appears in the scope of a quantifier of the form $(\forall y)$ or $(\exists y)$ within $\phi$. In this approach the inference rules are written down using the substitution notation, but we must add the proviso that the appropriate variables are free for the relevant substitutions.
My question is as follows. Say we take the second approach. Is there any standard notion to indicate that $x$ is free for $t$ in $\phi$? Most textbooks I see have no such notation. They simply have to express the concept in words in proximity to the inference rules of interest. I would prefer some metalogical way to notate this to make the inference rule definitions more compact and clear. A proposal would be something like $_{t/x}\phi$ means that $t$ is substitutable for $x$ in $\phi$.
A related question: Sometimes instead the inference rules require that $\phi$ NOT include some variable free. For example, an inference rule is valid conditioned on $y$ not appearing free in $\phi$. Is there any way to notate this as well? $\phi\{y\}$ or something…
Best Answer
It is straightforward to construct a uniquely determined relation between terms, variables and formulas for a first-order language that holds exactly if the term is freely substitutable for the variable in the formula. After that you can denote it via a metalanguage name of your choice .
We presuppose uniquely determined functions $free(\cdot), var(\cdot)$ sending formulas to the set of their free variables and sending terms to the set of variables occurring in them, respectively. Let $t$ be a term and $x$ a variable. By recursion on the structure of formulas we define a relation $\mathcal{R}$ between terms, variables and formulas by stipulating that $\mathcal{R}(t, x, \varphi)$ holds iff one of the following is the case:
It is straightforward to see that this relation is uniquely determined.