Adding one fresh witness preserves consistency

Write $E=\mathrm{\exists }x\varphi$ and $h=(E\to \varphi [c\mathrm{/}x])$, a sentence by the free-variable restriction in F1. If $T\cup \{h\}⊢\mathrm{\perp }$, deduction and $\mathrm{\neg }\mathrm{\perp }$ give $T⊢\mathrm{\neg }h$. The Boolean implications $\mathrm{\neg }(A\to B)\to A$ and $\mathrm{\neg }(A\to B)\to \mathrm{\neg }B$ then yield proofs from $T$ of $E$ and $\mathrm{\neg }\varphi [c\mathrm{/}x]$.

Apply fresh-constant replacement to the latter finite proof, choosing $z$ absent also from $\varphi$, $x$ and $\mathrm{\perp }$. The result is $T⊢\mathrm{\neg }\varphi [z\mathrm{/}x]$. This substitution identity follows because $c$ was absent from $\varphi$ and $z$ is unbound there. Boolean explosion gives $T⊢\varphi [z\mathrm{/}x]\to \mathrm{\perp }$. Eliminate $z$ to obtain $T⊢\mathrm{\exists }z\varphi [z\mathrm{/}x]\to \mathrm{\perp }$; $\mathrm{\perp }$ is a sentence, so the rule's restriction holds.

Fresh-variable existential renaming gives $T⊢E\to \mathrm{\exists }z\varphi [z\mathrm{/}x]$. Together with the proof of $E$ and step 2.1, MP yields $T⊢\mathrm{\perp }$ in the pure constant expansion. Conservativity removes that expansion, contradicting the given consistency of $T$. Therefore the witness extension is consistent. The same conservativity statement, without adding any sentence axiom, proves the seed-constant assertion.