# Question 1b (Exam Paper - 2018-02-14) : Sequent Calculus

In the below example, why did it break d<->a first and then !b|c?

According to operator precedence, | has higher precedence then <-> +1 vote

The operator precedence does not matter here. Operator precedence matters if you would consider a formula like a|b<->d which is to be read as (a|b)<->d since the disjunction has a higher precedence.

In sequents, we have however sets of formulas on the left and right hand sides (and not just single formulas). So, you have in the example a set with two formulas !b|c and d<->a. It does not matter which one you consider for the next decomposition, any ordering will be correct. In general, it does matter however if you want to generate as few goals as possible. Note that some operators enforce a splitting into two new subgoals while others only generate a single subgoal. To reduce the effort, it would be better to prefer the latter, but for correctness, it does not matter at all.
by (143k points)
selected by