
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 Atheorems 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 1place 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 Atheorems,
namely, 8.12 (i) and (ii) with all 's replaced by
A  's, i.e., with input and output both Atheorems. 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 Atheorem. 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 cleanerlooking 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").
