Soundness for arbitrary set signatures

Assumptions in $T$ are true at every assignment by the hypothesis and coincidence. Boolean tautologies are true under the Boolean values of their constituent formulas. Reflexivity is true because a term's value equals itself. For equality substitution, if $s_0=t_0$ is true, their denotations agree; updating $x$ with either value gives the same assignment, so F2 gives equal truth values for the two substituted formulas. Thus its implication is true.

Universal instantiation is true: the universal truth clause includes the particular value $\mathrm{⟦}t{\mathrm{⟧}}_s$, and F2 identifies the instance. Existential introduction is true: a true instance supplies precisely that value as a witness by F2. For distribution, if $\mathrm{\forall }x(\alpha \to \beta )$ and $\alpha$ are true at $s$, then $\alpha$ stays true at every $s[x:=a]$ because $x$ is not free in it. The universal premise gives $\beta$ at each such assignment, hence $\mathrm{\forall }x\beta$ at $s$.

Induct on proof lines with the invariant “true under every assignment in $M$.” MP preserves this invariant by the implication truth table. For generalization, the invariant for its premise holds at each $s[x:=a]$, so its universal conclusion holds at $s$.

For existential elimination, suppose $M,s\models \mathrm{\exists }x\alpha$. Take one witness $a$. The invariant for the earlier implication $\alpha \to \beta$ applies at $s[x:=a]$, giving $\beta$ there. Since the rule requires $x$ absent from $\mathrm{FV}(\beta )$, F3 gives $\beta$ at $s$. If the existential antecedent is false the conclusion is true by its Boolean clause. This verifies the third rule and finishes the induction.

Thus the last line is true at every assignment in every model of $T$, exactly F4. No such model satisfies $\mathrm{\perp }=\mathrm{\exists }{v}_0\mathrm{\neg }(v_0=v_0)$, because every candidate witness equals itself. A proof of $\mathrm{\perp }$ would contradict the established invariant, so any theory with a model is consistent. Only one witness was used for one implication in step 3.1; no family of witnesses or AC is required.