Logics for Computer Science

12.2. INTUITIONISTIC LOGIC 389 there is no twin prime bigger than 101010 . Hence at this stage, we cannot accept the truth of the following sentence: Either there is a twin prime bigger than 101010 or there is no twin prime bigger than 101010 . This is the basic insight of L. E. J. Brower who says that if the law of excluded middle is accepted, then we are assuming that every mathematical problem is solvable (in this sense), and this is certainly objectionable. In the absence of excluded middle, the law of double negation fails. Though A → ¬¬A would still remain valid, its converse ¬¬A → A will no more hold. In the intuitionistic propositional logic, INT, negation has a different meaning. In INT the sentence 0 = 1 is a contradiction, but for any sentence A, the proposition A ∧ ¬A cannot be accepted as a contradiction. INT has the same vocabulary as that of PL; leaving aside the symbols � and ⊥. We do not take ↔ into its vocabulary right now since this can be expressed in terms of → and ∧ as in PC. INT assigns different meanings to the connectives; it is a deviant logic. Axiom Schemes of INT: (I1) A → (B → A) (I2) A → (B → (A ∧ B)) (I3) (A ∧ B) → A (I4) (A ∧ B) → B (I5) A → (A ∨ B) (I6) B → (A ∨ B) (I7) (A ∨ B) → ((A → C) → ((B → C) → C)) (I8) (A → B) → ((A → (B → C)) → (A → C)) (I9) (A → B) → ((A → ¬B) → ¬A) (I10) A → (¬A → B) Rule of Inference of INT: (MP) A A→B B A. Heyting gave an axiomatization of INT, in which axioms and the law of uni- form replacement had been used. The above axiomatization is by M. Dummett, which uses axiom schemes. A possible world semantics of INT uses the same idea of a frame and a model as in the modal logics, except that all our frames are now reflexive and transitive. That is, a model is a triple M = (W, R, �), where W is a nonempty set of worlds, R is a reflexive and transitive relation on W, and � is a relation from W to the power set of all atomic propositions. The relation � is extended to include all propositions in its domain by using the following rules:

390 CHAPTER 12. SOME OTHER LOGICS w � ¬p iff for all z ∈ W with wRz, z �� p. w � p ∧ q iff w � p and w � q. w � p ∨ q iff w � p or w � q. w � p → q iff for all z ∈ W with wRz, z �� p or z � q. M � p iff for all w ∈ W, w � p. As assumed earlier, the completeness and the soundness of the axiomatic system INT can be proved with respect to the above semantics. However, since we use a possible world semantics for INT, it must have some connection with modal logics. It can be verified that the following translation (due to K. Go¨del) to the logic S4 (KT4) holds. Writing the translation by the map ∗, we have p∗ = p (¬p)∗ = ¬ �p∗ (p ∨ q)∗ = �p∗ ∨ �q∗ (p ∧ q)∗ = �p∗ ∧ �q∗ (p → q)∗ = �p∗ → �q∗ You can interpret � as ‘it is demonstrated that’. Now, rethink along the lines of the two introducing illustrations above (that of ab and of the twin primes). What is the relation between PL-validity and INT-validity? Note that all axioms of INT are PL-valid, and the inference rule is MP, which is also a valid consequence of PL. It follows (by induction?) that every INT-valid proposition is PL-valid. The converse does not hold. The relation is best understood by noting that whenever p is PL-valid, its double negation ¬¬p is also PL-valid. But this does not happen in INT. The following result (See Glivenko (1929) for a proof.) explains the connection between PL and INT. Theorem 12.1. For a set of propositions Σ, let ¬¬Σ = {¬¬w : w ∈ Σ}. Let A be any proposition. Then, Σ �PL A iff ¬¬Σ �INT ¬¬A. Moreover, �PL ¬A iff �INT ¬A. Notice that Theorem 12.1 does not say that �PL A iff �INT A. This holds when the only connectives used are ¬ and ∧. However, double negation does not hold even in this restricted language. For example, ¬¬p �PL p but ¬¬p �INT p. Theorem 12.1 suggests that PL-theorems may have a translation into INT in some sense. The following is such a translation of PL-theorems to INT-theorems via the map † : p† = ¬¬p (p ∧ q)† = p† ∧ q† (p ∨ q)† = ¬(¬p† ∧ ¬q†) (p → q)† = ¬(p† ∧ ¬q†) This translation preserves consequences. However, if p† = ¬¬p is replaced by p† = p, then only theorem-hood is preserved; see Gentzen (1936) and Łukasiewicz (1970). Dummett (1977) discusses the set assignment semantics for INT. Along with other proof procedures for INT, intuitionistic first order logic has also been well studied. Basing on this logic, intuitionistic mathematics has been created.

12.3. ŁUKASIEWICZ LOGICS 391 Exercises for § 12.2 1. Why is it that rejection of the law of excluded middle leads to the rejection of the validity of ¬¬A → A? Why does the conditional A → ¬¬A still hold? [Hint: Use PC instead of PL.] 2. Show that the rejection of the law of excluded middle leads to the invalidity of ¬(A ∧ B) → (¬A ∨ ¬B). 3. Prove that if A is a proposition that uses only ¬ and ∧, then �PL A iff �INT A. 12.3 ŁUKASIEWICZ LOGICS Consider the sentence: “There will be an earth quake tomorrow”. Is it true? Is it false? Since nothing about its truth or falsity is known today, it is neither true nor false. But it is quite possible that tomorrow an earth quake may really occur. Its truth is beyond the classical bivalence. It is something like an amoral action, which is neither moral nor immoral; it is beyond morality. To take into account such propositions, which do come up in abundance in day- to-day life, the bivalent logics like PL or FL would not suffice. What about assigning a new truth value to ‘beyond true or false’? Suppose that we agree to have one more truth value, say, 1/2, in addition to 0 and 1. As in PL, we start with �, ⊥, and the propositional variables as atoms and use the connectives ¬, ∧, ∨, → to build up a formal language of propositions. The semantics of the logic is different from that of PL. Writing the truth value of a proposition p as t(p), the semantics may be specified as follows: t(�) = 1 t(⊥) = 0 t(¬p) = 1 − t(p) t(p ∧ q) = min {t(p), t(q)} t(p ∨ q) = max {t(p), t(q)} � 1 if t(p) = t(q) t(p → q) = max {1 − t(p), t(q)} otherwise The same is also given in terms of a truth table; see Table 12.1. Formally, you can define an interpretation as a map from all propositions to the set of truth values {0, 1/2, 1}, obeying the conditions given in the truth table. Alter- natively, you can show that the map t(·) is well defined on the set of all propositions (due to unique parsing), starting from a preliminary definition on the set of atomic propositions. That defines the concept of an interpretation; each such map is an interpretation. Then you can define equivalence by p ≡ q iff t(p) = t(q) for any interpretation t. Moreover, we define the connective ↔ as follows: p ↔ q � (p → q) ∧ (q → p)

392 CHAPTER 12. SOME OTHER LOGICS Table 12.1: Truth table with three truth values � ⊥ p q ¬p p∧q p∨q p → q 10 0 0 1 0 0 1 1/2 0 1/2 0 1/2 1/2 100 0 1 0 0 1/2 0 1/2 1 1 1/2 1/2 1/2 1/2 1 1/2 1/2 1 1/2 01 01 1 1/2 1 1/2 1 1 11 11 1 We call this three-valued logic, L3 after the logician J. Łukasiewicz. Though the law of excluded middle does not hold in L3, a similar law called the law of trivalence holds. To formulate this law, we introduce the indeterminate proposition in L3, written as ıp (iota p). Let p be any propositional variable. Define a proposition ıp by ıp � p ↔ ¬p The proposition ıp is called an indeterminate proposition. The truth table of ıp can be given as p 0 1/2 1 ıp 0 1 0 Any proposition A equivalent to � is called an L3-tautology or an L3-valid propo- sitioTnh, eanladwisowf rtirtitvenalaesnc�eLi3s A. It thus follows that p q iff p q the metastatement ≡ ↔ ≡ �. p ∨ ¬p ∨ ıp ≡ � in L3 for any proposition p. You can also check the following for any interpretation t in L3: t(p → q) = 1 iff t(p) ≤ t(q), and t(p ↔ q) = 1 iff t(p) = t(q). Let Σ be a set of propositions (in L3 now), and let w be any proposition. Define the validity of an L3-consequence by Σ �L3 w iff for each interpretation t, if t(A) = 1 for each A ∈ Σ, then t(w) = 1. You can check that the following results hold: Modus Ponens: {p, p → q} �L3 q. Equivalence Replacement: p ↔ q �L3 A ↔ A[p :=e q]. Uniform Replacement: If �L3 B, then �L3 B[p := q]. where A[p :=e q] is obtained from A by substituting some or all or no occurrence of p in A by q, and B[p := q] is obtained from B by substituting every occurrence of p in B by q. Moreover, J. Łukasiewicz constructed L3 for arguing about possibility and neces- sity by using the following truth table:

