Return to Question

I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. 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 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\mathtt{N}\to W\oplus\mathtt{N}$ is the extension defined by $\bar{\sigma}(n)=n$ for all $n\in\mathtt{N}$ and ${\cal M}:{\bf P}(V)\to{\bf P}(V\oplus\mathtt{N})$ is the operation replacing all bound variables of a formula by elements of the copy of $\mathtt{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\mathtt{N}:[k/x]\mbox{ avoids capture in }{\cal M}(\phi_{1})\}$

I have an injective map $i:V\to W$ which induces a corresponding embedding $i:{\bf P}(V)\to{\bf P}(W)$ between formulas. My question is:

Question: is it true that $\Gamma$ consistent $\ \Rightarrow\ $ $i(\Gamma)$ consistent

When $V$ is an infinite set I know what to do: I can carry back any proof underlying the sequent $i(\Gamma)\vdash\bot$ into a proof of $\Gamma\vdash\bot$ by substituting variables from $W$ to $V$ while avoiding capture. The problem arises when $V$ is a finite set. I can no longer be sure I can carry back proofs while avoiding capture. I am looking for a reference where this question may have been dealt with, or any hints on how to approach the problem. More generally, this question can be phrased as follows: given $\phi\in{\bf P}(V)$ with $V$ finite, I want to show the implication $\vdash i(\phi)\ \Rightarrow\ \vdash\phi$. Heuristically, if $\phi\in{\bf P}(V)$ can be proved with variables in $W\supseteq V$, then it can also be proved with variables in $V$. This question is motivated by Gödel's completeness theorem which I am attempting to prove on ${\bf P}(V)$ for $V$ finite, following a Henkin type proof: as I add new variables to the language, I need to make sure consistency is preserved, i.e. that I have a conservative extension.

EDIT: Following Andreas' and Noah's answer, I have hopefully made the question clearer.

I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. 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 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\mathtt{N}\to W\oplus\mathtt{N}$ is the extension defined by $\bar{\sigma}(n)=n$ for all $n\in\mathtt{N}$ and ${\cal M}:{\bf P}(V)\to{\bf P}(V\oplus\mathtt{N})$ is the operation replacing all bound variables of a formula by elements of the copy of $\mathtt{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\mathtt{N}:[k/x]\mbox{ avoids capture in }{\cal M}(\phi_{1})\}$

I have an injective map $i:V\to W$ which induces a corresponding embedding $i:{\bf P}(V)\to{\bf P}(W)$ between formulas. My question is:

Question: is it true that $\Gamma$ consistent $\ \Rightarrow\ $ $i(\Gamma)$ consistent

When $V$ is an infinite set I know what to do: I can carry back any proof underlying the sequent $i(\Gamma)\vdash\bot$ into a proof of $\Gamma\vdash\bot$ by substituting variables from $W$ to $V$ while avoiding capture. The problem arises when $V$ is a finite set. I can no longer be sure I can carry back proofs while avoiding capture. I am looking for a reference where this question may have been dealt with, or any hints on how to approach the problem. More generally, this question can be phrased as follows: given $\phi\in{\bf P}(V)$ with $V$ finite, I want to show the implication $\vdash i(\phi)\ \Rightarrow\ \vdash\phi$. Heuristically, if $\phi\in{\bf P}(V)$ can be proved with variables in $W\supseteq V$, then it can also be proved with variables in $V$. This question is motivated by Gödel's completeness theorem which I am attempting to prove on ${\bf P}(V)$ for $V$ finite, following a Henkin type proof: as I add new variables to the language, I need to make sure consistency is preserved, i.e. that I have a conservative extension.

EDIT: Following Andreas' and Noah's answer, I have hopefully made the question clearer.

LAST EDIT: I have been stuck on this for a few weeks now. However, I am very hopeful the following strategy will work: first, spell out the details of an LK Gentzen type system in this particular setting ($V$ possibly finite, $[y/x]$ essential rather than just avoiding capture) which is equivalent to the Hilbert system. Then for all $i:V\to W$ injective, show the implication $i(\Gamma)\vdash i(\Delta)$ provable without cut $\Rightarrow$ $\Gamma\vdash\Delta$ provable without cut. Finally show that cut elimination holds in this setting. Proofs of the cut elimination theorem (e.g. Takeuti) seem to rely on an infinite supply of variables. However, if I am right about the implication $\Rightarrow$, I can always embed a sequent in a larger space to eliminate cut and bring it back to the smaller space. Comments and suggestions are very welcome.

