Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

We consider the language ${\cal L}=\{\in\}$ with an arbitrary set of variables $V$. Specifically we define ${\bf P}(V)$ as the free algebra of type $\{\bot,\to\}\cup\{\forall x:x\in V\}$ (with the obvious arity for each symbol) generated by the ordered pairs $(x,y)$, denoted $(x\in y)$, for $x,y\in V$. We consider the following Hilbert-style axiomatization on ${\bf P}(V)$:

Axioms:

(i) $\phi_{1}\to(\phi_{2}\to\phi_{1})$

(ii) $\phi_{1}\to(\phi_{2}\to\phi_{3})\to[(\phi_{1}\to\phi_{2})\to(\phi_{1}\to\phi_{3})]$

(iii) $[(\phi_{1}\to\bot)\to\bot]\to\phi_{1}$

(iv) $\forall x(\phi_{1}\to\phi_{2})\to(\phi_{1}\to\forall x\phi_{2})\ ,\ x\not\in\mathtt{Fr}(\phi_{1})$

(v) $\forall x\phi_{1}\to\phi_{1}[y/x]\ \ ,\ \ \mbox{$[y/x]:{\bf P}(V)\to{\bf P}(V)$ essential substitution of $y$ in place of $x$}$

Rules of inference :

(i) Modus ponens

(ii) Generalization w.r. to $x\in V$ which do not appear free in any hypothesis

An essential substitution $\sigma^{*}:{\bf P}(V)\to{\bf P}(W)$ associated with a map $\sigma:V\to W$ is a map which satisfies the property ${\cal M}\circ\sigma^{*}=\bar{\sigma}\circ{\cal M}$ where $\bar{\sigma}:V\oplus\mathbb{N}\to W\oplus\mathbb{N}$ is the extension defined by $\bar{\sigma}(n)=n$ for all $n\in\mathbb{N}$ and ${\cal M}:{\bf P}(V)\to{\bf P}(V\oplus\mathbb{N})$ is the operation replacing all bound variables of a formula by elements of the copy of $\mathbb{N}$ disjoint from $V$, as specified by the following recursion:

$(i)\ {\cal M}(x\in y)=(x\in y)$ $(ii)\ {\cal M}(\bot)=\bot$ $(iii)\ {\cal M}(\phi_{1}\to\phi_{2})={\cal M}(\phi_{1})\to{\cal M}(\phi_{2})$

$(iv)\ {\cal M}(\forall x\phi_{1})=\forall n{\cal M}(\phi_{1})[n/x]$

where $\ n=\min\{k\in\mathbb{N}:[k/x]\mbox{ avoids capture in }{\cal M}(\phi_{1})\}$

A substitution theorem is a result of the form:

Theorem (Substitution Theorem): $\Gamma\vdash\phi\ \Rightarrow\ \sigma(\Gamma)\vdash\sigma(\phi)$

for all $\sigma:{\bf P}(V)\to{\bf P}(W)$ satisfying [hypothesis here]

I can show the substitution theorem is true for essential substitutions $\sigma:{\bf P}(V)\to{\bf P}(W)$. I also believe it is true for naive variable substitutions $\sigma:{\bf P}(V)\to{\bf P}(W)$ which avoid capture on $\phi$ and every element of $\Gamma$, provided $|W|$ is an infinite cardinal or $|V|\leq|W|$ (this is because essential substitutions can be shown to exist when these conditions on cardinals are met). This leads to my question:

Question: Is the substitution theorem true for naive variable substitutions which avoid capture in the case when $W$ is a finite set smaller than $V$.

I have the feeling (or hope) it should be true, but there may be a simple argument showing my hopes are vain. The difficulty is that a sequent $\Gamma\vdash\phi$ does not say anything about the axioms potentially being used in the underlying proof. So even though $\sigma$ could avoid capture on $\phi$ and the elements of $\Gamma$, there is no guarantee it will avoid capture on the axioms. So I cannot hope to translate a proof from the larger space into the smaller space. This is the limitation I think of the Hilbert-style deduction system where we have no control on the complexity of proofs (but of course the experts already know that, I am simply learning the hard way). I am hoping a careful study of Gentzen $\bf LK$-system will allow me to have a better control on proofs once we show that cut elimination can hold in this setting. Comments or suggestions are very welcome.

share|improve this question
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.