12.3. ŁUKASIEWICZ LOGICS 393 p �p ♦p 00 0 1/2 0 1 11 1 From the above data, it is clear that ♦p ≡ ¬p → p and �p ≡ ¬♦¬p. (Verify.) Though A → �A is not L3-valid, we have �L3 A → (A → �A). Theorem 12.2 (Deduction Theorem in L3). Let Σ be a set of propositions, and let A, B be propositions. Then, Σ ∪ {A} �L3 B iff Σ �L3 A → (A → B). Further, we can have a translation of PL (or PC) into L3, which preserves conse- quences. This is achieved via the translation map ∗ from PL to L3 by p∗ = p for atomic propositions p. (¬p)∗ = p∗ → (p∗ → ¬(p∗ → p∗)) Σ∗ = {p∗ : p ∈ Σ} for any set Σ of propositions. Such a translation identifies PL in L3. Observe that a simplistic way of identifying both 1 and 1/2 with 1, i.e., true, would not result in PL. Similarly, identifying both 0 and 1/2 with 0 will also fail. (Why?) However, any L3-tautology is vacuously a PL-tautology since the truth tables of connectives in L3 restricted to the values of 0 and 1 are simply the PL-truth tables. Observe that the truth function σ p given by σ p is 1/2 for every value of p is not definable from the connectives ¬, ∧ and ∨. This is so because, if it were, then ¬σ p and σ p would be equivalent, forcing �L3 ¬σ p ↔ σ p to hold. Since each L3-tautology is a PL-tautology, ¬σ p ↔ σ p would also be PL-valid. But this is obviously wrong as ¬A ↔ A is not PL-valid. This truth function σ is called the Słupecki operator. Consideration of the Słupecki operator shows that for the truth functional completeness, the connectives ¬, ∧, ∨ are not enough in L3. However, the set {¬, →} of connectives is truth functionally complete in L3. An adequate axiomatic system (see Wo´jcicki (1998)) for L3 which uses ¬ and → as in PC, has the following axiom schemes and the rule of inference: Axiom Schemes for L3 (L1) A → (B → A) (L2) (A → B) → ((B → C) → (A → C)) (L3) (¬A → ¬B) → (B → A) (L4) ((A → ¬A) → A) → A Rule of Inference (MP) A A→B B

394 CHAPTER 12. SOME OTHER LOGICS A generalization of Łukasiewicz three-valued logic L3 has been obtained by him and A. Tarski. We briefly mention its peculiarity here. The idea is to view the truth values as any real number between 0 and 1, instead of the three values 0, 1/2, 1. An interpretation is taken as a map from the set of atoms to the interval [0, 1]. This map is extended to all propositions by t(¬p) = 1 − t(p) t(p ∨ q) = max {t(p),t(q)} t(p ∧ q) = min {t(p),t(q)} � 1 if t(p) ≤ t(q) t(p → q) = 1 − t(p) + t(q) otherwise Many logics can be defined using this scheme t of truth values, depending upon what subset of the interval [0, 1] is fixed as the co-domain of the interpretation t. Some of the logics and their corresponding co-domains of the interpretations are given in the following table: Logic Co-domain of interpretations Ln m { n−1 : 0 ≤ m ≤ n − 1, n ≥ 2} Lℵ0 Lℵ { m : 0 < m ≤ n, m, n ∈ N} n [0, 1] In all cases, a proposition is called valid if each interpretation evaluates it to 1. For example, Lℵ has the valid propositions as all p for which t(p) = 1 for each interpretation t with the co-domain as the interval [0, 1]. In this scheme, we get many logics such as L2, L3, L4, L5, . . . , Lℵ0 , Lℵ. Note that L2 is simply the propositional logic PL. Further, Ln =� Ln+1, and each valid proposition of Lm is also Ln-valid provided that n divides m. Again, Lℵ0 is the same as Lℵ in the sense that their valid propositions coincide. This is a non-trivial result; see Epstein (2001). Now, in view of these many-valued logics, what do you think of INT? For a proposition p, you have ¬p, ¬¬p; and ¬¬¬p is equivalent to ¬p in INT. So, is INT a three-valued logic? Is it L3, say, in the sense that INT-valid propositions coincide with L3-valid propositions? Or, is the converse true? K. Go¨del has proved in 1932 that INT cannot be characterized as any finite valued logic Ln (for n = 2, 3, 4, . . .). It is again a non-trivial a result. Still there are other varieties of many-valued logics. An example is Kleene’s three-valued logic which has the same three truth values 0, 1/2, 1. Unlike L3, in Kleene’s three-valued logic, when both A, B are 1/2, the formula A → B is evaluated to 1/2. You may define other many-valued logics by playing with the truth values and the connectives.

12.4. PROBABILISTIC LOGICS 395 Exercises for § 12.3 1. Verify the formulas for t(p) in Łukasiewicz logic using Table 12.1. 2. Construct the truth table for ↔ in L3 by defining p ↔ q as (p → q) ∧ (q → p). 3. Show that in L3, p ∨ ¬p �≡ � and that p → q ≡� ¬p ∨ q. 4. Show that �L3 p ∨ ¬p ∨ ıp. What are ı� and ı⊥? 5. Show the following equivalences in L3 : (a) (p → (q → p)) ≡ � (b) p ∨ q ≡ (p → q) → q (c) p ∧ q ≡ ¬(¬p ∨ ¬q) (d) σ ¬p ∨ q ≡ p → (p → q) 6. Prove Theorem 12.2. 7. With the translation map ∗ for L3, show that Σ �PL A iff Σ∗ �L3 A∗. 8. Show that Lℵ can be axiomatized with the axiom schemes L1, L2, L3, and (A → B) ∨ (B → A), and the inference rule MP. 12.4 PROBABILISTIC LOGICS A doctor wants to decide whether a patient has the disease D after listening to and examining the patient for symptoms. He only knows that certain symptoms and certain diseases occur with such and such probabilities. (In this section, we write p(·) for probabilities and not for denoting propositions.) Write S → D to mean that the symptom S implies the infliction of the disease D. To be specific, suppose that the doctor knows the following: A1: A → D holds with probability p1 . A2: ¬A → D holds with probability p2 . A3: B → D holds with probability p3 . When the patient exhibits the symptoms ¬A and B, the doctor wants to determine whether the patient has the disease D. Note that the probabilities assigned to the above statements are the doctor’s knowledge, i.e., they are subjective. So, the diag- nosis will also be subjective; it is his rational opinion. It is rational in the sense that the final decision uses an objective procedure even on the subjective probabilities. He uses his subjective probabilities to compute the probability of the patient suffer- ing from the disease D given that the patient exhibits the symptoms ¬A and B. The doctor’s interest is in determining the conditional probability p(D |¬A ∧ B) = p(D ∧ ¬A ∧ B) . p(¬A ∧ B) Such computations become meaningful in the presence of a probability distribution of propositions, that is, a probability space of propositions and a probability measure on this space. In the diagnosis problem, we may consider the relevant propositions to be drawn from the set U = {A, B, A ∧ D, ¬A, ¬A ∧ D, B ∧ D, D, A ∧ B, ¬A ∧ B, D ∧ ¬A ∧ B}. Then, we go for constructing the set of elementary propositions (not necessarily atomic) so that a probability measure can be defined. The set E = {E1, E2, . . . , En} of elementary propositions will satisfy the following properties:

