The "old" and "new" Leibniz
Inference Rules

The REALLY old Leibniz rule we got by fixing up the rule on the first page of chapter 3 (with our new meaning for textual substn., and also both a weak and a strong form -- weak for inputs and outputs real theorems, -- strong for inputs and outputs temporary theorems). But what I mean here by "old" Leibniz is really the generalization of that inference rule to the case where one has not biconditional (i.e., boolean "equal") theorems as premise and conclusion, but "equality" theorems involving expressions P, Q, etc. of arbitrary syntactic type.

"Old" Leibniz

We just "fix" (1.5) on page 12:

Let  P  and  Q  be expressions of the same syntactic type, 
let the first  =  (below) be the equality symbol for that type, and
let  z  be a variable of that same type.

Let  E  be an expression of some type, and 
let the second  =  (below) be the equality symbol 
for the type of E.  Then we have the (weak) inference rule

                       |-  P = Q

                |-   E[z:=P] = E[z:=Q]    .

Actually, this just comes out of 3.83, discussed in class already,
and weak derived inference rule
Modus Ponens.  We also have the strong version of this Leibniz
inference rule, namely, the rule where all  |-'s  are replaced by
A |- 's, i.e. where both input and output are A-theorems rather
than real theorems -- which comes out of 3.83 and strong M.P.

Of course, this is just shorthand for "If P = Q is a theorem, then blah, blah...." I give an example or two at the bottom of this file. (The example given in the book below (1.5) is not a good one.)

Note that we could not even STATE this inference rule until just now, because we have only JUST defined textual substitution E[z:=P] in our logical system.

I believe we should really define "inference rules" and "theorems" at the same time, in an inductive definition of "theorem", as we did before in propositional logic. Thus, one should really list one's axioms -- these would be our earlier 12, plus all instances of axiom schemes (1.2) and (1.3) (and (1.4)? -- Transitivity of = -- I guess I phrased that as an axiom?) and 3.83, which we mentioned recently, plus all instances of the 12 (?) axiom schemes listed at the back of the book from chapters 8 and 9.

As before, we still have the house of boolean expressions (wffs, formulas) and the room of theorems inside that house.

Then our inference rules are:

-- Equanimity  (this looks just as it did before)

-- Transitivity (this looks as before, ch. 3)

--  Leibniz.

Leibniz includes all three inference rules described in this file as Leibniz.

And the inductive defn. of "theorem" is phrased just the way it was before, with our new understandings of "boolean expression/formula" and our new axioms and inference rules.

"New" Leibniz:

The reason why "old" Leibniz above is not good enough is explained pretty well in the book, in the example above (8.12), p. 148. Here is a simpler example:

If there is any Justice in the World, the following should be a theorem of our system of predicate logic:

(\forall x ¬¬ A(x) ) == (\forall x A(x) )

(Here, take x to be a variable of any nonboolean type, and take A to be a 1-place predicate letter.)

But this is not an instance of 3.12. (It is easy to see this, because neither side of the biconditional begins with a double negation.) It is a wff in which the two "sides" of an instance of 3.12 -- ¬¬A(x) == A(x) -- are both buried inside the same universal quantification. One might try to prove that the above is a theorem by an argument like the one below (but it does not work):

    |-  ¬¬A(x) == A(x)  , by 3.12.

Let  E  be the boolean expression  (\forall x| true: r). Then 
"old" Leibniz  ((1.5) above in this file)  gives that
|-  (\forall x| true:  r)[r:= ¬¬A(x)]  ==  

                    (\forall x| true:  r)[r:= A(x)] ,

i.e., that  (being lazy when the range is the boolean constant
true, and dropping the "true" and the | and the :)

  |-   (\forall w  ¬¬A(x) )  ==  (\forall z  A(x) ) .

(We are in case (iii) of the definition of contextual substitution 
here -- we are forced to introduce fresh variables in each
quantification.  We could have used "w" in both places, but
the above is also ok.)

So Leibniz gives the above theorem.
But this is not what we WANTED!  We wanted dummies x in both

To solve the problem of proving that such "valid formulas" 

