7.2.2 Introducció de l'existencial

Si veiem una prova de la seva existència, podem dir que una propietat es compleix per algun element:

$$\begin{fitch*} \par n & A\{t/x\} \\ \par \hline \par & \exists x A & I$\exists$\ n,t \par \end{fitch*}$$

Això de $A\{ t/x\}$ és una substitució (es llegeix ``$t$ sobre $x$'' i consisteix en canviar $x$ per $t$).

Aquesta regla diu que si veiem $At$, on $t$ és un element, podem dir que $\exists xAx$, perquè sabem que quan $x$ és $t$ sí que es compleix.