Information Technology Reference
In-Depth Information
)
P
(
8x
:
P ^ R
)
(
8x
:
z ^ R
)h
Monotonicity: Weakening
P ) P _ Q i
)
P _Q
(
8x
:(
P_Q
)
^R
)
(
8x
:
z ^ R
)
P
:
(
8x :P ^ R
:
S
)
:
(
8x :z ^ R
:
S
(h
P ) P _ Q i
Antimonotonicity: Weakening
:
8x :
P _ Q
^ R
S
:
8x :z ^ R
S
)
P _Q
(
(
)
:
)
(
:
Examples of the Use of Monotonicity
When dealing with theorems of propositional logic, monotonicity is not needed at
all; as [3] shows, all proofs can be done easily without weakening/strengthening
steps. However, for predicate logic proofs, weakening/strengthening steps are
very useful, as the following examples show. These calculational proofs, using
monotonicity/antimonotonicity, are surprisingly simple, especially compared to
similar proofs in other proof systems. Each step of the proof is guided by the
shapes of the current formula and goal. The theorems used in these proofs are
from [3].
Proving Instantiation
In [3], the One-point rule is an axiom and Instantiation is a theorem:
One-point rule:
Provided
x
does not occur free in
E
,
(6)
(
8x x
=
E
:
P
)
P
[
x
:=
E
]
Instantiation:
(
8x
:
P
)
) P
[
x
:=
E
]
We prove Instantiation. Let
z
be a variable that does not occur free in
P
or
E
.Wehave:
(
8x
true
:
P
)
=
h
Dummy renaming |
z
not free in
P i
(
8z
true
:
P
[
x
:=
z
])
)h
Antimonotonicity:
true
( z
=
E i
(
8z
z
=
E
:
P
[
x
:=
z
])
=
h
One-point rule
i
P
[
x
:=
z
][
z
:=
E
]
=
h
Property of textual substitution |
z
is not free in
P i
P
[
x
:=
E
]
Mortality of Socrates
This example concerns proving English arguments sound by formalizing them
and proving their formalizations. Consider the following statement.
All men are mortal. Socrates is a man. Therefore, Socrates is mortal.
Search WWH ::
Custom Search