-- (a wff is a valid formula if it interprets as T in all possible 
interpretations;  what we used to call tautologies are now
called valid formulas in predicate logic) --

are theorems,
we introduce the two "new" Leibniz inference rules (8.12), one for
replacing "equals" in ranges, one for replacing "equals" in bodies,
of quantified wffs:

(8.12)(i)  New Leibniz on ranges of quantifcns.:

Let  P,Q and z be two expressions and a variable, 
all of the same syntactic type.

Let  E  be boolean,  x  be an object variable, 
* be a quantifier of the same type as  S ,  
and  S  be an expression. Then

                      |-  P = Q

     |-   (*x| E[z:=P]: S)  =  (*x| E[z:=Q]: S)   .

(As usual, this is lazy shorthand 
for an English "if, then" statement.)

(8.12)(ii)  New Leibniz on bodies of quantifications:

Let  P, Q, z  be as before.

Let  *  be a quantifier and  x  be
a variable of the same syntactic type.

Let  R  be boolean, and  E  be an expression
of the same syntactic type as *.

               |-    R  ==>  (P = Q)

         |-   (*x| R: E[z:=P])  =  (*x| R: E[z:=Q]) .

The semantic justification here is: Suppose that in any
interpretation  (particular UD's, etc.)  in which R interprets
as T,   P = Q  also interprets as T.  Then  P, Q interpret as
the same element of the appropriate UD  (BOOL', or REAL', or
INTEGER', or RHINOCEROS' or whatever). But then for all x's for
which R holds, the two substituted E's above interpret as the
same "thing", so "combining" all such by means of operator *,
over all such "values" of x, results in "things" that are the same.

Main use of Leibniz on bodies:

Suppose we somehow already know that for certain expressions
P  and  Q ,  |-  P = Q .

Then for ANY wff R,  |-  R ==> (P = Q). 

(To see this, use 3.4, 3.7, derived Leibniz,  3.72
and 3.4 and Equanimity.)

So from the general Leibniz on bodies we get 
this special case, 

which is by far the most common use of this
inference rule:

                      |-    P = Q

     |-   (*x| R:  E[z:=P])  =  (*x| R:  E[z:=Q]) ,

for any range R. 

Strong Versions of 8.12: We give ourselves also two inference rules for A-theorems, namely, 8.12 (i) and (ii) with all |-'s replaced by A |- 's, i.e., with input and output both A-theorems. But now we only allow use of these inference rules if x dnof (does not occur freely) in A. The two examples below were given in class, to show the need for the restriction above, when using 8.12 for temporary theorems: (1) Let A be the predicate (i.e., boolean expression) x=2. Let * be \Sum, let E be z+1 , and let R be (x=3) \/ (x=4). If we did not have the restriction on 8.12 above, then we could do the following: Assume A . A |- A. So by 8.12(ii), with P being x and Q being 2, (\Sum x| (x=3) \/ (x=4): (x+1)) = (\Sum x| (x=3) \/ (x=4): (2+1)) is an A-theorem. Call this wff B . Then by the Deduction Theorem, |- (x=2) ==> B . But in the standard interp. of all the symbols here with the universe of discourse being the integers, and if we interpret the variable x as the real live integer 2, this "theorem" interprets as (2=2) ==> (3+1) + (4+1) = (2+1) + (2+1) i.e., as 2=2 ==> 9=6. Which is pretty dumb. It's F, in the standard interpretation. So there must be something bad in the above "proof". What is bad is the use of 8.12(ii). (2) Here is another example, given in class: If we could use 8.12(ii) with no restriction like the one in bold type above, then, after assuming x=2, we could get the temporary theorem (\forall x|: x=2) == (\forall x|: 2=2). (* now is the universal quantifier, P is x, Q is 2, E is z=2, R is true.) But in the standard interpretation when the universe of discourse is the set of all real numbers, this says "All real numbers are 2 if and only if 2 is 2." (The second quantification says "for all real numbers x, 2 is 2". But that is logically equivalent to saying "2 is 2".) And this conclusion is semantically unacceptable.

Semantic discussion: What is happening in these two examples is the following: An assumption is made involving a wff with a free occurrence of a variable x. Semantically this means we are restricting our attention to interpretations in which that assumption interprets as T. Later, after deducing an equality P=Q on the basis of our assumption, we then jammed P into one quantification with dummy x, and Q into another. Now, the equality came only under the assumption that we were in an interpretation in which A interpreted as T, i.e., in which x had a particular interp. that made A interpret as T. But now in the quantification, x typically varies over a range of "things" in the univ. of discourse, some of which might make P=Q interpret as F! These two examples show the need for the bold restriction if x d.n.o.f. in A, in the use of 8.12 for temporary theorems. Examples of the use of (1.5): Any use of Leibniz we made in chs. 3,4, i.e., in propositional logic. Another (not very interesting) example: |- p /\ (c = w) == p /\ (w = c). Proof: |- (c=w) == (w=c), because this is an instance of axiom scheme (1.3) (Symmetry of =), which we gave a few days ago, with P being the "constant symbol" c and Q being the variable w of the same type as c. Now apply (1.5) with E being p /\ z, and replacing z. I thought about putting 3 = 49 here instead of w = c , or u = 49. Those are ok too, except that one should have a reserved set of "constant symbols", for the language of predicate logic, something like lower case Latin letters near the front of the alphabet, plus subscripted ones to get an infinite supply: a, b, c, d, c_1, c_2, ...., c_17, .... (In |E, we had only TWO constant symbols: true, false.) But the book allows things like "3" and "49" as constant symbols too, and I guess we will follow their lead (partly because constant symbols like 43 may turn up on our final exam). Examples of the use of New Leibniz: -- Well, now the above 3.12 example works fine. More generally, we can now take ANY "equality" theorem (including our old friends, the biconditional theorems) and stick the two sides of it into any expression in the range/body of any quantification, and get new "equality" theorems. -- Here is a sort of weird example: Let P and Q be any two expressions of the same syntactic type. Then (*x| false: P) = (*x| false: Q) is a theorem. Reason: Let E be simply z. Then the above follows from 8.12(ii) for real theorems, (3.75), 3.4 and Equanimity. One also has tons of theorems of the form R ==> (P=Q) coming out of 3.83. Each of these gives potential theorems using 8.12(ii): |- (*x| e=f: E[z:=e]) = (*x| e=f: E[z:=f]) . For instance, we have the theorem (\Product i| (i+20) = (i \times i): (i+20)+5) = (\Product i| (i+20) = (i \times i): (i \times i)+5). To justify saying this is a theorem, YOU must be able, on a test, to identify this as 8.12(ii), with E being z, and with input the real theorem 3.83, with E being z+5. (You could also switch the two E's, here.) Don't try interpreting the above wff. It is quite stupid and boring. I did not have time to find a more interesting example. Actually, looking at these 3.83 examples makes me realize that 8.12 as stated in the book is rather stupid. If we have P=Q as (absolute or relative) theorem, and E is an expression, then 3.83 gives us E[z:=P] = E[z:=Q] as (permanent or temporary) theorem. So we could just call the left and right sides just above "P" and "Q", and then 8.12 simplifies considerably -- with these new guys in place of the original P, Q, now just take E in 8.12 to be z. Then we get |- P == Q ----------------------------- for 8.12(i) |- (*x| P: S) = (*x| Q: S) and (playing a similar game and using the inference rule "transitivity of arrow" derived from 3.82(a)) |- R ==> (P = Q) ------------------------------- for 8.12(ii) |- (*x| R: P) = (*x| R: Q) These rules are just as powerful as the original 8.12, thanks to the derived inference rules "Leibniz for =" (gotten from 3.83) and "transitivity of arrow". So it was a bit silly to clutter up the original 8.12 in the text with the E's and the textual substitutions. By the way, the above cleaner-looking inference rules (which are fine for temp. theorems too, with a "dnof" clause)) start to get quite close to Tourlakis' inference rule "WLUS" ("weak Leibniz with uniform substitution").

The Chief