396 CHAPTER 12. SOME OTHER LOGICS 1. Each relevant proposition is a disjunction of some elementary propositions. 2. The elementary propositions are exhaustive: E1 ∨ . . . ∨ En ≡ �. 3. The elementary propositions are mutually exclusive: Ei ∧ E j ≡ ⊥ for i �= j. Thus, in our diagnostic problem, we take the set E = {A, B, D, ¬A, ¬B, ¬D} assuming that A, B, D are atomic. Next, a probability measure is defined on the set E = E ∪ {�, ⊥}. A probability measure is a function p : E → [0, 1] satisfying the following properties: (a) For any X,Y ∈ E, p(X) ≥ 0. (b) p(�) = 1, p(⊥) = 0. (c) If X ∧Y ≡ ⊥, then p(X ∨Y ) = p(X) + p(Y ). The probabilities are used to compute the required conditional probability. Note that the restrictions of a probability measure are imposed on the subjective probabil- ities of a decision-maker, here, the doctor. This is the reason that a decision-maker who uses probabilistic logic is assumed to be a rational agent. As you have guessed, probabilistic logic is rather a logical methodology for decision making than a logic. One can go further in deciding upon a consensus by taking opinions from experts for fixing the subjective probabilities of elementary propositions. One may also resort to statistical methods while arriving at a consensus. A good start on this topic may be Halpern (1990). In a probabilistic framework, it is not possible to assign a probability to igno- rance; we only assign a probability to what is known. In the presence of ignorance or insufficient information, and vagueness, probabilistic logic will not be appropri- ate. In the next section, we will have a rough outline of the two types of logics that deal with uncertainty and vagueness. 12.5 POSSIBILISTIC AND FUZZY LOGIC Consider the sentence s: Sam is tall. By introducing a variable h for the height of Sam, you can translate the sentence to h ≈ tall. If h takes values from the set { tall, medium, short }, then the truth predicate Ph can be evaluated to one value, depending upon whether h is tall, medium or short. Say, Ph is either 1, 1/2 or 0 according as h is tall, medium, or short. Then the predicate Ph is called a crisp predicate, as it has definite values. If height is allocated a value, say, any real number between 40 cm and 300 cm, then possible values for Ph will be uncountably many. In such a case, Ph has no definite value from among finitely many; it is now referred to as a vague predicate. The range of values, the closed interval U = [40 cm, 300 cm], is our universe for height h, and Ph is a vague predicate defined on this universe U. Here the predicate Ph is unary; thus, when it is crisp, it is just a subset of U. What would happen if Ph is a vague predicate? It is clearly not a subset, for we do not know or we cannot know for certainty which elements of U are in Ph and which are not. In such a case, we say that Ph is a fuzzy subset of the universe U. Any subset A of a set U can be characterized by its characteristic or indical function χA : U → {0, 1}, by the rule that for any u ∈ U, u ∈ A iff χA(u) = 1. In case

12.5. POSSIBILISTIC AND FUZZY LOGIC 397 A is a fuzzy subset of U, we identify this fuzzy subset with the membership function µA : U → [0, 1]. Thus, any element u ∈ U is a fuzzy member of the fuzzy subset A of U determined by its degree of membership µA(u). (Imagine membership to admit of degrees rather than being either 0 or 1.) If µA(u) = 1, then u ∈ A, as in the case of a crisp subset. If µA(u) = 0, then u �∈ A, again as in the crisp subset case. If µA(u) = α for 0 < α < 1, then the degree of membership of u in A is α. When B = Ph is taken as a fuzzy subset of U (as a vague predicate), we have a membership function µB. Then µB gives the idea as to how much tall Sam is, or rather, “what is the degree of tallness of Sam when his height is so and so”. It gives rise to four cases as considered in the following subsections. below. The ensuing four cases are of crisp sentences and precise information, crisp sentences and imprecise information, crisp sentences and fuzzy information, and vague sentences and fuzzy information. These cases are considered in the following subsections. 12.5.1 Crisp Sentences and Precise Information Suppose that B = {150 cm }; we know that Sam is 150 cm tall. Here, B ⊆ U is a crisp subset of U. Depending upon whether we consider 150 cm as a height to be termed as tall or not, µB(s) will take a value in {0, 1}. That is, the truth of the sentence s is either 0 (s is false) or 1 (s is true). Here, Sam’s height is exactly known. We also have a crisp sentence since we have the information whether this height is termed as tall or short. Thus the case is compared to PL, where the truth of each sentence is either 0 or 1. That is, t(s) = µB(s) ∈ {0, 1}. 12.5.2 Crisp Sentences and Imprecise Information Suppose we know that Sam’s height is within 150 cm to 200 cm, i.e., we do not have precise information here. Suppose also that the meaning of tall is crisp, i.e., if the height of a person is within a range, say, a to b in centimetres, then he is called tall. Symbolically, the predicate “tallness” is identified with the crisp subset [a, b] ⊆ U. Then, the following cases may be considered: (a) If B = [150, 200] ⊆ A = [a, b], then clearly, t(B) = 1; Sam is tall. (b) If A ∩ [a, b] = ∅, then t(B) = 0; Sam is not tall. (c) If A ∩ [a, b] =� ∅ but A ⊆� [a, b], then t(B) cannot be fixed to either 0 or 1. The sentence “Sam is tall” is possibly true or possibly false. These situations are tackled by introducing a possibility measure π as follows: for any subset E of U, π(E) = 1 if E ∩ A �= ∅, else, π(E) = 0. Then the above cases correspond to: (a) π(s) = 1, π(¬s) = 0. (b) π(s) = 0, π(¬s) = 1. (c) π(s) = 1, π(¬s) = 1. The case π(s) = 0, π(¬s) = 0 leads to inconsistency; hence, it cannot occur.

398 CHAPTER 12. SOME OTHER LOGICS 12.5.3 Crisp Sentences and Fuzzy Information Suppose that the meaning of tallness is crisp, i.e., we have a range of values for tallness, say, if the height of anyone is in [a, b] ⊆ U, then he is called tall. Assume also that our information on Sam’s height is fuzzy. That is, B = Ph is now a fuzzy subset of U, which is given by a membership function µB. Then, our answer to the query “whether Sam is tall” will have a fuzzy answer, i.e., tallness of Sam will have the degree of truth as µB(s). 12.5.4 Vague Sentences and Fuzzy Information Here, both the sets representing tallness and Sam’s height are fuzzy subsets of U. Suppose that S represents Sam’s height, i.e., S is a fuzzy subset of U given by its membership function µS, and tallness is also a fuzzy subset B of U given by its membership function µB. Then the answer to the query “whether Sam is tall” will also be fuzzy. That is, the truth of the sentence “Sam is tall” will take a fuzzy truth value in the interval [0, 1], depending on the values of µB and µS. For example, “Sam’s height is about 170 cm” is a fuzzy sentence. Such a sentence is translated to a membership function µS : [0, 1] → [0, 1] defined as µS(v) = sup {π(u) : µB(u) = v for u ∈ U}. Here, the supremum over an empty set is taken as 0. Thus whenever µ −1 (v) = ∅, B we have µS(v) = 0. The truth value t(s) of the sentence “Sam is tall” is approximated by the numbers N(s) and Π(s) given by N(s) ≤ t(s) ≤ Π(s), Π(s) = sup{min {µB(u), π(u)} : u ∈ U}, N(s) = 1 − Π(¬s) = inf{max {µB(u), 1 − π(u)} : u ∈ U}. This is the most general case, as all the earlier cases will fall into place by regarding the fuzzy subsets as crisp. The function Π is called the possibility measure and N is called the necessity measure so that the uncertainty or fuzzy measure t(s) lies between the possibility and necessity. The high rate at which work in fuzzy logic and fuzzy mathematics is growing at present prevents a non-specialist to catch up. However, it is wise to brush up some basic literature so that it will be easy for you later when some application domain demands fuzzy logic ideas. You may start with Tanaka (1996). 12.6 DEFAULT LOGIC In this section, we briefly look at another way of dealing with certain kind of vague- ness. The vagueness here is associated to limitations of knowledge or in its represen- tation. For instance, when we say that “birds fly”, we do not mean that all birds fly without exception, nor do we assert that only some birds fly. It is almost a general rule that birds fly; however, there might be exceptions, as we know that penguins do

