Information Technology Reference
In-Depth Information
We introduce two predicates.
man
:m
:
rs n
m
is a man.
mortal
:m
:person
m
is mortal.
We formalize the statement as follows, with
standing for Socrates, and prove
the formalization. The proof relies on inference rule Modus ponens,
S
Q ) P; Q
−! P
.
(
8 m
:
man
:m )
mortal
:m
)
^ man:S ) mortal:S
(
8m
:
man
:m )
mortal
:m
)
^ man:S
)h
Monotonicity: Instantiation, with
S
for
m i
(
man
:S )
mortal
:S
)
^
man
:S
)h
Modus ponens
i
mortal
:S
Here is a second proof, which transforms the whole formula into a known
theorem.
(
8m
:
man
:m )
mortal
:m
)
^
man
:S )
mortal
:S
(h
Antimonotonicity: Instantiation, with
S
for
m i
(
man
:S )
mortal
:S
)
^
man
:S )
mortal
:S
|Modus ponens
Having a Heart
Now consider the English statement:
None but those with hearts can love. Some liars are heartless. Therefore,
some liars cannot love.
Using
hh:p
for \
p
has a heart",
cl:p
for \
p
can love", and
li:p
for \
p
is a
liar", we formalize this as
(
8p
:
cl:p ) hh:p
)
^
(
9p
:
li:p ^:hh:p
)
)
(
9p
:
li:p ^:cl:p
)
:
We prove this formula.
(
8p
:
cl:p ) hh:p
)
^
(
9p
:
li:p ^:hh:p
)
=
h
Distributivity of
|to get
same outer quantication as in consequent
^
over
9
i
(
9p
:(
8p
:
cl:p ) hh:p
)
^ li:p ^:hh:p
)
)h
i
Monotonicity: Instantiation
(
9p
:(
cl:p ) hh:p
)
^ li:p ^:hh:p
)
=
h
Contrapositive
i
(
9p
:(
:hh:p ):cl:p
)
^ li:p ^:hh:p
)
)h
Monotonicity: Modus ponens)
i
(
9p
:
:cl:p ^ li:p
)
Search WWH ::
Custom Search