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.