How is $\exists$ formulated in a FOL proof system?

Question

$\exists x \phi(x)$ in mathematics means there is something $c$, s.t. $\phi(c)$ holds. What is the formulation of that same idea as a inference rule, an axiom, or something else in a proof system in FOL?

Particularly what is the elimination rule for $\exists$? (It is not correct that if $\Phi \vdash \exists x \phi$, there exists a term $t$ so $\Phi \vdash \phi[t/x]$.)

What is the similar one for $\forall$?

Answer 1

In the Natural Deduction proof system we have a pair of inference rules for the existential (as well as the universal) quantifier:

$(\exists \text I) \ \varphi [x/a] \vdash \exists x \varphi$

$(\exists \text E) \ \text { if } \Gamma \vdash \exists x \varphi \text { and } \Delta, \varphi [x/a] \vdash \psi, \text { then } \Gamma, \Delta \vdash \psi$.

In an Hilbert-style proof system we have at least one axiom for it, unless it is defined in terms of the universal one.

See e.g. J. Shoenfield, Mathematical Logic for the axiom

$A[x/a] \to \exists x A$

and the rule:

$\dfrac {A \to B}{\exists x A \to B}$, provided that $x$ is not free in $B$.

In Enderton's system (see page 78) the existential quantifier is an abbreviation: $∃x α$ abbreviates $(¬∀x(¬α))$.

Answer 2

There are different ways to introduce $\exists$ in a FOL proof system.

I think the most common approach is that $\exists$ is defined via $\forall$:

$$\exists x \phi(x) \stackrel{\text{def}}\iff \lnot\forall x \lnot \phi(x).$$

And $\forall$ is introduced axiomatically before that.