12.6. DEFAULT LOGIC 399 not fly and that a wounded bird may not fly. Such facts can be represented by first order consequences such as P(x) ∧ ¬ exception1(x) ∧ · · · ∧ ¬ exceptionm(x) � Q(x). In so doing, we are treating exceptions as general facts defeating the intention of a “general rule”. We are also assuming that these are all possible exceptions. Tomor- row, we may discover another species of birds which might not fly! To tackle such cases, we introduce a type of rule, called default. If we know that Tweety is a penguin, all penguins are birds, birds fly, and pen- guins do not fly, then we should be able to conclude that Tweety does not fly. We would not just dispense with the facts by telling that the facts are inconsistent. (Where is the inconsistency?) Here, we may take the following as facts: Each penguin is a bird. Tweety is a bird. Tweety is a penguin. The sentence “birds fly” will be taken not as a fact, but as a default rule since this is the one that may admit of exceptions. The default rule is: If x is a bird and it cannot be proved that x is a penguin, then deduce that x flies. Or, as a fraction: x is a bird : x is not a penguin Thus, x flies x is not a penguin would now mean if it cannot be proved that x is not a penguin. This can also be written as if it is consistent to assume that x is not a penguin. Formally, a default (a default rule) looks like u(x) : v1(x), . . . , vm(x) w(x) where u(x), v1(x), . . . , vm(x) and w(x) are well-formed formulas (of FL, in general) whose free variables are among x1, . . . , xn, written here as a single symbol x. The formula u(x) is called the prerequisite of the default. The formulas v1(x) . . . , vm(x) are the justifications and w(x) is called the consequent of the default. The meaning of the default is If v1(x), . . . , vm(x) are consistent with what is already known, then w(x) is inferred. A default theory is a pair of sets Δ = (D,W ), where D is a set of default rules and W is a set of FL-sentences.

400 CHAPTER 12. SOME OTHER LOGICS Default logic is a nonmonotonic logic in the sense that addition of new facts may invalidate earlier established consequences. For example, consider the default theory Δ = (D,W ), where W = {bird(tweety)} and D has the single rule: bird(x) : ¬ penguin(x) f lies(x) Here, we infer that f lies(tweety). If we enlarge W to W � = W ∪ {penguin(tweety)}, then we cannot infer f lies(tweety). EXAMPLE 12.1. Consider a universe (of constants) having two members, say a and b. Assume that an object in this universe is not an elf unless it is required to be. Moreover, at least one of a or b is an elf. Then its default theory is � � : ¬ el f (x) Δ = (D,W ) with W = {elf (a) ∨ elf (b)}, D = ¬ elf (x) . The default rule in D says that “if it is consistent to assume that x is not an elf, then deduce that x is not an elf”. You see that neither elf (a) nor elf (b) can be inferred from the single fact elf (a) ∨ elf (b). Since neither elf (a) nor elf (b) can be concluded, we would like to think that ¬ elf (a) ∧ ¬ elf (b) is provable. However, this sentence is inconsistent with the fact elf (a) ∨ elf (b). In order to avoid this inconsistency, default reasoning admits of many extensions. In the above example, we have an extension (an extended theory of Δ), where we can infer ¬ elf (a) ∧ elf (b), and in another extension of Δ, we can infer elf (a) ∧ ¬ elf (b). Formally, let Δ = (D,W ) be a given default theory. Let S be a set of FL-sentences. For any set A of FL-sentences, denote by Th(A), the theory of A, i.e., the set of all FL-sentences which can be inferred from the set of premises as A. Define Γ(S) as the smallest set satisfying the following properties: 1. W ⊆ Γ(S). 2. Γ(S) = T h(Γ(S)). u : v1, . . . , vm w 3. For u ∈ Γ(S), and for ¬v1, . . . , ¬vm ∈� S, if ∈D then w ∈ Γ(S). Finally, a set E is called an extension for Δ iff Γ(E) = E. You can interpret Γ(S) as the minimal set of beliefs that one can have in view of S, where S indicates which justification for beliefs is to be admitted. E is a fixed point of the operator Γ, just as Th(A) is a fixed point of the operator Th in FL (i.e., Th(T h(A)) = T h(A)). Alternatively, extensions of default theories can be defined from within. Let Δ = (D,W ) be a default theory. An extension for Δ is any set E = ∪i∈NEi, where the sets Ei are defined recursively by � � Ei . E0 = W, Ei+1 = T h(Ei) ∪ w : u : v1, . . . , vm ∈ D, u ∈ Ei, ¬v1 . . . , ¬vm ∈� w It can be proved that whenever W is consistent, every extension of the corresponding theory is consistent. The following examples will show you that a proper translation of facts and rules to a default theory can lead to the desired inference.

12.6. DEFAULT LOGIC 401 EXAMPLE 12.2. (Dubois et al. (1985)) Consider the following facts: 1. Generally, if Mary attends a meeting, Peter does not. 2. Generally, if Peter attends a meeting, Mary does not. 3. At least, one of Peter or Mary attends the meeting. To have a default theory, let us use the following symbolization: M : Mary attends the meeting. P : Peter attends the meeting. Here, � M : ¬P P : ¬M � ¬P ¬M . Δ1 = (D1,W1), W1 = {M ∨ P}, D1 = , This default theory has the unique extension E1 = Th({M ∨ P}). However, it is awk- ward since we cannot infer from this extension that “both do not attend the same meeting”. However, this sentence ought to be worth concluding. We will have an- other translation below, where this is possible. This time, we take Δ2 = (D2,W2), where W2 = W1, as earlier, but � :M :P � ¬P ¬M D2 = , . Here, the default translation of the sentence Generally, if x attends a meeting, then y does not. is taken as If it is consistent to assume that x attends a meeting, then infer that y does not attend it. In this translation, Δ2 has two extensions (Verify!): E2 = Th({M, ¬P}), E2� = Th({P, ¬M}). You see that ¬(M ∧ P) ∈ E2 and also ¬(M ∧ P) ∈ E2� . A still better translation would be: �: M ∧ ¬P : P ∧ ¬M � ¬P ¬M Δ3 = (D3,W3), W3 = W1, D3 = , . This theory has two extensions again, and in both of them, ¬(M ∧ P) can be inferred. Further, suppose that we have the following additional facts: 4. If Bill attends the meeting, then Peter attends. 5. Bill attends the meeting. Then, the sentence “Peter attends the meeting” can be inferred in the last two translations, but not in the first translation. Much work on default logic have been reported in journals. If you prefer to start with a book; see Besnard (1989).

402 CHAPTER 12. SOME OTHER LOGICS 12.7 AUTOEPISTEMIC LOGICS It is possible to have a knowledge base which has information about the scope and limitations of its own knowledge. For instance, in a database system, we often use the so-called closed world assumption, where “not” is interpreted as “not in the database”. It is a built-in metaknowledge about the database. More flexible knowl- edge bases should have the ability to determine explicitly whether the knowledge of the base about a particular object in the base is in some sense complete or not. In such a scenario, we do not have to think about many agents and their knowledge or belief about facts stored in the base. We would rather have a formalization of the phrases such as “it is known that”, or “it is believed that” as operators. Writing �p for “it is believed (known) that p”, the logic K45 would be an appro- priate logic. This is so because the K45 axioms �(p → q) → (�p → �q), �p → ��p, ¬ �p → �(¬ �p) capture the functionality of the operator � here. However, new beliefs change an ear- lier conclusion; thus we require a nonmonotonic logic to deal with this operator. In this section, we briefly discuss such a nonmonotonic logic of knowledge and belief. The requirement of nonmonotonicity is made clearer in the following example. EXAMPLE 12.3. Let p be the proposition: “Sam has died in the ongoing war”. First, if p holds, then I also believe it, i.e., p → �p. Next, suppose that I do not believe in a statement if I do not have any basis for such a belief. Hence I have the sole premise p → �p. Due to the absence of any information regarding Sam’s death, I do not believe that Sam has died in the ongoing war, i.e., I have ¬ �p. Since p → �p is equivalent to ¬ �p → ¬p, I conclude that ¬p. That is, Sam has not died in the ongoing war. However, if I have the information that Sam has, indeed, died, then I have two premises, p and p → �p, from which I conclude �p. Note that I have now p instead of the earlier conclusion ¬p, which was inferred in the absence of any information in the knowledge base. This is the kind of nonmonotonicity involved in a logic of belief or knowledge. Such a logic is called an autoepistemic logic. Syntactically, the formulas of an autoepistemic logic are the modal propositions of K; the semantics differs. Denote by L, the mps of K, which are now our building blocks for an autoepis- temic logic. For simplicity, omit the symbols ↔ and ♦; they can be introduced with the help of definitions such as p ↔ q � (p → q) ∧ (q → p) and ♦p � ¬ �¬p. A subset T ⊆ L is called an autoepistemic theory. An autoepistemic interpre- tation of an autoepistemic theory T is a function I : L → {0, 1} satisfying (a) I conforms with a PL-interpretation. (b) I(�p) = 1 iff p ∈ T. An autoepistemic interpretation I is an autoepistemic model of T if I(p) = 1 for each p ∈ T. In such a case, we also say that p is true in I. As usual, an autoepistemic theory T is called semantically complete if T contains each formula that is true in each model of T. Similarly, the theory T is called sound with respect to a set of