I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. 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$. I have an injective map $i:V\to W$ which induces a corresponding embedding $i:{\bf P}(V)\to{\bf P}(W)$ between formulas. I assume that $\Gamma\subseteq{\bf P}(V)$ is a consistent subset, namely that the sequent $\Gamma\vdash\bot$ is false in relation to some Hilbert-style deductive system. I am trying to establish that $i(\Gamma)$ is itself consistent. When $V$ is an infinite set I know what to do: I can carry back any proof underlying the sequent $i(\Gamma)\vdash\bot$ into a proof of $\Gamma\vdash\bot$ by substituting variables from $W$ to $V$ while avoiding capture. The problem arises when $V$ is a finite set. I can no longer be sure I can carry back proofs while avoiding capture. I am looking for a reference where this question may have been dealt with, or any hints on how to approach the problem. More generally, this question can be phrased as follows: given $\phi\in{\bf P}(V)$ with $V$ finite, I want to show the implication $\vdash i(\phi)\ \Rightarrow\ \vdash\phi$. Heuristically, if $\phi\in{\bf P}(V)$ can be proved with variables in $W\supseteq V$, then it can also be proved with variables in $V$. This question is motivated by Gödel's completeness theorem which I am attempting to prove on ${\bf P}(V)$ for $V$ finite, following a Henkin type proof: as I add new variables to the language, I need to make sure consistency is preserved, i.e. that I have a conservative extension.

EDIT: Following Andreas' answer, I realize no-one can really answer this question unless I spell out the details of a specific deductive system. This is all the more important as when dealing with a finite set $V$, it is very easy to spell out specialization axioms of the form $\forall x\phi_{1}\to\phi_{1}[y/x]$ with some caveats on variable capture which will effectively exclude many reasonable (valid) formulas which will not even be theorems (I discuss this point more fully in the post Axiomatization of first order logic (finitely many variables). When that happens, Gödel's completeness theorem will fail and we shall have cases of consistent subsets $\Gamma\subseteq{\bf P}(V)$ for $V$ finite which are no longer consistent when embedded into a larger ${\bf P}(W)$. For example, when $V=\{x,y\}$ with $x\neq y$, it is very easy to spell out an axiomatization on ${\bf P}(V)$ whereby the formula $\forall x\forall y(x\in y)\to\forall x(y\in x)$ is not regarded as a legitimate instance of a specialization scheme, and is therefore excluded as an axiom without there being any way to make it a theorem. So $\Gamma=\{ [\forall x\forall y(x\in y)\to\forall x(y\in x)]\to\bot\}$ will be consistent in ${\bf P}(V)$ but not in ${\bf P}(W)$ where $W=\{x,y,z\}$ with $x,y,z$ distinct. So here we go:

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

I am not insisting on this particular system, especially as I am not defining essential substitutions of variables (a sketch of such definition may however be found in my other post already referred to). I am very happy for someone to propose something reasonable (hopefully leading to the same set of true sequents $\Gamma\vdash\phi$) where consistent subsets $\Gamma\subseteq{\bf P}(V)$ remain consistent once embedded into a larger ${\bf P}(W)$. This is what we need I think to achieve a complete axiomatization on ${\bf P}(V)$. For those questioning the pertinence of finite variable fragments of FOL (a legitimate concern by all means), I refer them to my 'EDIT' section of the post mentioned above.

I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. 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 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\mathtt{N}\to W\oplus\mathtt{N}$ is the extension defined by $\bar{\sigma}(n)=n$ for all $n\in\mathtt{N}$ and ${\cal M}:{\bf P}(V)\to{\bf P}(V\oplus\mathtt{N})$ is the operation replacing all bound variables of a formula by elements of the copy of $\mathtt{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\mathtt{N}:[k/x]\mbox{ avoids capture in }{\cal M}(\phi_{1})\}$

I have an injective map $i:V\to W$ which induces a corresponding embedding $i:{\bf P}(V)\to{\bf P}(W)$ between formulas. My question is:

