# If $\vdash A$, then $\vdash A[x:=t]$

Let $$A$$ be a formula, $$x$$ a variable, $$t$$ a term and $$\Gamma$$ a set of formulas. If $$\Gamma\vdash A$$ and $$x$$ is not a free variable of some open assumption, then $$\Gamma\vdash A\to\forall_xA$$ and $$\vdash \forall_xA\to A[x:=t]$$ by the natural deduction rules. Thus, $$\Gamma\vdash A[x:=t]$$.

However, I was just told that $$\tag{1}\text{If }\vdash A\text{, then }\vdash A[x:=t]$$ is also true when $$x$$ is a free variable of $$A$$. I have the impression that $$(1)$$ does not follow from the natural deduction rules and I hope someone can elaborate on this. Is $$(1)$$ an additional axiom?

Addendum: Maybe I should mention how derivability was defined in my lecture:

Definition: A formula $$A$$ is called derivable in minimal logic, written $$\vdash A$$, if there is a derivation of $$A$$ without free assumptions using the natural deduction rules. $$A$$ is called derivable from assumptions $$A_1, \ldots, A_n$$ if there is a derivation of $$A$$ with free assumptions among $$A_1, \ldots, A_n$$. Let $$\Gamma$$ be a set of formulas. We write $$\Gamma\vdash A$$ if the formula $$A$$ is derivable from finitely many assumptions $$A_1,\ldots , A_n \in\Gamma$$.

• How do you interpret "$\vdash A$" when $A$ is not a closed formula? It's either nonsense or it means that $A$ is provable no matter what terms you put for the free variables.
– Karl
Nov 27 '21 at 16:50
• @Karl From my lecture notes: A formula $A$ is called derivable in minimal logic, written $\vdash A$, if there is a derivation of $A$ without free assumptions using the natural deduction rules. Nov 27 '21 at 16:52
• Also note that your conclusion that $\vdash A\to A[x:=t]$ when $x$ is not free in $A$ is sort of vacuously true, since $[x:=t]$ only modifies free occurrences of $x$.
– Karl
Nov 27 '21 at 16:55
• Right, so how would one derive a formula containing a free variable?
– Karl
Nov 27 '21 at 16:56
• @Karl I don't really know what to answer. We simply assume that $A$ is derivable. Maybe we can even consider the case $\Gamma\vdash A$ and ask if this implies $\Gamma\vdash A[x:=t]$. Of course, the fact that I don't see a problem doesn't mean that there isn't one. Nov 27 '21 at 17:05

Based on your most recent comment, yes, (1) is a special case when $$\Gamma$$ is empty.

I'm not exactly sure what part of the argument in the introduction you're skeptical of. I'm writing the answer under the assumption that it's the side condition that we impose on $$\Gamma$$. If this is mistaken, I'll amend my answer. I'm trying to avoid retreating to the semantics of first-order minimal logic (which is the system I think you're working in).

So, we have a way of eliminating the pesky side condition that $$x$$ does not occur as a free variable of any open assumption. That side condition is very convenient to use in a proof calculus though.

$$\frac{\Gamma \vdash A}{\Gamma[x := t] \vdash A[x:=t]} \;\; \text{holds}$$

Imposing the side condition is just a way of making sure that $$\Gamma$$ is equal to $$\Gamma[x:=t]$$.

When $$\Gamma$$ is empty the side condition is trivial since $$\varnothing$$ never contains any formulas and thus never contains any free variables.

• Thank you very much for the answer. The problem is that we haven't really discussed when and how the expression $A[x:=t]$ is defined in the lecture. I have the impression that you are using the following fact: If $x$ is not free in $B$, then $B[x:=t]=B$. Is that correct? Nov 27 '21 at 18:45
• Yes, what you are saying is correct. $A[x:=t]$ is equal to $A$ if and only if $x$ is equal to $t$ or $x \not\in \text{FV}(A)$. Let $\text{FV}(A)$ refer to the free variables of $A$. $A[x:=t]$ can be defined inductively on formulas by finding free occurrences of $x$ and replacing them with $t$. There is some complexity that you have to deal with if $t$ itself has free variables that might end up being captured. For example, what should the following mean: $(\forall y \mathop. x =y)[y := f(x)]$ ? I don't think there's one universal convention for how to deal with this problem. Nov 27 '21 at 18:55