Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

769 questions

886 answers

1.3k comments

424 users

0 votes

Hello ,

Why is the last second leaf node wrong? why is it - " b yields a " and not " empty set yields b,a"?

Thanks.

in # Study-Organisation (Bachelor) by (290 points)

1 Answer

0 votes

You need to understand the meaning of sequents: The semantics of a sequent {g1,...,gm} |- {d1,...,dn} is the semantics of the formula g1 & ... & gm -> d1 | ... | dn. Recall also the special cases of an empty conjunction, which is true and an empty disjunction which is false. Hence, {} |- {d1,...,dn} means true -> d1 | ... | dn, i.e., d1 | ... | dn, and {g1,...,gm} |- {} means g1 & ... & gm -> false, i.e., !(g1 & ... & gm).

The rules of the sequent calculus just perform equivalent transformations such that the root sequent of a proof tree is equivalent to the conjunction of the leaf sequents.

So, if you construct a proof tree for {} |- {(c->b)->a}, you are transforming the formula (c->b)->a itself, and when you get the leaf sequents {}|-{a,c} and {b}|-{a} it means that  (c->b)->a is equivalent to (a|c) & (!b|a). 

If you construct a proof tree for {(c->b)->a} |- {}, you are transforming the formula !((c->b)->a), and when you get the leaf sequents {c}|-{b} and {a}|-{} it means that !((c->b)->a) is equivalent to (!c|b) & (!a).

The two proof trees are as follows (you mixed them up!):

Moreover, a root sequent is valid if and only if all leaf sequents are valid. In other words, it is not valid if one of its leaf sequents is not valid, and the counterexample of that leaf sequent is then also a counterexample to the root sequent.

by (117k points)
Thank you for your answer!
In the second proof tree (with equation on the right hand side of yields-validity proof) , how is the last node (second leaf) is "b |- a" ?

According to me it should be " { } |- b,a " (much similar to the " |- a, c" )
Ah, your question is about sequent calculus rules for the implication. Remember that a->b is an abbreviation of !a|b so that we get the rules from this definition. As you can see with the proof trees above {} |- {c->b} becomes {c} |- {b} and {c->b} |- {} becomes {} |- {c} and  {b} |- {}.
As a short addition, I think this confusion is based on the fact that there is an error on the exercise slides of sheet 1, which state that "a->b" on the left side of a |- symbol should be reduced to "SPLIT({} |- a, {} |- b)" which is of course wrong and should be "SPLIT({} |- a, b |- {})" instead.
Imprint | Privacy Policy
...