Alright, that makes sense (if my reading of proofs seems uncharitable at times, it is because I know enough about logic to know when a statement doesn't make sense, but I don't know enough to tell what the statement wants to be).

Soundness seems like an interesting property to think about for a formal system. I am reminded of the bizarre systems you can get, e.g., by taking PA and adding the axiom "PA is inconsistent". This, if I recall correctly, is consistent provided PA itself is consistent, but (whether or not it's consistent) it definitely can't be sound.