I am trying to write the definition of a basis for a topological space as a subsidiary deduction rule. A collection $\beta$ of subsets of a set $X$ is a basis for a topology on $X$ if and only if $(\forall x \in X:\exists B \in \beta: x \in B) \wedge (\forall x \in X:\forall B_1 \in \beta:\forall B_2 \in \beta:x \in B_1 \cap B_2 \rightarrow \exists B_3 \in \beta:x \in B_3 \wedge B_3 \subset B_1 \cap B_2)$.
My question is that is it appropriate to write the former definition in the following form.
A collection $\beta$ of subsets of a set $X$ is a basis for a topology on $X$ if and only if $\vdash \forall x \in X:\exists B \in \beta: x \in B$ and $x \in X,B_1 \in \beta, B_2 \in \beta, x \in B_1 \cap B_2 \vdash \exists B_3 \in \beta:x \in B_3 \wedge B_3 \subset B_1 \cap B_2$?
My confusion is owing to the fact that the property of being a basis appears to be a semantic one (I am not sure) and given that, if it is appropriate to use $\vdash$ instead of $\vDash$. Secondly, since the subsidiary deductions are true contingently, depending on if $\beta$ is a basis or not, is it acceptable to use them. What would then be an appropriate way to write the definition in a metalanguage other than natural language?