In proof by contradiction, we assume a statement S is false, and thus $\lnot S$ is true, and then show $\lnot S$ implies some contradiction. This is normally show in the predicate logic as $( T \cup \lnot S \vdash \bot ) \to (T \vdash S)$, where T is any first order theory and $\bot$ is a contradiction. My question is related to the truth value of $\lnot S$. There could exist some model where in $(T \cup \lnot S)$ $\lnot S$ is false, there is a valid sequence of steps to $\bot$, and $\bot$ is true. In fact, $\lnot S$ could be false in all models.
Is it a requirement for a proof by contradiction that the added statement $\lnot S$ must also be true in all models for the proof by contradiction to be valid and sound?
If we can add a false statement, how does one prove $\bot$ when we can never show the proof is sound (for all models)?
(i) Here are two theorems of (classical) first order logic: $\bot\to S$ and $(\lnot S\to S)\to S$ [note, this is the law of excluded middle]. We have $T,\lnot S\vdash\bot$, but also $T,\lnot S\vdash\bot\to S$, so by modus ponens (MP) we have $T,\lnot S\vdash S$. By the deduction theorem, $T\vdash \lnot S\to S$. Now, $T\vdash (\lnot S\to S)\to S$, so by MP, $T\vdash S$.
(ii) By the completeness theorem, a theory is consistent iff it has a model. That is, a theory is inconsistent (derives $\bot$) iff it has no models. Thus $\bot$ has no models. (And thus (ii) is vacuously true if $T$ is inconsistent.)
Let $M\models T$.
Suppose that $M\models \lnot S$. By (i), $T\vdash S$, so $M\models S$. Thus $M\models (S\land\lnot S)$, and so $M\models \bot$. But there is no such $M$ — contradiction. So $M$ is not a model of $\lnot S$.
Every model of the same signature as $T$ is either a model of $S$ or a model of $\lnot S$.
By excluded middle, $M$ is a model of $S$.