I have been examining the tool of proof by contradiction.
$\Gamma\vdash\lnot\varphi$ iff $\Gamma\cup\{\varphi\}$ is inconsistent.
This is a very natural tool, and makes sense for closed formulas $\varphi\in\mathit{Sent}_L$ , but it does not seem to work for general formulas; for example, $\{\lnot\forall x \forall y(x=y), x=y\}$ is inconsistent (a simple use of generalization gives us a deduction), while $\{\lnot\forall x \forall y(x=y)\}\not\vdash x\not=y$ (we can prove this using the soundness of first-order logic). From what I have seen, this might be because the proof of the relevant direction uses the deduction theorem, which only works for closed formulas. Am I correct in my reasoning? Is this rule just irrelevant for non-closed formulas?
I think you are using the notation $\Gamma \vdash \alpha$ to mean that formula $\alpha$ is a consequence of the formulas in the context $\Gamma$.
If you allow the context $\Gamma$ to include formulas with free variables, then you need to decide how to interpret those free variables. You are interpreting them as universally quantified in your example, so that you read $\{\lnot\forall x \forall y(x=y), x=y\}$ as equivalent to $\{\lnot\forall x \forall y(x=y), \forall x \forall y(x=y)\}$ and hence derive a contradiction. Some authors also allow formulas with free variables in contexts but interpret them as existentially closed, so they wouldn't get a contradiction. I think it is safest to bypass this by disallowing free variables in contexts.