I’m studying for my first logic exam and have some questions regarding proof trees:
In the process of proving the satisfiability of a formula by a proof tree with sequent calculus, I need to close all the branches of the proof tree and can do so by closing it with a goal assumption (e.g. A, B, C ⊢ B) or with a contradictory assumption (e.g. A, B, ¬B ⊢ C). What I’m not really sure about is:
- Do goal assumptions and contradictory assumptions both indicate that a formula is satisfiable?
- E.g. if I have a proof tree with 3 branches – 2 closed by a contradictory assumptions and 1 one by a goal assumption – does this proof the formula to be satisfiable?
- And if I only have contradictory assumptions in my proof tree – is the formula satisfiable or not?
Thank's for any help in advance!