I'm trying to derive the following rule :

from $α→β$, infer $(∃x)α→β$, provided that $x$ is not free in $β$

in the system of Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001).

The axioms are [see page 112] :

The logical axioms are all generalizations of wffs of the following forms, where $x$ and $у$ are variables and $\alpha$ and $\beta$ are wffs:

  1. Tautologies;

  2. $\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$;

  3. $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$;

  4. $\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.

If the language includes equality, the usual axiom for it are added.

Modus ponens is the sole rule of inference.

What we can prove in Enderton's system is the following meta-theorem :

if $\Gamma \vdash \alpha \rightarrow \beta$, and $x$ is not free in $\beta$ nor in any formula in $\Gamma$, then : $\Gamma \vdash \exists x \alpha \rightarrow \beta$.

Proof :

We have to start from :

(1) $\Gamma \vdash \alpha \rightarrow \beta$

(2) $\Gamma \vdash \lnot \beta \rightarrow \lnot \alpha$ --- from (1) and Taut, by mp

(3) $\lnot \beta$ --- assumed

(4) $\Gamma, \lnot \beta \vdash \lnot \alpha$.

Now, due to the proviso, we can apply the Gen Th to have :

(5) $\Gamma, \lnot \beta \vdash \forall x \lnot \alpha$

(6) $\Gamma \vdash \lnot \beta \rightarrow \forall x \lnot \alpha$ --- from (3) and (5), by Deduction Theorem

(7) $\Gamma \vdash \lnot \forall x \lnot \alpha \rightarrow \beta$ --- from (6) and Taut, by mp

(8) $\Gamma \vdash \exists x \alpha \rightarrow \beta$ --- abbreviation.

From this theorem, under the same proviso, with $\Gamma = \emptyset$ we have :

(A) if $\vdash \alpha \rightarrow \beta$, then $\vdash \exists x \alpha \rightarrow \beta$.

Note : these rules are not stated in Enderton's book, but we can easily derive the last one from the theorem in Example (Q3B) [page 122] :