12.7. AUTOEPISTEMIC LOGICS 403 premises A ⊆ L if every autoepistemic interpretation of T , which is a model of A is also a model of T. Due to the absence of monotonicity, it is not easy to define the notion of a con- sequence. However, as in default logic, extensions would give rise to some closure conditions which can be used to define the set of all consequences of a theory. Instead of defining a “closure of a theory”, we will give a name to a theory which is equal to its closure. A stable theory is an autoepistemic theory satisfying the following conditions: 1. If q1, . . . , qn ∈ T and {q1, . . . , qn} �PL q, then q ∈ T. 2. If q ∈ T, then �q ∈ T. 3. If q �∈ T, then ¬ �q ∈ T. It can be proved that an autoepistemic theory is semantically complete iff it is stable. However, stability is silent about what is not believed; hence, soundness with respect to a set of premises cannot be achieved under mere stability. The initial premises must be included somewhere. Suppose that A is a set of premises (formu- las). A theory T is grounded in A if T ⊆ �q : A ∪ {�p : p ∈ T } ∪ {¬ �p : p �∈ T } �PL q�. That is, T is grounded in A iff T is stable and it does not contain any formula which is not a PL-consequence of a stable extension of A. It can be shown that a theory T is sound with respect to A iff T is grounded in A. Now, using both soundness and completeness, we arrive at the notion of a stable expansion of a theory. An autoepistemic theory T is a stable expansion of a set of premises A iff T is a superset of A that is stable and grounded in A, that is, T = {q : A ∪ {�p : p ∈ T } ∪ {¬ �p : p ∈� T } �PL q}. A stable expansion contains all autoepistemic conclusions of the premises in A. This means, ‘whatever that can be believed when all the formulas in A are believed’ are in the stable expansion. Does there exist always a stable expansion? Is it unique? EXAMPLE 12.4. Let A = {¬ �p → p : p is any formula }, and let T be a stable autoepistemic theory that contains the formula ¬ �p → p. If p �∈ T, then due to stability, ¬ �p ∈ T. Since ¬ �p → p ∈ T, we have p ∈ T. Hence, p ∈ T. If T is grounded in A, then T contains the PL-consequences of the set {¬ �p → p : p is any formula} ∪ {�p : p ∈ T } ∪ {¬ �p : p ∈� T }. Since p ∈ T, �p ∈ T, we have ¬ �p �∈ T ; otherwise, we have p �∈ T, resulting in a contradiction. However, ¬ �p ∈� T implies that ¬ �¬ �p ∈ T. Again, ¬ �¬ �p → ¬ �p ∈ A implies ¬ �p ∈ T as a PL-consequence. The con- tradiction ¬ �p ∈ T and ¬ �p ∈� T shows that T cannot be grounded in A. Therefore, there is no stable expansion of A. EXAMPLE 12.5. Let A = {¬ �p → q, ¬ �q → p}. Let T be any stable expansion of A. The first element of A says that if p is not believed then q holds, and the second one asserts that if q is not believed then p holds. Now, if p �∈ T , then q ∈ T ; and if q �∈ T, then p ∈ T. Then there can be two stable expansions of T ; one containing p but not q, and the other containing q but not p.

404 CHAPTER 12. SOME OTHER LOGICS These examples show that stable expansions may not exist; and even if one exists, it need not be the only stable expansion. Note that a stable expansion in A formal- izes the notion of all consequences of the premises in A. Thus, even if a theory is consistent, there may not be any conclusion, and even if there are conclusions, the set of all conclusions need not be unique. The status of theorem-hood with axioms in A is doubtful. However, this is pragmatic since belief in some statements need not conclusively guarantee other beliefs. An alternative is to regard the intersection of all stable expansions as the set of all beliefs one may have. That is, any statement which is in every stable expansion of a theory grounded in a set of premises A can be regarded as theorems of A. This will be the view of an external observer about the agent. Also, in such a case, an empty intersection will lead to a definition of an inconsistent autoepistemic theory grounded in a set of premises. There is a deep connection between default logic and autoepistemic logics. You may approach both the topics from applications point of view; see Baral (2003). 12.8 SUMMARY This chapter briefly reviews some of the logics that have been in use for quite some time. You can start from the edited text Smets et al. (1998) to get an overall picture of nonstandard logics having some general frameworks and then go through the topics that interest you in Gabbay & Guenthner (2002). We have not reviewed many logics which are in current use. One of them is the description logic. It is a restricted fragment of first order logic used for modelling relationships between various entities found on the web. In a description logic one uses constants, unary predicates and binary predicates, all finite in number. These are used to represent relations about the individuals named by constants, the classes named by unary predicates, and the roles or properties named by binary predicates. You may start from the introductory article Kro¨tzsch et al. (2013) and go through the references quoted there for a comprehensive account of description logics.

References Andrews, P. B. (1970), ‘Resolution in type theory’, J. Symbolic Logic, 36, 414–432. Apt, K. R. & Olderog, E.-R. (1991), Verification of Sequential and Concurrent Programs, Springer-Verlag, New York. Backhouse, R. C. (1986), Program Construction and Verification, Prentice Hall, Englewood Cliffs, N.J. Baral, C. (2003), Knowledge Representation, Reasoning and Declarative Problem Solving, Cambridge University Press, Cambridge. Barwise, J. & Etchemendy, J. (1999), Language, Proof and Logic, CSLI Publica- tions, Stanford. Besnard, J. (1989), An Introduction to Default Logic, Springer-Verlag, New York. Bilaniuk, S. (1999), A Problem Course in Mathematical Logic, Unpublished Note, [email protected]. Boole, G. (1951), An Investigation of the Laws of Thought, Dover, (Reprint of Walton & Maberley, 1854), New York. Boolos, G. (1979), The Unprovability of Consistency: An Essay in Modal Logic, Cambridge University Press, Cambridge. Boolos, G., Burgess, J., Richard, P. & Jeffrey, C. (2007), Computability and Logic, Cambridge University Press, Cambridge. Chang, C. L. & Lee, R. C. T. (1973), Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York. Chellas, B. F. (1980), Modal Logic-An introduction, Cambridge University Press, Cambridge. Copi, I. M. (1979), Symbolic Logic, Macmillan, London. Copi, I. M., Cohen, C., Prabhakar, M. & Jetli, P. (2010), Introduction to Logic, Pearson, Delhi. 405

406 REFERENCES Davis, M. D. & Putnam, H. (1960), ‘A computing procedure for quantification theory’, J. ACM 7, 210–215. Dijkstra, E. W. (1976), A Discipline of Programming, Prentice Hall, Englewood Cliffs, N.J. Dijkstra, E. W. (1982), Selected Writings on Computing: A personal perspective, Springer-Verlag, New York. Dowling, W. F. & Gallier, J. H. (1984), ‘Linear time algorithms for testing the satisfiability of propositional horn formulas’, Journal of Logic Programming, 3, 267–284. Doyle, J., Sandewall, E. & Torassi, P., eds (1994), Proc. Fourth International Conference on Principles of Knowledge Representation and Reasoning, Morgan Kaufmann. San Fransisco. Du, D., Gu, J. & Pardalos, P. M. (1997), Satisfiability Problem : Theory and applications, (Ed.) American Mathematical Society, Providence. AMS DIMACS Series : Vol.35. Dubois, D., Farreny, H. & Prade, H. (1985), ‘Sur divers proble´ms inhe´rents a´ l’ automatisation des raisonnements de sens commun’, Congre´s AFCET-RFIA, Grenoble 1, 321–328. Dummett, M. (1977), Elements of Intuitionism, Clarendon Press, Oxford. Ebbinghaus, H. D., Flum, J. & Thomas, W. (1994), Mathematical Logic, 2nd ed., Springer, New York. Enderton, H. B. (1972), A Mathematical Introduction to Logic, Academic Press, New York. Epstein, R. L. (2001), Propositional Logics: The Semantic Foundations of Logic, Wadsworth, Belmont, USA. Ershov, Y. L. & Palyutin, E. A. (1984), Mathematical Logic, Mir Publishers, Moscow. Fagin, R., Halpern, J. Y., Moses, Y. & Vardi, M. Y. (1995), Reasoning about Knowledge, MIT Press, Cambridge, USA. Fitting, M. (1993), Basic modal logic, in D. Gabbay, C. Hogger & J. Robinson, eds, ‘Handbook of Logic in Artificial Intelligence and Logic Programming’, Vol. 1, Oxford University Press, Oxford. Fitting, M. (1996), First Order Logic and Automated Theorem Proving, Springer- Verlag, New York. Fitting, M. & Mendelson, R. L. (1998), First Order Modal Logic, Kluwer Academic Publishers, Dordrecht, The Netherlands.

