The "old" and "new" Leibniz
Inference Rules

"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.

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:

(\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
quantifications.


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 *.
Then:


               |-    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").