Let $\Sigma$ be a set of $L$-sentences and let $\sigma$ be an $L$-sentence. Assume $\Sigma\vdash_L\sigma$ (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 (\psi\rightarrow\varphi))$
  2. $(\varphi \rightarrow (\psi\rightarrow\chi)) \rightarrow ((\varphi\rightarrow\psi) \rightarrow (\varphi\rightarrow\chi))$
  3. $((\neg\varphi\rightarrow\neg\psi)\rightarrow ((\neg\varphi\rightarrow\neg\psi)\rightarrow\varphi))$
  4. $\forall x\varphi \rightarrow \varphi\binom{x}{t}$, with $t$ freely substitutable for $x$ in $\varphi$
  5. $\forall x \ (\varphi\rightarrow \psi) \rightarrow (\forall x \varphi \rightarrow\forall x \psi)$
  6. $(\varphi \rightarrow \forall x \varphi)$ with $x$ not free in $\varphi$

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

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

My though Because $\Sigma\vdash_L\sigma$, 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_1\in\Sigma$ $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_b\rightarrow\varphi_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



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


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.