REFERENCES 407 Francez, N. (1992), Program Verification, Addison-Wesley, Reading, USA. Frege, G. (1934), Die Grundlagen der Arithmetik, Eine logischmathematische Untersuchung u¨ber der Begriff der Zahl., Breslau, Reprinted Marcus, Breslau. Frege, G. (1984), ‘Collected papers on mathematics, logic, and philosophy’, Oxford. Ed. by M. Mc. Guninness. Gabbay, D. M. & Guenthner, F. (2002), Handbook of Philosophical Logic, 2nd ed., Vol. 1-9, Kluwer Academic Publishers, Dordrecht, The Netherlands. Gallier, J. H. (1987), Logic for Computer Science: Foundations of Automatic Theorem Proving, John Wiley & Sons, New York. Garey, M. R. & Johnson, D. S. (1979), Computers and Intractability: A Guide to the Theory of NP-completeness, Freeman, New York. Gentzen, G. (1936), ‘Die widerspruchsfreiheit der reinen zahlentheorie’, Mathemais- che Annalen, 12, 493–565. Glivenko, V. (1929), ‘Sur quelques points de la logique de m. brouwer’, Acade´mie Royale de Belgique, Bulletins de la Classe des Sciences, Ser. 5, 15, 183–188. Goldblatt, R. (1987), Logics of Time and Computation, CSLI Publications, Stanford. Gries, D. (1981), The Science of Programming, Springer-Verlag, New York. Gries, D. (1982), ‘A note on a standard strategy for developing loop invariants and loops’, Science of Computer Programming, 2, 207–214. Gries, D. & Schneider, F. B. (1993), A Logical Approach to Discrete Math, Springer- Verlag, New York. Haken, A. (1985), ‘The intractability of resolution’, Theoretical Computer Science, 39, 297–308. Halpern, J. Y. (1990), ‘An analysis of first order logics of probability’, Artificial Intelligence, 46, 311–350. Hehner, E. C. R. (1984), The Logic of Programming, Prentice Hall, Englewood Cliffs, N.J. Hoare, C. A. R. (1969), ‘An axiomatic basis for computer programming’, Comm. ACM, 12, 576–580,583. Hodges, W. (1993), Model Theory, Cambridge University Press, London. Hughes, D. E. & Cresswell, M. J. (1971), An Introduction to Modal Logic, Methuen, New York. Huth, M. & Ryan, M. (2000), Logic in Computer Science: Modelling and reasoning about systems, Cambridge University Press, Cambridge.

408 REFERENCES Jones, C. B. (1980), Software Development: A Rigorous Approach, Prentice Hall, Englewood Cliffs, N.J. Kowalski, R. (1979), Logic for Problem Solving, Elsevier, Amsterdam. Kro¨tzsch, M., Simancik, F. & Horrocks, I. (2013), A description logic primer. arXiv:1201.4089v3 [cs.AI]. Lemmon, E. J. (1977), An Introduction to Modal Logic, Basil Blackwell, Oxford. Ed. N. Rescher, Monograph No.11, American Philosophical Quaterly Monograph series. Lewis, C. I. (1918), A Survey of Symbolic Logic, Dover, New York. Lewis, C. I. & Langford, C. H. (1938), Symbolic Logic, Century, New York. Loveland, D. W. (1979), Automated Theorem Proving: A logical basis, Elsevier, Amsterdam. Łukasiewicz, J. (1970), ‘Selected works’, North Holland, Amsterdam. Ed. by L. Borkowski. Manaster, A. B. (1978), Completeness, Compactness and Undecidability: An Introduction to Mathematical Logic, PHI Learning, New Delhi. Manin, Y. I. (1977), A Course in Mathematical Logic for Mathematicians, Springer Verlag, New York. Mates, B. (1972), Elementary Logic, Oxford University Press, New York. Mendelson, E. (1979), Introduction to Mathematical Logic, D. Van Nostrand, New York. Meyer, J. J. C. & van der Hoek, W. (1993), Epistemic Logic for AI and Computer Science, Cambridge University Press, Cambridge. Paulson, L. C. (1991), ML for the Working Programmer, Cambridge University Press, Cambridge. Pelletier, F. J. (1999), ‘A brief history of natural deduction’, History and Philosophy of Logic, 20, 1–31. Popkorn, S. (1994), First Steps in Modal Logic, Cambridge University Press, Cambridge. Post, E. L. (1921), ‘Introduction to general theory of elementary propositions’, American Journal of Mathematics, 43, 163–185. Quine, W. V. (1959), ‘On cores and prime implicates of truth functions’, American Math. Monthly, 66, 755–760. Rasiowa, H. & Sikorski, R. (1970), The Mathematics of Metamathematics, 3rd ed., Polish Scientific Pub., Warschau.

REFERENCES 409 Rautenberg, W. (2010), A Concise Introduction to Mathematical Logic, 3rd ed., Springer, New York. Reiter, R. & de Kleer, J. (1987), ‘Foundations of assumption based truth maintenance systems : Preliminary report’, Proc. AAAI-87 . Reynolds, J. C. (1981), The Craft of Programming, Prentice Hall, Englewood Cliffs, N.J. Robinson, A. (1996), Nonstandard Analysis, Princeton University Press, New Jersey, USA. Robinson, J. A. (1979), Logic: Form and Function, Elsevier, New York. Robinson, J. A. & Wos, L. (1969), ‘Paramodulation and theorem proving in first order logic with equality’, Machine Intelligence, 4, 135–150. Schmidt, D. A. (1994), The Structure of Typed Programming Languages, MIT Press, Cambridge, USA. Selman, B. & Kautz, H. (1991), Knowledge Compilation using Horn Approximation, (Ed.) Proc. Ninth National Conference on Artificial Intelligence, Anaheim, CA. Shoenfield, J. R. (1967), Mathematical Logic, Addison Wesley, Reading, USA. Singh, A. (1999), ‘Computing prime implicants via transversal clauses’, Int. J. Computer Math., 70, 417–427. Singh, A. (2009), Elements of Computation Theory, Springer-Verlag, London. Singh, A. & Goswami, C. (1998), Fundamentals of Logic, Indian Council of Philosophical Research, New Delhi. Smets, P., Mamdani, A., Dubois, D. & Prade, H. (1998), Non-standard Logics for Automated Reasoning, Academic Press, New York. Smullyan, R. M. (1968), First Order Logic, Springer-Verlag, New York. Smullyan, R. M. (1978), What is The Name of This Book?, Prentice Hall, Englewood Cliffs, N.J. Smullyan, R. M. (1983), The Lady or the Tiger and the Other Logical Puzzles, Penguin Books, Harmondsworth, UK. Smullyan, R. M. (2014), A Biginner’s Guide to Mathematical Logic, Dover Pub. Inc., New York. Snyder, D. P. (1971), Modal Logic and its Applications, Van Nostrand Reinhold Company, New York. Sperchneider, V. & Antoniou, G. (1991), Logic, a Foundation for Computer Science, Addison Wesley, Reading, USA.

