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)$:


(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.


2 Answers 2


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.

  • $\begingroup$ Yes I am assuming a given reasonable system: 3 propositional axioms + $\forall x(\phi_{1}\to\phi_{2})\to(\phi_{1}\to\forall x\phi_{2})$ with $x$ not free in $\phi_{1}$ and $\endgroup$ Jul 23, 2013 at 15:46
  • $\begingroup$ and specialization $\forall x\phi_{1}\to\phi_{1}[y/x]$, being understood that the substitution of variable $[y/x]:{\bf P}(V)\to{\bf P}(V)$ avoids capture. Apart from modus ponens, I assume generalization on variables which are not free in any hypothesis of proof. Such system is sound and allow deduction theorem to be stated in full generality (e.g. does not require formulas to be closed) $\endgroup$ Jul 23, 2013 at 15:55

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.

  • $\begingroup$ I suppose I'm implicitly assuming, in the latter part, that $V$ is nonempty. But I don't imagine that we care about this. $\endgroup$ Aug 23, 2013 at 1:11
  • $\begingroup$ yes $V$ nonempty is fine, I can treat the case separately. Thank you very much for this. Will study your answer carefully and revert. $\endgroup$ Aug 23, 2013 at 4:29
  • $\begingroup$ It just occurred to me that most of my answer is vacuous: if we disallow negation, then we're looking at positive sentences only, and any set of positive sentences is consistent. :P $\endgroup$ Aug 23, 2013 at 6:20
  • $\begingroup$ On the initial part of your answer, we do require $f:V\to W$ to be injective. However, formulas may have free variables so you could even choose $\Gamma=\{x E y, (y E y)\to\bot\}$ to make your point. Consistency cannot realistically be preserved without injectivity. More to come on your second part. $\endgroup$ Aug 23, 2013 at 12:53
  • $\begingroup$ @ Noah on the second part, I agree with your conclusion that if $\Gamma$ is satisfiable (There is an $(M,r)$ $r$ binary on $M$ and a variable assignment $a:V\to M$ such that $M\vDash\phi[a]$ for all $\phi\in\Gamma$), then so is $f(\Gamma)$, for all $f:V\to W$, provided the associated $f:{\bf P}(V)\to{\bf P}(W)$ avoids capture on every element of $\Gamma$ (or is regarded as 'essential' which is what you implicitly assume, and which works fine when $W$ is infinite set or $|V|\leq|W|$). The real issue is.... $\endgroup$ Aug 23, 2013 at 13:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.