Repetition of formulas in nodes of Semantic Tableau

Question

I'm studying Propositional and First Order Logic and I have to practice with the Tableaux Method in order to check satisfiability of a formula.

I create new nodes of the tree by using the Completion Rules in a straightforward way, but I have a doubt about it.

Everytime I have a new node, I repeat some of the previous node's formulas. I make an example:

I have this block:

Is it legit to repeat the two "or" formulas again in the two new branches?

I rewrite them because in this way I don't forget to use them, it is only for my comfort.

Thanks in advance.

Answer 1

You have two options:

1. Either you do what you do, which is to copy all of the remaining statements into the branches below. The disadvantage of this is that you have to copy all those statements (i.e. it will be more work)

2. You don't copy the statements, but when you apply a tree rule on any of the remaining statements, you have to make sure to put the result in all of the branches under it. The disadvantage of this is that you have to be a bit more careful in making sure that indeed you do this.

So yes, what you do is fine, but not necessary, as long as you are careful!