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

  • $\begingroup$ 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. $\endgroup$
    – Karl
    Nov 27 '21 at 16:50
  • $\begingroup$ @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. $\endgroup$
    – Filippo
    Nov 27 '21 at 16:52
  • $\begingroup$ 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$. $\endgroup$
    – Karl
    Nov 27 '21 at 16:55
  • $\begingroup$ Right, so how would one derive a formula containing a free variable? $\endgroup$
    – Karl
    Nov 27 '21 at 16:56
  • $\begingroup$ @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. $\endgroup$
    – Filippo
    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.

  • $\begingroup$ 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? $\endgroup$
    – Filippo
    Nov 27 '21 at 18:45
  • 1
    $\begingroup$ 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. $\endgroup$ Nov 27 '21 at 18:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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