Your first case is correct. I think you're on the right path with the second case, but I don't believe it is that issatisfied. We say thatsatisfiesormodelsoris a model ofthe formula on the RHS of the turnstile. Furthermore, satisfiability is asemanticconcept, and your proof, as you've written with the single-turnstile, is a proof aboutprovability. I think you should keep to the syntactical proof theory in your proof.

I would approach the problem from this perspective. Ask yourself, what happens when our set of sentences proves G? (i.e., ) Since our assumption is that is consistent, and it is precisely so because of the removal of G, I think the answer to that question will provide your solution: it eliminates the case of proving G and leaves us with only one other option, i.e., that it proves ¬G. Do you see why?