Existential introduction - required or not?

Question

Consider a theory $T$ in first order logic, and a formula $C$. If there exist a proof of $C$, and that all formulas in $T$ and $C$, none of them contains $\exists$.

The question is: does there always exist a proof of $C$ that do not invoke $\exists$ introduction?

My intuition say no. I constructed some formulas as follow:

$\neg\forall xP(x)$

$\forall x(\neg P(x)\rightarrow\neg Q(x))$

as the theory. And the conclusion is $\neg\forall Q(x)$.

It seems intuitive that you can't avoid getting $\exists x\neg P(x)$ somewhere in the proof. But I can't quite prove that all proof will have something like that sentence, or otherwise use $\exists$ introduction somewhere.

Hope someone can help with this. Thank you for your help.

Answer 1

I'm not sure to understand the statement of your problem; so I try to interpret it as :

Consider a theory $T$ in first order logic, and a formula $C$ such that all formulae in $T$ nor $C$ contain $\exists$. Does always exist a proof of $C$ from $T$ that do not invoke $∃$-introduction?

I do not know if you are considering specifically natural deduction, but - in general - we can have a proof system for first-order logic (see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)) which use only $\forall$ as primitive (obviously : $\exists$ is defined as an abbrevation for $\lnot \forall \lnot$).

A system like Enderton's is sound and complete for validity.

Thus if we have : $\Gamma \vdash \alpha$, where no formula in $\Gamma$ nor $\alpha$ contain $\exists$, we have that the proof does not need logical axioms or inference rules with $\exists$, simply because there are none in the system.

---

Regarding your example, we can prove it as follows, using axiom :

$\forall x \alpha \rightarrow \alpha(x/t)$, where $t$ is substitutable for $x$ in $\alpha$ [see Enderton, page 112]

and some tautological equivalences.

Proof

(1) $\forall x (\lnot P(x) \rightarrow \lnot Q(x))$ --- assumed

(2) $\lnot \forall x P(x)$ --- assumed

(3) $\lnot P(x) \rightarrow \lnot Q(x)$ --- from (1) and axiom, by mp

(4) $Q(x) \rightarrow P(x)$ --- from (3) by contraposition

(5) $\forall x Q(x)$ --- "temporary" assumption

(6) $Q(x)$ --- from (5) and axiom, by mp

(7) $P(x)$ --- from (4) and (6) by mp

(8) $\forall x P(x)$ --- from (7) by Generalization Th [see Enderton, page 117 : $x$ is not free in the assumptions].

But (2) and (8) are contradictory; thus by Reductio Ad Absurdum [see Enderton, page 119] :

(9) $\lnot \forall x Q(x)$ --- "discharging" assumption (5).