Putting it all together

Definition 8.4 (Closure). We call a branch of a tree closed provided there are some

$\mathcal{L}_1$formulas of form

$Y$,

$\neg Y$occurring on it. We call a tree closed if all its branches are closed.

Then, we can define what syntactic entailment means in first-order logic.

Definition 8.5 (Syntactic entailment). Let

$A=\{X_1, X_2, …\}$be any set of formulas and let

$Y$be any formula of

$\mathcal{L}_1$. Then, the set of premises

$A$syntactically entails

$Y$, or

$Y$is a syntactic consequence of

$A$(in first-order logic), iff there is a closed tree with

$\neg Y$at its origin, where each occurrence of a formula on the tree except

$\neg Y$is derived using one of the following rules:

1. the rules

   $\neg\neg$,

   $\wedge$,

   $\neg \vee$,

   $\neg \rightarrow$;

2. the rules

   $\vee$,

   $\neg \wedge$,

   $\rightarrow$;

3. the rules

   $\forall$,

   $\exists$,

   $\neg \forall$,

   $\neg \exists$;

4. the premise rule Pr (using

   $A$).

In such cases, we write

$A \vdash Y$, and call the closed tree a proof of

$Y$from the premise set (or simply, premises)

$A$. If no occurrence of a formula on the tree was introduced using the rule Pr, we say

$Y$is a theorem of first-order logic.