Question: is it true that $\Gamma$ consistent $\ \Rightarrow\ $ $i(\Gamma)$ consistent

When $V$ is an infinite set I know what to do: I can carry back any proof underlying the sequent $i(\Gamma)\vdash\bot$ into a proof of $\Gamma\vdash\bot$ by substituting variables from $W$ to $V$ while avoiding capture. The problem arises when $V$ is a finite set. I can no longer be sure I can carry back proofs while avoiding capture. I am looking for a reference where this question may have been dealt with, or any hints on how to approach the problem. More generally, this question can be phrased as follows: given $\phi\in{\bf P}(V)$ with $V$ finite, I want to show the implication $\vdash i(\phi)\ \Rightarrow\ \vdash\phi$. Heuristically, if $\phi\in{\bf P}(V)$ can be proved with variables in $W\supseteq V$, then it can also be proved with variables in $V$. This question is motivated by Gödel's completeness theorem which I am attempting to prove on ${\bf P}(V)$ for $V$ finite, following a Henkin type proof: as I add new variables to the language, I need to make sure consistency is preserved, i.e. that I have a conservative extension.

EDIT: Following Andreas' and Noah's answer, I have hopefully made the question clearer.

I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. I have an injective map $i:V\to W$ which induces a corresponding embedding $i:{\bf P}(V)\to{\bf P}(W)$ between formulas. I assume that $\Gamma\subseteq{\bf P}(V)$ is a consistent subset, namely that the sequent $\Gamma\vdash\bot$ is false in relation to some Hilbert-style deductive system. I am trying to establish that $i(\Gamma)$ is itself consistent. When $V$ is an infinite set I know what to do: I can carry back any proof underlying the sequent $i(\Gamma)\vdash\bot$ into a proof of $\Gamma\vdash\bot$ by substituting variables from $W$ to $V$ while avoiding capture. The problem arises when $V$ is a finite set. I can no longer be sure I can carry back proofs while avoiding capture. I am looking for a reference where this question may have been dealt with, or any hints on how to approach the problem. More generally, this question can be phrased as follows: given $\phi\in{\bf P}(V)$ with $V$ finite, I want to show the implication $\vdash i(\phi)\ \Rightarrow\ \vdash\phi$. Heuristically, if $\phi\in{\bf P}(V)$ can be proved with variables in $W\supseteq V$, then it can also be proved with variables in $V$. This question is motivated by Gödel's completeness theorem which I am attempting to prove on ${\bf P}(V)$ for $V$ finite, following a Henkin type proof: as I add new variables to the language, I need to make sure consistency is preserved, i.e. that I have a conservative extension.

I am looking at FOL with no equality, no constant, no function symbol and the unique binary predicate $\in$ with variables in arbitrary sets $V$ or $W$. 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$. I have an injective map $i:V\to W$ which induces a corresponding embedding $i:{\bf P}(V)\to{\bf P}(W)$ between formulas. I assume that $\Gamma\subseteq{\bf P}(V)$ is a consistent subset, namely that the sequent $\Gamma\vdash\bot$ is false in relation to some Hilbert-style deductive system. I am trying to establish that $i(\Gamma)$ is itself consistent. When $V$ is an infinite set I know what to do: I can carry back any proof underlying the sequent $i(\Gamma)\vdash\bot$ into a proof of $\Gamma\vdash\bot$ by substituting variables from $W$ to $V$ while avoiding capture. The problem arises when $V$ is a finite set. I can no longer be sure I can carry back proofs while avoiding capture. I am looking for a reference where this question may have been dealt with, or any hints on how to approach the problem. More generally, this question can be phrased as follows: given $\phi\in{\bf P}(V)$ with $V$ finite, I want to show the implication $\vdash i(\phi)\ \Rightarrow\ \vdash\phi$. Heuristically, if $\phi\in{\bf P}(V)$ can be proved with variables in $W\supseteq V$, then it can also be proved with variables in $V$. This question is motivated by Gödel's completeness theorem which I am attempting to prove on ${\bf P}(V)$ for $V$ finite, following a Henkin type proof: as I add new variables to the language, I need to make sure consistency is preserved, i.e. that I have a conservative extension.