The button will add this page to my log of things to fix. Use it for broken links, equations not rendering correctly, etc. Submit other issues on GitHub.
Soundness Theorem
Let be a set of formulae in a first-order language and be a formula in
If then
Proof (NONEXAMINABLE)
By induction on the length of a proof of from
In the case is , there is a subset s.t. doesn’t occur free in , and . Then by induction
Since does not occur free in , we have and so