7.2.3 Forigo de ekzistokvantoro

Eltiri ion certan el $\exists xPx$ iom kostas, sed oni agas tiel:

$$\begin{fitch*} \par m & \exists x A \\ \par n & \fh A\{a/x\}... ... \par \hline \par & B & E$\exists$\ m,n,p,a \par \end{fitch*}$$

Do, se unu el la pluraj $A$ entenas $B$, tiam oni scias ke $B$, ĉar ja konas ke unu el la $A$ certas. Laŭ teknikaj teorioj, ne rajtas aperi iun $a$ ĉe $B$ nek ĉe iu atingebla hipotezo.