$\vdash (\exists x \alpha \rightarrow \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, provided that $x$ does not occur free in $\beta$.

Proof :

(1) $\vdash \alpha \rightarrow \beta$

(2) $\vdash \forall x(\alpha \rightarrow \beta)$ --- by Generalization Theorem [page 117] : if $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$, with $\Gamma = \emptyset$.

(3) $\vdash \exists x \alpha \rightarrow \beta$ --- by (Q3B).

In the same way, from the theorem of Example (Q2A) [page 121] :

$\vdash (\alpha \rightarrow \forall x \beta) \leftrightarrow \forall x(\alpha \rightarrow \beta)$, provided that $x$ does not occur free in $\alpha$,

we can prove the meta-theorem :

(B) if $\vdash \alpha \rightarrow \beta$, then $\vdash \alpha \rightarrow \forall x \beta$,

with the same proviso.

Of course, we can deduce it from the "more general" meta-theorem :

if $\Gamma \vdash \alpha \rightarrow \beta$, and $x$ is not free in $\alpha$ nor in any formula in $\Gamma$, then : $\Gamma \vdash \alpha \rightarrow \forall x \beta$

which can easily be proved as the other one.

The rules (A) and (B) are the Rules for the Universal and Existential Quantifiers used by David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic (2nd ed - 1937; see english translation, page 70) and due to Paul Bernays (see footnote); they are used also by S.C.Kleene in his textbooks.

  • $\begingroup$ Re: "From $α→β$, infer $(∃x)α→β$, provided that $x$ is not free in $β.$" Existential generalization need not be this complicated. You rarely see such considerations in mathematics textbooks, and for good reasons. For details, download my free proof-checking software at dcproof.com If there is sufficient interest, I can post excerpts from my user manual for discussion at the sci.math newsgroup. $\endgroup$ May 5, 2014 at 5:38
  • $\begingroup$ @DanChristensen - in so-called Hilbert-style proof system (like Enderton's), this is simply the "equivalent" of the Natutral Deduction rule for $\exists$ Elimination. $\endgroup$ May 6, 2014 at 10:28
  • $\begingroup$ I found the interplay between existential specification and universal generalization to be one of the most difficult problems to solve in my program: How to prohibit deriving $\exists y: \forall x\in S:R(x,y)$ from $\forall x\in S: \exists y: R(x,y)$ in some elegant, easy to explain fashion not too different from how mathematicians actually write proofs. $\endgroup$ May 6, 2014 at 15:31
  • $\begingroup$ @DanChristensen - I'm not sure to understand the formulae; the first one looks like : $(∃y)(∀x)[x∈S \rightarrow R(x,y)]$. Is my "translation" the right one ? Or it is : $(∃y)[(∀x)x∈S \rightarrow R(x,y)]$ ?. For the second one : $(∀x)[x∈S \rightarrow (∃y)R(x,y)]$ ... $\endgroup$ May 6, 2014 at 15:47
  • $\begingroup$ You could translate it as: $\forall x:[x\in S \implies \exists y: R(x,y)].$ I'm just restricting the domain of the universal quantifier. I don't allow introduction of free variables by universal specification ($\forall$ Elimination). $\endgroup$ May 6, 2014 at 15:51

2 Answers 2


The rule

from $α→β$, infer $(∃x)α→β$, provided that $x$ is not free in $β$,

without "constraint" on the assumption $\alpha \rightarrow \beta$, is not sound.

Let $\alpha := x = y$ and let $\beta := \forall x (x = y)$; the proviso that $x \notin FV(\beta)$ is satisfied.

If we apply the above rule, we get :

$\exists x (x = y) \rightarrow \forall x (x = y)$.

But this is not true in a domain with more than one element.

Thus, we need the assumption in the form : $\Gamma \vdash \alpha \rightarrow \beta$, whit proviso that $x$ is not free in $β$ nor in any formula in $\Gamma$.

If we try to use in the "unconstrained" form, we are using it with $\Gamma = \{ α→β \}$, and in this case it is nor more true that $x$ is not free in any formula in $\Gamma$.


I don't know if this works, and it's definitely not formal since I'm not listing the tautologies properly, but maybe it'll get you thinking.

assumption   (1) (α→β) 

hypothesis   (2) (∃x)α 

axiom 4      (3) [(α→β)→∀x(α→β)]

MP (1), (3)  (4) ∀x(α→β)

axiom 3      (5) [∀x(α→β)→(∀xα→∀xβ)]

MP (5), (4)  (6) (∀xα→∀xβ)

MP, Taut, (6) (7) (¬∀xβ→¬∀xα)  (the tautology is CCpqCNqNp in Polish notation)

MP, Taut, (7) (8) (¬¬∀xβ $\lor$ ¬∀xα) (the tautology is CCpqANpq)

MP, Taut, (8) (9)  (¬¬∀xβ $\lor$ ¬∀x¬¬α) (the tautology is CANNpqANNpNNq)

Def. of ∃     (10) (¬¬∀xβ $\lor$ ∃x¬α)

MP twice, Taut, 10, 2  (11) ¬¬∀xβ (the tautology is CANNpNqCqNNp)

MP Taut, 11 (12) ∀xβ (the tautology is CNNpp)

axiom 2     (13) ∀xα→α[x/t]

MP, 13, 12  (14) β

DT 2-14      (15) ((∃x)α→β)
  • $\begingroup$ I think there is a mistake : the proviso of the (to be verified) rule is : in the assumption $\alpha \rightarrow \beta$, $x$ is not free in $\beta$ ... but it may be free in $\alpha$. In your step 3, you applied axiom n°4 in the form : $(\alpha \rightarrow \beta) \rightarrow \forall x(\alpha \rightarrow \beta)$ and this needs that $x$ is not free in $\alpha \rightarrow \beta$. $\endgroup$ May 5, 2014 at 6:10

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.