|
|
|
Variable-
Binding
in L |
The logic of L departs from that of conventional, single-sorted, first-order
languages in its definition of variable-binding and formulation of the
Quantifier Rules. An occurrence of a variable t/t/T within
a formula 
is a bound occurrence of t/t/T in
if, and only if, it occurs within some part of
which is a formula of the form  t
or of the form  t.
Otherwise, that occurrence is a free occurrence of t/t/T in .
If a formula t
or t
occurs within a formula
(or is the formula
itself), then the scope in
of that occurrence of the quantifier t
or t
is the formula t
or t
itself.8 |
|
Quantifier
Rules
in L |
The rule of Universal Instantiation sanctions the
move from (1) to (2),
(1) t (...ti/ti/Ti...)9
(2) (...tk/tk/Tk...)
where (2) results from replacing every occurrence of ti/ti/Ti
free in,
(3) (...ti/ti/Ti...)
by occurrences of tk/tk/Tk
free in (2). UI thus sanctions the move from (4) to (5,6,7);
(4) wx(w
ex X w
ex W)
(5) x(w
ex Xw
ex W)
(6) x(y
ex Xy
ex Y)
(7) x(z
ex Xz
ex Z)
|
|
|
in each of which generically identical, individual and haecceity variables
w/W free in,
(8) x(w
ex Xw
ex W)
have been replaced by other--or perhaps the same--generically identical,
individual and haecceity variables free in:
(9) x(w
ex Tt
ex T)
UI does not, however, sanction the move from (4) to (10).
(10) x(w
ex X
u ex Y)
For (10) results from replacing generically identical, individual and haecceity
variables w and W in (5), by the generically distinct u and Y.
The rule of Existential Instantiation sanctions the move from (11) to
(12),
(11) t(...ti/ti/Ti...)
(12) (...tk/tk/Tk...)
where (12) results from replacing every occurrence of
ti/ti/Ti
free in (13),
(13) (...ti/ti/Ti...)
by occurrences of tk/tk/Tk
free in (12), which do not occur free in any earlier line of a proof. |
|
|
|
|
cont.
