B4. LOGIC REIFIED
1. Conjunction
Since we are reifying eventualities and identifying them with
propositions, we need as well to reify combinations of eventualities.
In particular, we need to be able to talk about the conjunction and
disjunction of two eventualities/propositions, about their negation,
and about conditionals or implications.
We will use the name of the logical operator as the name of the
predicate, and as with all predicates there is a primed version of the
predicate that is basic. we will generally but not always use the
primed version, so confusion with CL logical operators should not
arise. A good rule of thumb is that if the arguments of "and", "or",
and "not" are predications, then they are the CL logical operators; if
they are variables, they are predicates in our "Logic Reified" theory.
Thus, in (and (p x)(q x)), "and" is the CL logical operator, and in
(and e1 e2), "and" is the predicate explicated below. In any case, if
a confusion does arise, the meaning of the two expressions will be the
same.
Conjunction is the most straightforward. The "and" of two
eventualities is itself an eventuality, and it exists when its two
constituent eventualities exist.
(forall (e e1 e2) (1)
(if (and' e e1 e2)
(and (eventuality e) (eventuality e1) (eventuality e2)
(iff (Rexist e)
(and (Rexist e1)(Rexist e2))))))
This says that if e is the conjunction of e1 and e2, then all of e,
e1, and e2 are eventualities, and e really exists exactly when e1 and
e2 both really exist.
It does not matter whether the arguments of "and'" are eventuality
types or eventuality tokens.
It is often convenient to apply the "Rexist" predicate to sets of
eventualities. When this is done, it will be interpreted as
conjunction. In fact, existence of a set in the real world is always
true whenever all its members exist in the real world, so we need not
restrict the axiom to eventualities.
(forall (s) (2)
(iff (Rexist s)
(forall (e)
(if (member e s)(Rexist e))))))
2. Negation
The simplest way to characterize negation is analogous to Axiom (1).
The negation of an eventuality really exists if and only if the
eventuality doesn't.
(forall (e1 e2) (3)
(if (not' e1 e2)
(and (eventuality e1)(eventuality e2)
(iff (Rexist e1)
(not (Rexist e2))))))
If e1 is the eventuality of e2's not obtaining, then e1 really exists
exactly when e2 does not really exist.
However, a problem arises with negation. Generally, what is negated
is not an eventuality token but an eventuality type. Consider the
situation where e2 is an eventuality token of the door being opened.
Then we want e1 to be the negation of that, and expect its existence
to mean that the door is not being opened. Suppose in e2 the door is
opened two feet; being an eventuality token, it can have properties
this specific that are not represented in the eventuality structure.
Then e1 could be the eventuality token of the door being opened one
foot. Axiom (3) would hold; if the door is opened two feet, it's not
opened one foot, and if it's opened one foot, it's not opened two
feet.
We could define a stronger concept -- call it "nott'" -- which says
that there is an eventuality type of which e2 is an instance, and the
negation is the negation of that eventuality type.
(forall (e1 e2) (4)
(if (nott' e1 e2)
(exists (e3)
(and (instance e2 e3)(not' e1 e3)))))
In the door opening example, e2 is the eventuality token of opening
the door two feet, e3 could be the eventuality type of opening the
door in general, and e1 would be the eventuality type that negates the
latter.
This may seem highly underspecified, since we are not demanding that
e3 encompass all openings of the door. It could be the eventuality
type of opening the door today, or within the last half hour, or only
from the inside of the room. But in fact in natural language, we
always must determine from context what the set of eventuality tokens
is that is being ruled out. The sentence "John didn't open the door."
usually does not mean that he never in the past opened the door. It
is usually very highly contextually constrained. That is, part of the
interpretation process is exactly to find the appropriate eventuality
type e3 that is being negated.
In this book, when we use the predicate "not'", we will generally
apply it to eventuality types. For example, one person might have a
goal of e2 while another person has a conflicting goal of e1 where
(not' e1 e2) holds. Goals are generally eventuality types rather than
tokens, so the negation presents us with no problem.
The other context in which negation appears is in changes of state
where some eventuality exists before the change and does not exist
after the change. For this, we will define predicates "changeFrom"
and "changeTo" that will hide the complexities in dealing with types
and tokens. This is done in Chapter B10.
3. Disjunction and Implication
Disjunctions and implications also generally take eventuality types as
arguments. We will not insist on it in the definitions, but we will
use the predicates in this book in this fashion.
Disjunction can be defined analogous to conjunction.
(forall (e e1 e2) (5)
(if (or' e e1 e2)
(and (eventuality e) (eventuality e1) (eventuality e2)
(iff (Rexist e)
(or (Rexist e1)(Rexist e2))))))
If eventuality e is the disjunction of eventualities e2 and e3, then
e really exists exactly when one of e2 and e3 really exist.
Disjunction can be applied to a whole set of eventualities. We will
say that the disjunction of a set really exists exactly when one of
the members of the set really exists.
(forall (e s) (6)
(if (disjunction e s)
(and (eventuality e)(eventualities s)
(iff (Rexist e)
(exists (e1)
(and (member e1 s)(Rexist e1)))))))
Implication is defined similarly to "or'", except that in addition to
a single eventuality as the antecedent, we will allow a set of
eventualities as well. The set will be interpreted as the
conjunction.
(forall (e e1 e2) (7)
(if (imply' e e1 e2)
(and (eventuality e) (eventuality e2)
(or (eventuality e1) (eventualities e1)))))
The implication really exists provided the consequent really exists
whenever the antecedent really exists.
(forall (e e1 e2) (8)
(if (imply' e e1 e2)
(iff (Rexist e)
(if (Rexist e1)(Rexist e2)))))
A set of eventualities really exists exactly when each of the
eventualities exists, so this definition covers the case of e1 being a
set of eventualities as well as the case of its being a single
eventuality.
The most important rule of inference involving implication is Modus
Ponens. It can be stated as follows:
(forall (e e1 e2) (9)
(if (and (imply' e e1 e2)(Rexist e)(Rexist e1))
(Rexist e2)))
That is, if e is the implication from e1 to e2, and e and e1 really
exist, then e2 also really exists. This is an immediate consequence
of Axioms (8) and (2).
Implication is transitive. If e1 implies e2 and e2 implies e3, then
e1 implies e3. This follows from Axioms (8) and (2).
(forall (e1 e2 e3 i1 i2 i3)
(if (and (imply' i1 e1 e2)(imply' i2 e2 e3)(imply' i3 e1 e3)
(Rexist i1)(Rexist i2))
(Rexist i3)))
Two sets of eventualities are inconsistent if one implies an
eventuality and the other implies its negation. That is, they have
inconsistent consequences.
(forall (s1 s2) (11)
(iff (inconsistent s1 s2)
(and (eventualities s1) (eventualities s2)
(exists (e1 e2)
(and (imply s1 e1)(imply s2 e2)(not' e2 e1))))))
We can say that some set s1 of eventualties minimally proves an
eventuality e2 if s1 implies e2 but no proper subset of s1 proves e2, and
furthermore e2 is not itself a member of s1.
(forall (s1 e2)
(iff (minimallyProves s1 e2)
(and (not (member e2 s1))
(imply s1 e2)
(not (exists (s2)
(and (properSubset s2 s1)
(imply s2 e2)))))))
Ruling out e2 in s1 is a way of eliminating the trivial case where
{e2} minimally proves e2.
Quantifiers are also a part of logic, but these were dealt with in
Chapter B3. The reification of a universally quantified proposition
is an eventuality that involves typical elements.
Predicates Introduced in this Chapter
(and' e e1 e2): e is the eventuality of both e1 and e2
existing.
(not' e1 e2): e1 is the eventuality of e2 not existing.
(nott' e1 e2): e1 is the eventuality of nothing of e2's
type existing.
(or' e e1 e2): e is the eventuality of either e1 or e2
existing.
(disjunction e s): e is the eventuality of some member of s
existing.
(imply' e e1 e2): e is the eventuality of an implicational
relation between e1 and e2 existing.
(inconsistent s1 s2): s1 and s2 are inconsistent sets of
eventualities.
(minimallyProves s1 e2): s1 proves e2 and no subset of s1 proves e2.