410 REFERENCES Srivastava, S. M. (2013), A Course on Mathematical Logic, 2nd ed., Springer (Universitext), New York. Stoll, R. R. (1963), Set Theory and Logic, W.H. Freeman, New York. Suppes, P. (1957), Introduction to Logic, Van Nostrand, Princeton, N.J. Tanaka, K. (1996), An Introduction to Fuzzy Logic for Paractical Applications, Springer-Verlag, New York. Tarski, A. (1944), ‘The semantic conception of truth’, Philosophy and Phenomeno- logical Research, 4, 341–376. Tennent, R. D. (1991), Semantics of Programming Languages, Prentice Hall, Englewood Cliffs, N.J. Tison, P. (1967), ‘Generalization of consensus theory and application to the minimization of boolean functions’, IEEE Trans. on Elec. Comp., EC-16(4), 446–456. Turner, T. (1991), Constructive Foundations for Functional Languages, McGraw-Hill, New York. van Dalen, D. (1989), Logic and Structure, Springer-Verlag (Universitext), New York. van Heijenoort, J. (1967), From Frege to Go¨del: A Source Book in Mathematical Logic 1879-1931, Ed. Harvard University Press, Cambridge, USA. Wittgenstein, L. (1922), Tractatus Logico Philosophicus, Kegan & Paul, London. Translated by C.K. Ogden. Wo´jcicki, R. (1998), Theory of Logical Calculi, D. Reidel, Dordrecht, The Netherlands.

Index B-support, 102 Atomic proposition, 3 F-valid, 369 Atoms, 3 A, 313 Autoepistemic L3, 392 wp , 292 interpretation, 402 kSAT, 81 logic, 402 kcnf, 81 model, 402 FORM, 199 soundness, 402 SAT, 81 theory, 402 3SAT, 82 Axiom K, 354 Axiom of PC, 36 Abbreviated formula, 138 Axiom schemes, 307 Accessibility relation, 345 of FC, 168 Adequacy of of KC, 354 of PC, 36 FND, 243 Bacus-Naur form, 3 FT, 259 Biform literal, 87 GFC, 247 Biform variable, 87 GPC, 116 Binary search, 290 PT, 126 BNF, 3 Adequate set of connectives, 77 Body, 270 Admissible substitution, 140 Boolean Agree, 153 expression in CL, 268 Alphabet of function, 78 FL, 132 valuation, 13 PL, 3 variable, 70, 78 Applying a substitution, 214 Boolean conditions, 12 Arbitrarily large model, 188 Bound, 269 Arithmetic, 313 by a quantifier, 135 Arity, 132 occurrence, 135 Assignment variable, 135 axiom, 275 Branching proposition, 118 function, 141 Branching rules, 113, 118, 363 statement, 269 Calculation, 103, 237 Assumption schemes, 369 Calculational proof, 104 Atomic formula, 133 411

412 INDEX Canonical model, 358 Characteristic function, 396 Crisp predicate, 396 Church-Turing thesis, 325 CTL, 380 Closed Debugging, 264 formula, 136 Declarative version, 5 path, 118 Deductively closed, 68 path for K, 364 Deductive closure, 68 tableau, 118 Default, 399 tableau for K, 364 term, 133 extension, 400 world assumption, 231, 402 theory, 399 cnf, 72, 211 Definable relation, 332 Coloring, 185 Denial, 99 Compactness, 55, 184 Derivation in KC, 358 Complement, 78 Derived rules, 40 Complementary Literal, 72 Deviant logics, 387 Completed path, 118 Disjunctive clause, 72, 211 Completed tableau, 118 Disjunctive normal form, 72 Completeness dnf, 72, 211 for PC, 54 Domain, 142 of FC, 183 Domain of a structure, 306 of FT, 258 DPLL, 97 of resolution, 92 DT, 26, 41, 156, 172 Complete path, 118 Dual, 99 Composition, 269 Composition of substitutions, 215 EG, 193 Compound formula, 133 Eigenvariable condition, 245 Compound proposition, 3, 118 Elementarily equivalent, 339 Computation tree logic, 380 Empty sequent, 111 Conclusion, 20, 39 enf, 100 Conditional statement, 269 Entails, 20, 118, 150 Conjunctive clause, 72, 211 Equality Conjunctive normal form, 72 Connectives, 3, 132 axioms, 158 Consequence, 20, 358 rules in FT, 250 Consequent, 399 sentences, 159 Consistent Equivalence in K, 351 in KC, 357 Equivalent in PC, 42 in FL, 150 in PND, 107 in PL, 20 set in FC, 172 states, 166 set in FT, 256 valuations, 166 set in PT, 118 Equivalently replaced with, 61 Contingent, 17 ES, 193 Contradiction, 17 Exclusive or, 99 Correspondence theory, 369 Exclusive or Normal form, 100 Exclusive sum, 78 Existential

INDEX 413 closure, 155 Go¨del number, 329 formula, 250, 337 Go¨del numbering, 329 quantifier, 132 Generalized consequence, 115 rule, 250 GFC, 245 Expressed by a formula, 331 Ghost variable, 267 Expressible in A, 331 GPC, 111 Expression, 3, 132 Ground Expressions, 329 Extended logics, 387 atomic formulas, 317 instances, 235, 318 Factor of a clause, 223 literals, 317 Falsifies, 17, 143, 154, 346 terms, 235, 316 FC, 168 Grounded theory, 403 fcnf, 211 Guard, 270 fdnf, 211 Finitely generated tree, 56, 123 Has colour, 185 Finite model property, 328 Herbrand Finite state-model, 143 First order language, 305 base, 317 First order theory, 307 expansion, 318 Flagged variable, 196 interpretation, 317 FND, 240 map, 317 Follows from, 20 model, 317 Formation rules, 3 universe, 316 Formula, 133, 402 Hintikka set, 53, 181 Four colour theorem, 56 Hoare Frame, 345 logic, 280 Frame properties, 370 proof, 280 Free proof tree, 281 triple, 267 for a variable, 139 Horn clause, 84, 230 occurrence, 135 Horn formula, 84 universe, 255 Hypothesis, 20 variable, 135 FT, 250 IC, 49 Functional Identity, 132 cnf, 211 Immediate sub-proposition, 9 dnf, 211 Inconsistent form, 209 normal form, 211 in GPC, 113 standard form, 211 in PC, 42 Function symbol, 132 in PND, 107 Fundamental clause, 94 set in FC, 172 Fuzzy subset, 396 set in FT, 256 set in PT, 118 G, 370 Independence of axioms, 68 Go¨del logic, 370 Indeterminate proposition, 392 Indical function, 206, 396 Individual constants, 132

414 INDEX Inductive construction, 5 Logical Infinitesimal, 188 constants, 16 Infinite state-model, 143 symbols, 305 Infinity, 188 variable, 267 Instance of PCP, 325 Integer expression in CL, 268 Logic gates, 79 Interpolant, 100, 338 Logic of knowledge, 376 Interpretation, 12, 142, 306 Invalid, 17, 149 M, 25, 43, 156, 172 Invariant, 271, 277 Main connective, 9 Isomorphic, 338 Marriage condition, 57 Match in a PCP, 325 Justifications, 399 Matrix of, 201 Maximally K-calculus, 354 K-valid, 350 consistent, 51 KC, 354 consistent in KC, 357 KND, 360 inadequate, 99 Knowledge compilation, 76 Membership function, 397 Kowalski form, 230 MFC, 200 KT, 364 mgu, 219 Miniscope form, 338 Law Modal ∧-distributivity, 294 atomic formula, 343 �-distributivity, 294 atomic proposition, 343 →-distributivity, 294 prefix, 363 ¬-distributivity, 294 proposition, 343 ∨-distributivity, 294 Modality Excluded miracle, 294 alethic, 375 FL, 192 deontic, 375 in K, 350 doxastic, 375 of trivalence, 392 temporal, 375 PL, 62 Model, 17, 20, 154 Termination, 294 based on a frame, 369 checkers, 384 Lemma finite, 154 Diagonalization, 330 infinite, 154 Ko¨nig’s, 56, 124 of K, 346 Lindenbaum, 53, 357 Monochromatic, 185 Relevance, for sentences, 155 Monotone circuit, 81 Relevance, in FL, 152 Monotonic logics, 388 Relevance, in PL, 14 Most general unifier, 218 Substitution, 144 mp, 343 Truth, 358 Names, 132 Length of a proposition, 82 NAND, 78 Level of a term, 133 Natural deduction system, 106 Literal, 19, 72, 211 Necessitation, 354

