1/29/08 10Software Under construction
Skills to be acquired in this tutorial:
To become familiar with the new rules for predicate logic trees with identity.
Tutorial:
It is possible to use trees with formulas containing identity. Two new rules are needed.
With identity, at a rough and hand-waving level, two different things might go on. First, everything is identical to itself ie a=a, b=b, c=c, etc.,in sum (x)(x=x). Then, identities are used to substitute for one term in another, so, for example, Fa and a=b allow the inference to Fb. Building these into tree rules is awkward in both cases.
To cover the first, there is an Identity Introduction rule which grows a tree by adding (x)(x=x) (in turn, this is almost always followed by Universal Decomposition, the tree counterpart of Universal Instantiation, to get a=a or m=m or a formula saying that a term is identical to itself, for some desired term). Identity Introduction is at stress with the general tree approach which is decompositional ie it takes things apart. [There are other ways to address this first feature of identity, but all of them have their inelegancies.] To use Identity Introduction, a formula is selected and then 'Identity Introduction' from the menu. From a logical point of view, there is no need to select a formula. However, when extending a tree, the User may have several open branches, and wish to have the identity in one branch and not the others-- selecting a formula picks that branch. Here are 3 examples of Indentity Introduction in use. The (valid) example argument is
a=b∴ (a=a.b=a)
and the tree for it starts
now, Identity Introduction could be used immediately to give
or the ~.D tree rule could have been used first, and then Identity Introduction used on the left branch
or on the right branch
[We will see which of these are useful, shortly.]
The second identity rule is the one that allows substitutions. It also is unusual in that it requires two formulas before it can be used (all the other tree rules decompose one formula, apart from Identity Introduction, which extends from nothing). One of these two formulas needs to be an identity statement, and the other can be any statement containing one of the terms. Here is a suitable tree, with the two formulas selected. [To select two formulas, you mouse click on one, then command-click or clover-leaf click on the second.]
and what the rule allows you to do is to extend the tree by substituting for one or more of the terms in the 'any' statement. So, here is one growth
and another
and another
(which you do depends on the purposes at hand).
Now we can show how to close that first tree (for the valid argument a=b∴ (a=a.b=a))
There is a restriction to the substitution rule. Were the identity to contain variables, there could be problems with 'capturing' when a substitution is made. So, the terms in the identity must be variable free. So, an identity like a=b is fine, because both the terms are constants, so too is f(a)=h(c) because these complex terms do not contain any variables. On the other hand, a=x or f(x)= h cannot be used, because some of the terms contain variables. There is a label to describe terms of the desired kind. A closed term is either a constant or a complex (compound) term whose subterms are themselves closed terms. Then for the tree Identity Decomposition rule, the terms in the identity have to be closed terms.
Exercises to accompany Tree Tutorial 5
Exercise 1 (of 2):
Determine whether these arguments are valid (ie try to produce closed trees for them). [These three statements are known as the axioms for identity (reflexivity, symmetry, and transitivity).]
a) ∴(x)(x=x)
b) ∴(x)(y)(x=y ⊃y=x)
c) ∴(x)(y)(z)((x=y).(y=z) ⊃y=z)
Exercise 2 (of 2):
Determine whether these arguments are valid (ie try to produce closed trees for them)
d) (x)Fxx,(∃x)(∃y)~Fxy ∴ (∃x)~(x=a)
e) (x)(Fxc⊃x=a), ~c=a ∴ (x)(~x=c)
f) (x)(x=a⊃Gxb), ~(∃x)Gxx∴ ~a=b