| ||||||||||||||||||||||||||||||
Tableau rules for identity
We are now ready to introduce some new tableau rules to deal with "x=y". We have two new rules for extending a tableau.
|
The left hand rule
|
The right hand rule
|
where the designator D occurs in j, and y is the result of replacing one or more occurrence of D in j by E.
Notice that in each case y says the same about E as j says about D. So the rationale for the rules is that, if D is one and the same thing as E, whatever is true of D is true of E. (This is sometimes called "Leibniz's law".)
We also have a new rule for closing a branch: any branch which contains (as a complete line) something of the form "¬D=D" closes. The rationale for this is obvious: since everything is the same as itself, "¬a=a" cannot be true – at any rate if "a" names something, which we are assuming it does.
Example: we will show that |-"x"y[x=y®y=x]:
| ü¬"x"y[x=y®y=x] ü$x¬"y[x=y®y=x] ü¬"y[a=y®y=a] ü$y¬[a=y®y=a] ü¬[a=b®b=a] a=b ¬b=a ¬b=b |
Notice three things.
1. We got "¬b=b" by using the left hand rule, "a=b" being our "D=E" and "¬b=a" being our "j". We could equally well have got "¬a=a" by using the right hand rule.
2. We could not close the branch until we had got "¬b=b", since "b=a" is not the same formula as "a=b"; so the other closure rule, which allows us to close a branch containing j and ¬j, did not apply.
3. We didn't tick either "a=b" or "¬b=a" when we used them to get "¬b=b". This is because in principle formulae like "a=b" can be used in more than one application of an identity rule, and likewise the "j" of the identity rules can figure in more than one application. So these rules, like the ""xj" rule do not give rise to ticking.
Another example: $x"y[x=y«Cy]|-$x[CxÙ"y[Cy®y=x]]
(You will recognise these two formulae as alternative ways of formalising "there is exactly one C.")
|
Comments:
We have not bothered with ticking in this tableau.
Line 3: from 1 by $xj rule
Line 4: from 2 by ¬$xj rule
Line 5: from 4 by "xj rule
Line 6: from 3 by "xj rule. This is the line which is going to tell us that Ca.
Lines 7 and 8: from 6 by [j«y] rule. The right branch closes, and we have indeed got "Ca" (and the uninformative "a=a").
Line 9: from 5 by the ¬[jÙy] rule.
Line 10: from 9 by the ¬"xj rule
Line11: from 10 by the $xj rule. Notice we had to use a new designator.
Lines 12 and 13: from 11 by the ¬[j®y] rule.
Line 14: from 3 by the "xj rule. Notice this is the second time we have used 3.
Lines 15 and 16: from 14 by the [j«y] rule.
Line 17: from 15 and 13 by the left hand identity rule.
 |
Print this page |
