6.3.3. Derivations for identity

We are now in a position to state the derivation rules for identity that will be part of our basic system. We will have four rules for closing gaps. Each of them extends one of the rules QED and Nc, with each of those rules being extended in two ways. One sort of extension is based on the law for co-aliases alone and the other also rests on the law of congruence for predicates.

The first pair of extensions of QED and Nc—Equated Co-aliases (EC) and Distinguished Co-aliases (DC)—are shown in Figures 6.3.3-1 and 6.3.3-2.

The bracketed remark concerning τ and υ stipulates that there be enough equations among the available resources to make the terms τ and υ co-aliases. The law for aliases then tells us that the resources entail the equation τ = υ. So, if this equation is our goal, we may count the gap closed; and, if its denial is among our resources, we have the inconsistency required to close the gap of a reductio argument. An important special case of these rules is one where τ and υ are the same term. In this case, τ = υ is τ = τ (which is also υ = υ) and, since a term is a co-alias of itself with respect to any set—even with respect to a set in which it does not appear—any gap with a self-equation as its goal may be closed, as may the gap of a reductio argument with a negated self-equation among its resources. Notice that the general form of these rules differs from the special case for self-equations only by exchanging terms that are co-aliases.

Some abbreviated terminology will help in stating the second pair of rules for identity. Let us say that two series of terms τ₁…τ_n and υ₁…υ_n are co-alias series when they have the same length and their corresponding members are co-aliases—that is, when τ_i and υ_i are co-aliases for each i from 1 to n, where n is the length of the two series. Then the second pair of rules for identity are shown in Figures 6.3.3-3 and 6.3.3-4. These are Quod Erat Demonstrandum Given Equations (QED=) and Non-contradiction Given Equations (Nc=).

Here a bracketed remark stipulates that the available resources contain enough equations to make corresponding component terms of Pτ₁…τ_n and Pυ₁…υ_n co-aliases and thus to entail identities between these terms. The law of congruence for P then tells us that Pυ₁…υ_n is entailed by available resources. If it is our goal, we may close the gap, and we may do so also if the gap is in a reductio argument and our resources contain its denial ¬ Pυ₁…υ_n.

The sentences Pτ₁…τ_n and Pυ₁…υ_n that figure in the last two rules have been described as applications of the same predicate whose corresponding component terms are co-aliases. A little thought will show that we can describe such expressions equally well as atomic sentences that differ only by components that are co-aliases. This makes the similarity of this rule to QED and Nc a little more apparent. Instead of saying that we can close a gap when our goal is among our resources and when one resource negates another (as we do in QED and Nc), we say here that we can close a gap if a resource differs from the goal or from the negation of another resource only by co-aliases. This way of describing these rules leads to the question whether we really need to limit them to predications. The answer is that we do not although that is the only case where we really need to use the rule.

Other rules can be extended in the way QED and Nc are extended in QED= and Nc=: if the illustration of the rule displays two occurrences of a sentence, these may be sentences that are different but that differ only by terms that are co-aliases given the available resources. (As was noted above, even our first two rules for identity could be seen as the result of extending in this way rules that say that we can close a gap whose goal is a self-equation and a reductio gap whose resources contain the denial of a self-equation.) When a rule is extended in this way, its label should be followed by the equals sign, as in the labels for QED= and Nc=. We will call the result an extension of the rule for equations; and, as with QED= and Nc=, the equals sign added to the name may be read given equations.

Below are two derivations that illustrate these ideas and also show how we will keep track of co-aliases.

The first derivation uses the rule of Figure 6.3.3-3 to close the gap after stage 2. The second uses an extended version of modus ponens; the resource Rc(fa) and the antecedent of Rcc → Gc differ only by terms (fa and c) that are co-aliases given the equations fa = b and b = c. (If the extended form of modus ponens was not used in the second derivation, we would need to set up an indirect proof to reach the goal Qc and exploit Rcc → Qc using the rule RC for exploiting conditionals in reductio arguments. Both gaps of the derivation would then close using the identity rules for closing gaps.) At each stage when an equation is added to the resources, the resulting alias sets are indicated at the right. This is done by listing the members of each alias set with dashes between, further delimiting the different alias sets by commas. This may be written to the right of the last equation added at a given stage. There is no need record the alias sets until the first stage when an equation appears as a resource since up to that point each term is in an alias set by itself.

The point of listing alias sets to the right of equations is to sum up the co-aliases at at each stage when they change. Although it is usually by adding equations that the alias sets will change, this is not the only possible way. When a term is added, either in a new resource or in a new goal, it must be accommodated in the co-alias sets. Although new terms will be introduced regularly in later chapters, they could be introduced now only if attachment rules or the rule LFR were used to introduce sentences that are not already components of sentences in the derivation. Since that is not a use of such rules that we have been considering, we will not consider examples, but a general guideline for listing alias sets can be stated that will include such cases: at the initial stage of a derivation if it has equations as resources and at any stage thereafter at which the alias sets of a gap have changed, list the alias sets at the right near the top of the gap. When several resources are added, the alias sets can be added after the last new resource that figures in the change. If no new resources are added (and the alias sets change only because of vocabulary added in a new goal), the alias sets may be listed at the right of the top of the scope line of the gap.

It is sometimes useful to be able to enter an equation between co-aliases as a further resource. Since this does not change the alias sets, it does bring a gap near an end and it is not automatically progressive. Therefore, we will count it as an attachment rule. We will call this rule Co-alias equation (CE):

Equations are never exploited, so the X at the right does not mark the added equation as already exploited; instead it indicates that the equation leads to no change in the alias sets since its component terms are already co-aliases. Since any use of such an equation to close a gap is already covered by other rules, this rule will serve primarily to provide auxiliary resources for detachment rules (and available resources for use in other attachment rules). Here is a simple example.

In order to construct a derivation using only basic rules, we would need to resort to a reductio argument and the rule RC.

The rule CE is really only needed when no co-alias of the terms being equated appears as a term of an equation. The rule would not have been necessary in the example above if the conditional’s antecedent had been something like a = c ∧ b = b because this sentence could be added by the extended attachment rule Adj= since it differs from a conjunction of the first two premises only by co-aliases. In general, if our resources contain any equation between co-aliases of the terms that we want to join in the new equation, we have an equation differing from the one we want only by co-aliases and we can use the extended form of whatever rule we might apply to the new equation.

Finally, we will add an attachment rule that allows a resource to be added when it differs from an available resource only by co-aliases. Such resources can be represented as θτ₁…τ_n and θυ₁…υ_n where τ₁…τ_n and υ₁…υ_n are co-alias series. That is, it is understood that the differences between the resources are limited to the displayed series of terms so the resources amount to predications to the two series τ₁…τ_n and υ₁…υ_n of an abstract θ that takes the form [… x₁ … x_n …]_x1…xn, where x₁…x_n is a series of distinct variables with the same length as τ₁…τ_n and υ₁…υ_n. The name of the rule is Congruence (Cng).

The resource that is added by this rule is marked as exploited because any exploitation of the earlier resource will be enough to take account of it. The rule Cng offers the following alternative to an earlier derivation.

Notice that the ordinary form of MPP is used here rather than the extended form MPP= used earlier, and Cng can always be avoided by using the extended forms of other rules. The point of using Cng is only to add a step to a derivation that may make it easier to follow.