Dtjytyk

Let $Sigma$ be a set of $L$-sentences and let $sigma$ be an $L$-sentence. Assume $Sigmavdash_Lsigma$ (in the calculus $mathcal{C}_1$ of first order logic without equality). Prove that there is a deduction of $sigma$ from $Sigma$ in $mathcal{C}_1$ consisting in $L$-sentences.

I have the idea quite clear, but writing it is proving more difficult than expected (It might be not that clear then... or I'm just complicating myself)

Some context Recall that a $L$-sentence is a formula with no free variable.
The axioms for $mathcal{C}_1$ are

1. $(varphi rightarrow (psirightarrowvarphi))$


2. $(varphi rightarrow (psirightarrowchi)) rightarrow ((varphirightarrowpsi) rightarrow (varphirightarrowchi))$


3. $((negvarphirightarrownegpsi)rightarrow ((negvarphirightarrownegpsi)rightarrowvarphi))$


4. 
   $forall xvarphi rightarrow varphibinom{x}{t}$, with $t$ freely substitutable for $x$ in $varphi$
   


5. $forall x (varphirightarrow psi) rightarrow (forall x varphi rightarrowforall x psi)$


6. 
   $(varphi rightarrow forall x varphi)$ with $x$ not free in $varphi$
   

And we also have $MP$ (Modus Ponen)
begin{array}{l}
(varphirightarrow psi)\
varphi\
hline
psi
end{array}

Axioms 1 to 3 are from $mathcal{C_0}$

My though
Because $Sigmavdash_Lsigma$, then there exist a dedution of $sigma$ from $Sigma$
$$ D :left{ begin{array}{cl}
varphi_1\
varphi_2\
vdots\
varphi_n &= sigma
end{array}right.$$
With every $varphi_i$ is either an element of $Sigma$, an axiom of $mathcal{C}_1$ or obtained by MP from the previous formulas.

Suppose first that no axioms are necessary for the deduction. Then necessarily, $varphi_1inSigma$ $L$-sentence. We can reason by induction : Suppose that true for all $i-1$. look at $varphi_i$,

• if it is from $Sigma$ then we're done


• if it is from $MP$, then there exist $a<i$ and $b<i$ such that $varphi_a$ is $(varphi_brightarrowvarphi_i)$. By induction $varphi_a$ and $varphi_b$ are sentences. hence $varphi_i$ must be too. It need some writing but the idea is here.

The issue arises with axioms. Axioms 1 to 3 are quantifier free, so I guess that they cannot introduce free variables. With the same idea, Axioms 5 and 6 cannot introduce free variable in the deduction. Axioms 4 could, but then because are last formule $sigma$ is a sentence, I guess that there would be no way to get "rid of it"...

I'm not sure on how to redact this last part, the whole block regarding the introduction of axioms. If someone can help or direct me to some source.
Thanks

Hint

The proof is by induction on the derivation $D$, considering the fact that in it we may have only a finite number of variables $y_1, ldots, y_n$ that have free occurrences in formulas.

We need new distinct constant symbols $c_1, ldots, c_n$ that never appear in $D$ and we replace each term $t$ in $D$ by $t' := t[y_i/c_i]$ and each formula $theta$ in $D$ by $theta ' := theta [y_i/c_i]$.

What we get, is a new derivation $D'$ with the desired property.

The base step is straightforwrd (as you noted) for all axioms except one; the induction step is also obvious, because the only inference rule : Modus Ponens, does not modify sentences.

The only point to be carefully checked is (Ax.4) : $∀xφ → φ[x/t]$, with $t$ freely substitutable for $x$ in $φ$.

We have to check that the above defined transformation does not "invalidate" the axiom, i.e. that

$(∀xφ → φ[x/t])' := ∀xφ' → φ'[x/t']$, where $t'$ is freely substitutable for $x$ in $φ'$.

Now, $x$ cannot be one of $y_1,ldots,y_n$, because $x$ is neither free in $(∀xφ)$ nor in $φ[x/t]$.

Thus we have that $(∀xφ)' := ∀xφ'$ and $(φ[x/t])':= φ'[x/t']$.

We have only to check that $t'$ is freely substitutable for $x$ in $φ'$.