INDEX 415 Possible world semantics, 385 Necessity rules, 364 Post’s correspondence problem, 325 Negation Postcondition, 266 Precedence rules, 10 as failure, 231 Precondition, 266 complete, 54 Predicate, 132 complete set, 339 Prefixed mp, 363 normal form, 99, 234 Prefix of, 201 New Premise, 20, 39, 118, 250 constant, 194, 251 Prenex form, 201, 211 term, 250 Prenex normal form, 211 variable, 245 Prerequisite, 399 nnf, 99, 234 Prime implicant, 76 Nonfundamental clause, 94 Prime implicate, 76 Nonlogical constants, 16 Procedure Nonlogical symbols, 305 Nonstandard model, 188 CompSub, 215 Nontrivial clause, 94 HornSat, 85 NOR, 78 NorFor, 73 PrenForm, 202 Open PropDet, 8 formula, 136 QuaEli, 206 path, 118 TwoSat, 83 path for K, 364 Unify, 218 tableau, 118 Product, 78 Product structure, 337 Outfix notation, 29 Program Binary search, 291 Paramodulant, 224 specification, 267 Paramodulation, 224 state, 266 Parent clauses, 221 StringMatching, 264 Parse tree, 4 termination, 265 Partially correct, 273 variable, 266 Partial correctness, 265 Proof Path, 56 by calculation, 237 Path in a tableau, 118 in FC, 169 PC, 37 in KC, 354 pcnf, 211 in MPC, 130 PCP, 325 in PC, 37 PCS, 325 in PND, 107 pdnf, 211 of an FC-consequence, 169 Peano’s arithmetic, 313 of a PC-consequence, 39 PL, 3 of a sequent, 113 PL-formulas, 3 of partial correctness, 280 Place, 13 summary, 282 PND, 106 Prop, 3 PND-deduction, 107 Propositional Polish notation, 29 Possibility rules, 364

416 INDEX constants, 3, 132 Rule of knowledge base, 76 binary resolution, 229 language, 16 composition, 276 theory, 76 conditional statement, 276 variable, 3 full resolution, 229 Provability predicate, 334 global assumption, 365 Provable implication, 276 consequence, 39, 169 inconsistency, 49 in FC, 169 inference of FC, 169 in KC, 354 inference of GPC, 111 in PC, 37 inference of KC, 354 in PND, 107 inference of PC, 36 sequent, 113 Leibniz, 62 PT, 117 local assumption, 365 Punctuation marks, 132 resolution, 88 Pure literal, 96 sequential execution, 276 total while, 289 QualEli-∀, 209 while, 277 Quantifiers, 132 Quasi-proof, 64, 195 S4, 371 S5, 371 RA, 26, 43, 156, 173, 279 Satisfiability form, 210 Rank, 30 Satisfiable, 17, 20, 149, 150 RC, 279 Satisfiable path, 257 Rectification, 201 Satisfied, 273 Rectified formula, 201 Satisfies, 17, 143, 154, 346, 348 Reflexive frame, 369 scnf, 211 Residue of subsumption, 95 Scope, 135 Resolution sdnf, 211 Semantically complete, 402 DAG, 89 Semantic tree, 117 method, 226 Semi-decidable, 328 proof, 89, 226 Sentence, 136 refutation, 89, 226 Sentential forms, 210 Resolvent, 87, 221 Separating variant, 217 Resolvent closure, 92 Sequent, 111 Resolving upon, 87 Sequential control, 269 Result of a substitution, 214 Sequent rules, 111 RI, 279 Signature, 16, 305 RPL, 88 Situation, 13 RS, 279 Skolem Rule BP, 355 cnf, 211 GA, 365 dnf, 211 LA, 365 form, 206 R, 355 function, 206 RW, 279 normal form, 211

INDEX 417 Completeness of KC, 358 standard form, 211 Completeness of PC, 54 term, 206, 233 Correspondence, 370 Skolemization, 206 Craig’s interpolation, 100, 338 Soundness Deduction for L3, 393 of FT, 258 Deduction for FC, 172 of PC, 51 Deduction for FL, 156 of resolution, 92 Deduction for K, 353 Stable expansion, 403 Deduction for PC, 41 Stable theory, 403 Deduction for PL, 26 Stacking proposition, 118 Equality, 161 Stacking rules, 113, 118, 363 Equivalence replacement in FL, 190 State, 13, 143 Equivalence replacement in K, 351 State-model, 143, 150 Equivalence replacement in PL, 61 Strongly entails, 351 Existential generalization, 193 Structure, 306 Existential specification, 193 Subformula, 135 Finiteness for FC, 173 Sublogic, 370 Finiteness for PC, 44 Subproposition, 9 Finiteness of PT, 124 Substitution, 139, 214 Functional form, 210 Substructure, 337 Fundamental invariance, 303 Subsumption, 95 Go¨del’s first incompleteness, 333 Sum, 78 Go¨del’s second incompleteness, 334 Systematic tableau, 122, 255 Hall’s marriage, 58 Słupecki operator, 393 Herbrand’s, 322 Infinite Ramsey, 185 Tableau Laws in FL, 192 derivation, 366 Laws in K, 350 first order, 250 Laws of PL, 62 for a proposition, 118 Model existence, 182 for a set, 118 Model existence for PC, 54 proof for K, 364 Monotonicity for FC, 172 propositional, 117 Monotonicity for FL, 156 rules for K, 363 Monotonicity for K, 353 theorem for K, 364 Monotonicity for PC, 43 Monotonicity for PL, 25 Tautological clause, 94 Normal form, 72 Tautology, 17, 190 of FC, 169 Temporal logic, 377 of GPC, 113 Term, 132 of KC, 354 Theorem of PC, 37 of PND, 107 Adequacy of PND, 110 of PT, 118 Adequacy of resolution, 94 Paradox of material implication, 25, Beth’s definability, 338 Biconditional replacement in K, 355 156 Closure property of resolution, 93 Prenex form, 202 Compactness of FL, 184 Compactness of PL, 55

418 INDEX Prenex normal form, 211 assignment, 12 Ramsey, 186 function, 18, 70 functionally complete, 77 Reductio ad absurdum for FC, 173 Reductio ad absurdum for FL, 156 Truth table, 12 Reductio ad absurdum for PC, 43 Truth values, 11 Reductio ad absurdum for PL, 26 TW, 289 Regularity, 355 Resolution principle, 88, 222 UG, 193 Sentential form, 210 Ultrafilter, 59 Skolem, 189 Undecidability of FL, 327 Skolem-Lo¨wenheim, 200, 323 Underlying frame, 346 Skolem-Lo¨wenheim upward, 189, 324UUnniififiearb,le21c7lause, 217 Skolem Form, 234 Uniformly replaced with, 60 Skolem form, 207 Uniform replacement, 48, 191 Soundness of KC, 357 Unit resolution, 102 Standard form, 211 Universal Strong adequacy of FC, 183 Strong adequacy of FND, 243 closure, 155 Strong adequacy of FT, 259 formula, 250, 337 Strong adequacy of GFC, 247 quantifier, 132 Strong adequacy of GPC, 116 rule, 250 Strong adequacy of PT, 126 sequent, 111 Strong completeness of FT, 258 Universe, 142 Strong generalization, 176 Unsatisfiable, 17, 149 Strong soundness of FC, 177 US, 193 Strong soundness of FT, 258 Vague predicate, 396 Strong soundness of PC, 51 Syntactic interpretation, 321 Valid, 17, 149 consequence in K, 351 Tarski’s, 331 in a frame, 369 Tautological replacement, 191 in K, 350 Tautological replacement in K, 350 Validity form, 210 Turing’s Undecidability, 327 Valuation, 13, 141, 143 Ultrafilter, 59 Uniform replacement, 191 Variables, 132 Variable capturing, 139 Uniform replacement in PL, 60 Variant, 217, 288 Unique parsing in FL, 134 Unique parsing in K, 344 Verification condition, 283 Verifies, 17, 143, 346, 348 Unique parsing in PL, 6 Universal generalization, 193 Weakest precondition, 292 Universal specification, 193 Weakly entails, 351 Theory of a structure, 306 wff, 3 Totally correct, 288 World, 13, 344 Total correctness, 265 World truth mapping, 346 Trivial clause, 94 XOR, 99 True at a world, 345, 346 Truth ZFC, 310