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.