Existential Instantiation/Proof System

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\LL$ be a specific signature for the language of predicate logic.

Let $\mathscr H$ be Hilbert proof system instance 1 for predicate logic.


Let $\map {\mathbf A} x, \mathbf B$ be WFFs of $\LL$.

Let $\FF$ be a collection of WFFs of $\LL$.


Let $c$ be an arbitrary constant symbol which is not in $\LL$.

Let $\LL'$ be the signature $\LL$ extended with the constant symbol $c$.


Suppose that we have the provable consequence (in $\LL'$):

$\FF, \map {\mathbf A} c \vdash_{\mathscr H} \mathbf B$

Then we may infer (in $\LL$):

$\FF, \exists x: \map {\mathbf A} x \vdash_{\mathscr H} \mathbf B$


Proof



Sources