Sequent Calculus

Question

Does the operator precedence play a role in which operator to consider at the particular step in the tree in sequent calculus? 

I have attached an image below of a solution in a past paper, which performs a split on <-> operator on the 5th node. But when I worked it out, I performed the split on the OR operator (|) at that step. Which gave me the same leaf nodes finally, but they were on different branches, is that okay?? I am also attaching my solution (worked out from 5th node) to this question. 

 

My solution: 

Answer 1

Well, two things have to be mentioned in the answer: First of all, the precedence matters, of course, since if we have a formula like p|q&r, then we first have to decompose the disjunction before the conjunctions. Otherwise, we consider a different formula, and clearly, may get different results.

Your doubt is however less critical. You are essentially wondering how to decompose an equivalence like p<->q which can be replaced either with p&q|!p&!q or (!p|q)&(p|!q), i.e., by a DNF or a CNF. All of these formulas are equivalent to each other, and therefore it does not matter which one you choose for the definition of a "syntactic sugar" operator. Once that is done, however, precedence matters!

Comments

Thanks for your answer.
I am not wondering how to decompose <-> operator. I am asking if it matters which operator I choose to create the child nodes on. Since at the same level I have an OR operator and an <-> operator in the format (!b |c), d<->a , does it matter if I choose to split on "|" or "<->" ??
So is it still correct if I choose to perform the split on the OR operator first and then the <-> operator in this case?

---

Okay, I see. You are wondering about the decomposition order of the different formulas in the sequent. For the final result, this order does not matter, but the proof trees will look different. You should get the full points for any correct proof tree, don't worry about this. However, choose those formulas first that don't provoke a split, since that is more efficient.

---

Thanks! Got it