Embedding of consistent subset in first order logic (finitely many variables)

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.

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.

Answer 1

You refer to "some Hilbert-style deductive system", with no explicit requirement of soundness or reasonableness. In this generality, the result seems to be false. The system could include an axiom "scheme" saying that $(\forall x\forall y\forall z\,\phi)\to\bot$ whenever $x,y,z$ are distinct variables. This, with modus ponens and some other, traditional axioms, would allow you to prove $\bot$ when at least three variables are available but not when there are only two. I suppose you intended the notion of "Hilbert-style" to include some restrictions that prohibit such silly examples, but I'd want to see explicitly what the restrictions are, since they would play a big role in a "real" answer to your question.

Answer 2

The answer is no, if I understand correctly. (I use $E$ instead of $\in$, here, since the latter is fairly meaning-loaded to me.)

Consider the set of sentences $\Gamma=\lbrace \forall x\exists y(xEy), \forall x(\neg xEx) \rbrace$. Then if $V$ has two elements and $W$ has one element, and $f$ is the unique function from $V$ to $W$, clearly $\Gamma$ is consistent but $f(\Gamma)$ is inconsistent.

Does this answer your question?

---

Of course, the key point above is that we have negation. Without negation, the answer to your question is "yes:"

Let me rephrase your question in more semantic terms, which I find easier to deal with. If I understand correctly, you are considering the signature $\Sigma=\lbrace E\rbrace$, where $E$ is a binary relation; then, given sets $V$, $W$ and a map (not a homomorphism) $f: V\rightarrow W$, you are asking whether, given a $\Sigma$-structure $\mathcal{M}$ with domain $V$ and a consistent set $\Gamma$ of sentences with parameters from $V$ which do not use the symbol "=" and are true in $\mathcal{M}$, we can find some $\Sigma$-structure $\mathcal{N}$ with domain $W$ such that $$ \forall \varphi(\overline{a})\in \Gamma, \mathcal{N}\models \varphi(f(\overline{a})).$$ (Quantifying over sets of sentences holding in $\Sigma$-structures should be the same as quantifying over consistent sets of sentences, as long as things aren't terrible.) Without loss of generality, $\Gamma$ is just the set of all sentences with parameters from $V$ true in $\mathcal{M}$; that is, we can just quantify over equality- and negation-free diagrams.

Let $A=ran(f)$, and let $\mathcal{A}=f(\mathcal{M})$ be the structure on $W$ gotten by moving over the structure $\mathcal{M}$, so that $f$ (with new codomain) is a homomorphism from $\mathcal{M}$ to $\mathcal{A}$. $$\text{(Formally, we set $\mathcal{A}=(A; \lbrace (x, y): \mathcal{M}\models f^{-1}(x)Ef^{-1}(y)\rbrace)$.)}$$ $\mathcal{A}$ satisfies $D_{enf}(\mathcal{M})$, the equality- and negation-free diagram of $\mathcal{M}$, by an easy induction.

Clearly if $A=W$, we're done. So suppose $A\not=W$. Now fix $c\in \mathcal{A}$, let $B=W-A$, and consider the structure $\mathcal{N}$ on $W$ gotten from $\mathcal{A}$ by creating several identical copies of $c$. Formally, for $b\in B, x\in W$, we make $bEx$ hold iff $\mathcal{A}\models cEx$, and we make $xEb$ hold iff $\mathcal{A}\models xEc$.

$\mathcal{N}$ is clearly a $\Sigma$-structure with domain $W$; and by induction on the complexity of $\varphi(\overline{a})\in D_{enf}(\mathcal{M})$, we have $\mathcal{N}\models\varphi(f(\overline{a}))$. So we're done.