Information Technology Reference
In-Depth Information
P
but antimonotonic in
R
,and (
9x R
:
P
) is monotonic in both
P
and
R
.
Formally, we have:
Monotonic
_
:
(
P ) Q
)
)
(
P _ R ) Q _ R
)
(1)
Monotonic
^
:
(
P ) Q
)
)
(
P ^ R ) Q ^ R
)
Antimonotonic
:
:
(
P ) Q
)
)
(
:P (:Q
)
(2)
Monotonic consequent:
(
P ) Q
)
)
((
R ) P
)
)
(
R ) Q
))
P ) Q
)
P ) R
(
Q ) R
Antimonotonic antecedent:
(
)
((
)
(
))
8
P ) Q
)
8x P
R
(
8x Q
R
Antimonotonic
-range:
(
)
((
:
)
(
:
))
8
P ) Q
)
8x R
P
)
8x R
Q
Monotonic
-body:
(
)
((
:
)
(
:
))
Monotonic
9
-range:
(
P ) Q
)
)
((
9x P
:
R
)
)
(
9x Q
:
R
))
Monotonic
9
-body:
(
P ) Q
)
)
((
9x R
:
P
)
)
(
9x R
:
Q
))
(3)
But which of the following two formulas is valid, if either?
(
8x :P
:
S
)
)
(
8x :
(
P _ Q
):
S
)
(
8x :P
:
S
)
(
(
8x :
(
P _Q
):
S
)
P
The answer is given by the following denition and theorem. Throughout,
E
denotes non-capture-avoiding substitution of free variable
z
by
P
in formula
E
.Also,
E
[
z
:=
P
] denotes capture-avoiding substitution:
E
[
z
:=
P
]isacopy
of expression
E
in which all occurrences of variable
z
have been replaced by
expression
, with names of dummies (bound variables) being rst replaced to
avoid capture.
Denition 1.
Consider an occurrence of free variable
P
z
in a formula
E
(but
not within an operand of
is called
monotonic
if it is nested within an even number of negations, antecedents, and ranges of
universal quantications; otherwise, it is
antimonotonic
.
). The position of
z
within
E
P ) Q
Theorem 2. Metatheorem Monotonicity.
Suppose
is a theorem.
E
z
Let expression
contain exactly one occurrence of free variable
. Then:
(a) Provided the position of
z
in
E
is monotonic,
z
z
Q
is a theorem.
(b) Provided the position of
E
P
) E
z
in
E
is antimonotonic,
P
( E
Q
E
is a theorem.
[
Note:
Actually,
,aslongasall
its positions are monotonic or all its positions are antimonotonic.]
We can state (a) and (b) as inference rules:
E
can contain more than one occurrence of
z
Monotonicity:
Provided
z
's position in
E
is monotonic,
(4)
z
z
Q
P ) Q −! E
P
) E
Antimonotonicity:
Provided
z
's position in
E
is antimonotonic,
(5)
z
z
Q
P ) Q −! E
P
( E
Search WWH ::
Custom Search