Information Technology Reference
In-Depth Information
EA Implies AE
In [4], Carroll Morgan derives a nice proof of
(
9x
:(
8y
:
P
))
)
(
8y
:(
9x
:
P
))
:
(7)
Wim Feijen [2] presents convincing heuristics for the development of the proof.
Here is the proof. Note that it uses Metatheorem Monotonicity, twice, although
neither Morgan nor Feijen cite it.
(
9x
:(
8y
:
P
))
)h
Monotonicity:
R )
(
8y
:
R
), prov.
y
doesn't occur free in
R
|introduce the necessary universal quantication over
y i
(
8y
:(
9x
:(
8y
:
P
)))
)h
Monotonicity: Instantiation |Eliminate universal quantication
i
8y
(
:(
9x
:
P
))
When we generalize (7) to allow ranges other than
true
, the proof becomes
more complicated. Below, we prove:
Provided
x
not free in
Q
and
y
not free in
R
,
(8)
(
9x R
:(
8y Q
:
P
))
)
(
8y Q
:(
9x R
:
P
))
Since
does not occur free in the consequent, by Metatheorem Witness (9.30)
of [3], (8) can be proved by proving instead
x
R ^
(
8y Q
:
P
)
)
(
8y Q
:(
9x R
:
P
))
;
which we now do:
R ^
(
8y Q
:
P
)
)h^
over
8
, since
y
not free in
R i
(
8y Q
:
R ^ P
)
)h
Monotonicity:
9
-Introduction
i
(
8y Q
:(
9x
:
R^P
))
=
h
Trading
i
(
8y Q
:(
9x R
:
P
))
Discussion
Monotonicity properties (1){(3), as well as Metatheorem Monotonicity, are well-
known. They can be found, in one guise or another, in several texts on logic.
But the two major topics that deal with the calculational approach do a bad
job of explaining how monotonicity/antimonotonicity is to be used. On page 61
of [1], Dijkstra and Scholten discuss the monotonic properties of negation and
implication. But they don't state the general theorem (2) and they don't give
a convention for indicating its use. On page 93 of [1], a hint explicitly states
the use of monotonicity of
^
and
9
in a weakening step, but on pages 73 and
Search WWH ::
Custom Search