Deduction of $\vdash \forall x \phi \rightarrow \exists x \phi$

Question

I can show that $\forall x \phi \vdash \exists x \phi$ through a direct deduction as follows, using axioms as defined in Enderton

1. $(\forall x) \phi$ by hypothesis.

2. $ (\forall x) \phi \rightarrow \phi$, Axiom.

3. $ \phi$, modus ponens on lines 1 and 2.

4. $(\forall x)\neg \phi \rightarrow \neg \phi$, Axiom.

   5. $ ((\forall x) \neg \phi \rightarrow \neg \phi )\rightarrow ( \phi \rightarrow (\exists x) \phi)$, Axiom (tautology).

   6. $ \phi \rightarrow (\exists x) \phi$, modus ponens on lines 4 and 5.

   7. $(\exists x) \phi$, modus ponens on lines 3 and 6.

However, at this point, I now need to invoke the deduction theorem in order to conclude that $\vdash \forall x \phi \rightarrow \exists x \phi$. I want to avoid metalogical results and be purely syntactic. I know that you can prove the deduction theorem through a direct deduction, but I'm wondering how I can adjust my specific proof directly to get the result through just axioms and modus ponens.

I think that if I can show $\vdash \forall \phi \rightarrow ( \phi \rightarrow (\exists x) \phi)$, I could apply the $T$ rule. But I'm not sure. Help appreciated.

Answer 1

The "trick" to get rid of the Deduction Th is to prefix (in a suitable way) the assumption that you want to "discharge" with DT to the steps in the derivation; see Stephen Cole Kleene, Mathematical logic, Dover (1967), page 40.

But in the present case, the needed derivation is quite straightforward:

1) $\vdash (∀x)ϕ→ϕ$ , Axiom.

2) $\vdash (∀x)¬ϕ→¬ϕ$ , Axiom.

3) $\vdash (∀x)¬ϕ→¬ϕ)→(ϕ→(∃x)ϕ)$ , Axiom (tautology).

4) $\vdash ϕ→(∃x)ϕ$ , modus ponens on lines 2 and 3.

With a suitable instance of the Axiom (tautology) :

5) $\vdash (p \to q) \to ((q \to r) \to (p \to r))$

6) $\vdash (∀x)ϕ → (∃x)ϕ$ , modus ponens twice on lines 1, 4 and 5.

---

Note

In Enderton's system this formula is valid because the semantics for FOL used is the "traditional" one, with nonempty domain $D$.

This is consistent with the fact that in Free Logic and Inclusive Logic, i.e. logics cosistent with the assumption that $D$ may be empty, the schema:

$∀xA → A$,

is not valid