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

Solution 1:

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.