In contrast to (IA), a quantifier rule describing _what_ can be
deduced from (Ax) F(x) does not require a proviso about free
variable proofs; it simply says
if H has a proof from hypotheses _C_ together with a free
replacement rep(y,t | F(y)) of F(y) ,
(EA0) _C_ , rep(y,t | F(y)) => H ,
then this proof can be prolonged to give a proof of H from
_C_ together with (Ax) F(x) :
(EA1) _C_ , (Ax) F(x) => H ;
here rep(y,t | F(y)) is a replacement of F(y) if it arises from
F(y) by inserting the term t in place of the variable y ,
whereever y is not in the scope of a quantifier (Qy), and this
replacement is free if t does not contain variables z such that
in F(y) the replaced variable y was in the scope of a quantifier (Qz) .
[In Frege 1879 this rule appears on p.52 as formula 61).]
Concerning the existential quantifier (Ex), Frege reduces it to
non-(Ax)-non . An explicit rule to prove (Ex) F(x) takes the form
if a free replacement rep(y,t | F(y)) of F(y) has a proof from a
collection of hypotheses _C_ ,
(IE0) _C_ => rep(y,t | F(y)) ,
then this proof can be prolonged to give a proof of (Ex) F(x) :
(IE1) _C_ => (Ex) F(x) ,
and an explicit rule to prove _from_ (Ex) F(x) is
if H has a proof from hypotheses _C_ together with F(y) ,
(EE0) _C_ , F(y) => H ,
then this proof can be prolonged to give a proof of H from
_C_ together with (Ex) F(x) :
(EE1) _C_ , (Ex) F(x) => H ,
provided the variable y is free in (EA0), i.e. does not
already occur in the hypotheses _C_ or in H outside the scope
of quantifiers (Qy).
As an example, let me use the rules (IA), (EA) an (IE) to give
a proof of the continuity of the function f(x) = xx . To this
end, let _C_ be a system of axioms for the rational (or the
real) numbers, written in form of universally quantified
sentences such that the proviso in (IA) will always hold.
Observe also that, for any quantifier free axiom B(x,y,...),
built propositionally from equations and inequalities, for which
(Ax)(Ay)...B(x,y,...)
occurs in _C_ , there first is trivially a proof
_C_ , B(x,y,...) => B(x,y,...) ,
hence by (EA) also a proof
_C_ , (Ax)(Ay)...B(x,y,...) => B(x,y,...)
which is a proof _C_ => B(x,y,...) . Taking for B the
appropriate laws on inequalitites, I can prove from them
|x-y| < e/|x+y| -> |x+y||x-y| < e ,
hence also
_C_ => (|x-y| < e/|x+y| -> |x+y||x-y| < e ) ;
taking for B the equations for addition and multiplication, I
likewise find proofs
_C_ => xx - yy = (x+y)(x-y) ,
and combining them this gives proofs
_C_ => (|x-y| < e/|x+y| -> |xx - yy| < e ) .
But the last formula is a (trivially free) replacement result
when writing e/|x+y| in place of d in
(|x-y| < d -> |xx - yy| < e ) ,
and so I obtain
_C_ => (Ed)(|x-y| < d -> |xx - yy| < e ) by (IE)
_C_ => (Ay)(Ed)(|x-y| < d -> |xx - yy| < e ) by (IA)
_C_ => (Ax)(Ay)(Ed)(|x-y| < d -> |xx - yy| < e ) by (IA)
_C_ => (Ae)(Ax)(Ay)(Ed)(|x-y| < d -> |xx - yy| < e ) by (IA) .
So much for continuity. Now I also could have argued
_C_ => (|x-y| < e/|x+y| -> |xx - yy| < e )
_C_ => (Ay)(|x-y| < e/|x+y| -> |xx - yy| < e ) by (IA)
_C_ => (Ax)(Ay)(|x-y| < e/|x+y| -> |xx - yy| < e ) by (IA) ,
but while this formula still is a replacement result
rep(d, e/|x+y| | (Ax)(Ay)(|x-y| < d -> |xx - yy| < e )
this replacement is not free, and so I cannot use (IE) to
proceed to
_C_ => (Ed)(Ax)(Ay)(|x-y| < d -> |xx - yy| < e ) .
And this is good so since f(x) = xx is not uniformly continuous
on the whole line. It is so, however, on any bounded domain.
Because taking appropriate laws for inequalities, I can prove
from them
i < x,y < j -> x+y < 2 max(|i|,|j|) ;
hence if J(i,j) is (Ax)(Ay)( i < x,y < j ) then I obtain proofs
_C_ , J(i,j) => x+y < 2 max(|i|,|j|)
_C_ , J(i,j) => |x-y| < e/2 max(|i|,|j|) -> |x+y||x-y| < e
_C_ , J(i,j) => |x-y| < e/2 max(|i|,|j|) -> |xx - yy| < e
_C_ , J(i,j) => (Ay)(|x-y| < e/2 max(|i|,|j|) -> |xx - yy| < e )
_C_ , J(i,j) => (Ax)(Ay)(|x-y| < e/2 max(|i|,|j|) -> |xx - yy| < e ) .
Again, this formula is a replacement result
rep(d, e/2 max(|i|,|j|) | (Ax)(Ay)(|x-y| < d -> |xx - yy| < e )
but this replacement now is free ! Thus I can continue with (IE) to
_C_ , J(i,j) => (Ed)(Ax)(Ay)(|x-y| < d -> |xx - yy| < e )
_C_ , J(i,j) => (Ae)(Ed)(Ax)(Ay)(|x-y| < d -> |xx - yy| < e ) .
So much for uniform continuity.
W.F.