Definition talk:Tableau Extension Rules

Are the last parts of iff and exclusive or correct? It seems like they should be children of the listed objects and grandchildren of the original formulas. --Cynic (talk) 23:03, 12 July 2009 (UTC)

I think they are. Two WFFs on the same branch are "and", two children of the same node are "or".

So the Iff one is:

A and not A are both children of t. That is, both A and not A are possible consequences of the node t which is a direct consequence of A iff B.

But given A, it also has to follow that B is a consequence of A iff B. Hence A and B occur on the same branch of t.

On the other hand, given not A, it has to follow that not B is a consequence of A iff B. Hence not A and not B occur on the same branch of t.

Similarly for Exclusive Or.

The drawings are supposed to show:

t is a descendant of A iff B.

A and not A are direct children of t.

B is a direct child of A (and so a grandchild of t).

not B is a direct child of not B (and so a grandchild of t).

The drawings are not clear because I'm limited in the graphics capability of the tool I'm using.

--Matt Westwood 23:12, 12 July 2009 (UTC)

"Iff: If $t$ has an ancestor $\mathbf A \iff \mathbf B$, extend $T_k$ by adding two children $\mathbf A$ and $\neg \mathbf A$ of $t$, a child $\mathbf B$ of $\mathbf A$ and a grandchild $\neg \mathbf B$ of $\neg \mathbf A$."

But aren't you saying that you add a child $\neg \mathbf B$ of $\neg \mathbf A$? --Cynic (talk) 02:06, 13 July 2009 (UTC)

Aah, gotcha. Fixed it. --Matt Westwood 11:29, 13 July 2009 (UTC)