Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

A Kotas-Style Characterisation of Minimal Discussive Logic

A Kotas-Style Characterisation of Minimal Discussive Logic axioms Article A Kotas-Style Characterisation of Minimal Discussive Logic 1, ,† 2, ,† Krystyna Mruczek-Nasieniewska * and Marek Nasieniewski * Department of Logic, Nicolaus Copernicus University in Torun, ´ ul. Moniuszki 16/20, 87-100 Torun, ´ Poland * Correspondence: mruczek@umk.pl (K.M.-N.); mnasien@umk.pl (M.N.) † These authors contributed equally to this work. Received: 26 August 2019; Accepted: 27 September 2019; Published: 1 October 2019 Abstract: In this paper, we discuss a version of discussive logic determined by a certain variant of Jaskowski’s ´ original model of discussion. The obtained system can be treated as the minimal discussive logic. It is determined by frames with serial accessibility relation. As the smallest one, this logic can be treated as a basis which could be extended to richer discussive logics that are obtained by varying accessibility relation and resulting in a lattice of discussive logics. One has to remember that while formulating discussive logics there is no one-to-one determination of discussive logics by modal logics. For example, it is proved that Jaskowski’s ´ logic D can be expressed by other than S5 modal logics. In this paper we consider a deductive system for the sketchily described minimal logic. While formulating the deductive system, we apply a method of Kotas that was used to axiomatize D . The obtained system determines a logic D as a set of theses that is contained in D . Moreover, 2 0 2 any discussive logic that would be expressed by means of the provided model of discussion would contain D , so it is the smallest discussive logic. Keywords: discussive logics; the smallest discussive logic; discussive operators; seriality; accessibility relation; Kotas’ method; modal logic 1. Introduction Stanisław Jaskowski’s ´ aim was to propose a calculus that would allow for explication of inconsistent theories by means of some consistent framework. As a result Jaskowski ´ developed a logic denoted as D that was meant to be a basis for calculus that would not lead in general to overfull set of conclusions when applied to inconsistent set of premisses. He used the scenario of a discussion as a model case. Intuitively, during discussions participants can contradict each other, but a possible external observer as well as particular participants would not conclude that everything follows from such discussion. (Some analysis on this matter can be found in [1].) Interactions that take place between participants of a discussion are expressed formally by discussive counterparts of implication, conjunction and equivalence. Moreover, in Jaskowski’s ´ intuitive model, operators take only auxiliary role and modal operators are not present in the object language of the discussive logic. Such a variant seems to be natural and has been considered in [1]. Our aim is to indicate the weakest logic that arises from a natural variant of Jaskowski ´ model of discussion and moreover, give an adequate deductive system for such a logic. 2. D and the Minimal Variant of Discussive Logic In the original formulation, Jaskowski ´ considered a situation in which there is no restriction on possible reactions of participants of a discussion, in other words he considered a model, where every two participants of the discussion are connected. It corresponds to the full accessibility relation that semantically allows to determine the logic S5. However, it is known that not every thesis is in fact used Axioms 2019, 8, 108; doi:10.3390/axioms8040108 www.mdpi.com/journal/axioms Axioms 2019, 8, 108 2 of 17 or needed to express discussive theses. What is only used, is the so-called M-counterpart of the logic S5 (for investigations on this notion see [2]). In various papers it has been shown (see [3–7]) that to be able to formulate D , one can use various modal logics. (Jaskowski’s ´ logic was meant to be a basis for a consequence relation and also in this case there can be given other systems than S5 which also allow to express D -consequence relation (see [8]).) Moreover, one can introduce a general discussive consequence relation framework, in which D would be the set of theses of one of its special cases (for details see [9]). However, this does not mean that any modal logic would be equally good to obtain D . We will keep original Jaskowski’s ´ meaning of discussive connectives of implication and conjunction. Jaskowski’s ´ discussive implication denoted here as ! , is meant to be read as “if anyone states that p, then q” (see [10] p. 150, 1969), in modal terms: p ! q. Discussive conjunction is usually interpreted as saying “p and someone said q”, in the modal Jaskowski’s ´ interpretation it is read as p ^ q. (The disjunction conjunction was introduced in the second Jaskowski ´ paper on discussive logic [11].) In both cases is originally interpreted as possibility that can refer to any participant of discussion. In our interpretation it will refer only to those participants, who are connected by the accessibility relation. In particular, it means that statements of participants, who are not connected to any disputant, make the whole discussion (since we are interested in expressing what logically follows, so we ought to consider each world — or in the nomenclature of the model of the discussion — each point of view) meaningless. As Jaskowski ´ says, every thesis of the discussive system during its interpretation ought to be preceded by the reservation: “in accordance with the opinion of one of the participants in the discourse”, so “if a thesis is recorded in a discursive system, its intuitive sense ought to be interpreted so as if it were preceded by the symbol Pos” ([10] p. 149, 1969), which nowadays is denoted standardly by ‘’. Taking into account what has been said, the minimal requirement for the considered model of discussion is that the ‘outer ’ possibility ought to be ruled by a serial accessibility condition. From the formal point of view, the underlying modal logic that will be used for the formulation of the proposed variant of discussive logic, will be the deontic normal logic D. As it is known, it is semantically expressed by the class of frames with serial accessibility relation (where seriality means that for every world w there is a world v such that wRu). To strictly formulate the presented idea we will need two formal languages: modal and discussive. 3. Modal and Discussive Languages Throughout the paper we will use modal formulas that are formed in the standard way from propositional letters: ‘p’, ‘q’, ‘r’, ‘s’, ‘t’, ‘p ’, ‘p ’, ‘p ’, . . . ; truth-value operators: ‘:’, ‘_’, ‘^’, ‘!’, 0 1 2 and ‘$’ (connectives of negation, disjunction, conjunction, material implication and material equivalence, respectively); modal operators: the necessity and possibility operators ‘’ and ‘’; and the brackets. Let For denote the set of all modal formulas. Of course, the set For includes m m the set of all classical formulas (without the use of ‘’ and ‘’), in particular the set of all classical tautologies denoted as CL. The modal language plays only an auxiliary role in the formulation of discussive logic. Its object language is built again from propositional letters, truth-value operators ‘:’ and ‘_’ and discussive implication (! ), discussive conjunction (^ ) and discussive equivalence d d ($ ). The set of all discussive formulas is denoted by ‘For ’. d d 3.1. Basics of Normal Modal Logics A normal modal logic is a set M  For that fulfils the following conditions: 1. CL  M, 2. M is closed under modus ponens (mp), uniform substitution (us) and necessitation rule (rn): if j and (j ! y) belong of M, so does y. (mp) if j 2 M then s(j) 2 M, (us) if j 2 M thenj 2 M, (rn) Axioms 2019, 8, 108 3 of 17 3. M contains formulas (df) and (K) p $ ::p (df) (p ! q) ! (p ! q) (K) As it is known, every normal modal logic contains the following formulas (p ! q) ! (p ! q) (1) (p ! q) ! (p ! q) (2) (p ! q) ! (p ! q) (3) D is the smallest normal logic containing (D): p ! p (D) Standardly, K is the smallest normal modal logic and S5 = KT5, that is, S5 is the smallest normal modal logic containing (T) and (5), where p ! p (T) p ! p (5) 4. Discussive Logics In the original formulation every two participants are connected one to another—in fact, for the explication of discussive implication one reads: ‘if anyone states that p’. The same idea is applied for the modality that is corresponding to possibility expressing the point of view of an external observer. Hence, Jaskowski’s ´ discussive logic D is defined by means of S5 as follows: D := f A 2 For : i (A) 2 S5g , 2 d 1 where i is a translation of discussive formulas into the modal language, that is, i is a function from 1 1 For into For such that: d m 1. i (a) = a, for any propositional letter a, 2. for any A, B 2 For : (a) i (:A) = :i (A), 1 1 (b) i (A _ B) = i (A) _ i (B), 1 1 1 (c) i (A ^ B) = i (A) ^ i (B), 1 d 1 1 (d) i (A ! B) = i (A) ! i (B). 1 d 1 1 (e) i (A $ B) = (i (A) ! i (B)) ^ (i (B) ! i (A)). 1 d 1 1 1 1 One can also consider a more general case. Let S be any normal modal logic. Now, we can define D := f A 2 For : i (A) 2 Sg . (4) S d 1 We easily see that in the case where there is no formula of the form(A) that would belong to a given modal logic S, then we have D = ?. In particular, for any modal logic S that is determined by a class of Kripke frames, whose accessibility relation does not fulfil seriality condition, we obtain D = ?. (We use standard results from modal logic, for details see for example, References [12,13].) Of course, if for a given normal modal logic S, we have (D) 2 S, then D  S. It is known (see Reference [6]) that one can consider various accessibility relations but the resulting discussive logic would be still the same. By definition, D = D . We easily see that S5 2 Axioms 2019, 8, 108 4 of 17 Fact 1. For any modal logics S and S , if S  S , then 1 2 1 2 D  D S S 1 2 By induction on the complexity of a formula j 2 For , we can obtain: Fact 2. For every j 2 For , there is A 2 For such that i (A) $ j 2 K. m d 1 In this paper we focus on the case where in the condition (4), D is taken as the modal system S. We denote the resulting system as D . Thus, by definition D := f A 2 For : i (A) 2 Dg . (5) 0 d 1 In the context of the definition of D , first, let us observe that: Lemma 1. For any A, A , . . . , A 2 For and any variables a , . . . , a , 1 n d 1 n (i (A))(a /i (A ), . . . , a /i (A )) = i (A(a /A , . . . , a /A )) 2 D. n n n n 1 1 1 1 1 1 1 1 Proof. The proof goes by induction on the complexity of a formula A. For the initial case, let A = a . We have: (i (a ))(a /i (A ), . . . , a /i (A )) = i (A ) = i (a (a /A , n n i 1 i 1 1 1 1 1 i 1 i 1 1 . . . , a /A )). If A is a variable that does not belong to fa , . . . , a g, we have (i (A))(a /i (A ), . . . , n n 1 n 1 1 1 1 a /i (A )) = A = i (A(a /A , . . . , a /A )). n n n n 1 1 1 1 For the inductive step assume that inductive hypothesis holds for B and C. For the case of discussive conjunction observe that the following equations hold: (i (B ^ 1 d C))(a /i (A ), . . . , a /i (A )) = (i (B) ^ i (C))(a /i (A ), . . . , a /i (A )) = 1 1 1 n 1 n 1 1 1 1 1 n 1 n (i (B))(a /i (A ), . . . ,a /i (A )) ^ (i (C))(a /i (A ), . . . , a /i (A )). Using n n n n 1 1 1 1 1 1 1 1 1 1 inductive hypothesis and features of substitution, we have (i (B))(a /i (A ), . . . , 1 1 1 1 a /i (A )) ^ (i (C))(a /i (A ), . . . , a /i (A )) = (i (B))(a /i (A ), . . . , a /i (A )) ^ n n n n n n 1 1 1 1 1 1 1 1 1 1 1 ((i (C))(a /i (A ), . . . , a /i (A ))) = i (B(a /A , . . . , a /A )) ^ i (C(a /A , . . . , 1 1 1 1 n 1 n 1 1 1 n n 1 1 1 a /A )) = i ((B(a /A , . . . , a /A ) ^ C(a /A , . . . , a /A ))) = i ((B ^ C)(a /A , . . . , a /A )). n n n n n n n n 1 1 1 d 1 1 1 d 1 1 Similarly, also the proofs for :, _, ! and $ are straightforward. d d Fact 3. The set D is closed under substitution and modus ponens with respect to ! . 0 d Proof. Let A 2 D and A ! B 2 D , that is i (A) 2 D and i (A ! B) 2 D, so (i (A) ! 0 0 1 1 1 i (B))) 2 D, by the distributivity of with respect to ! i (A) ! i (B) 2 D, but by normality 1 1 1 i (A) 2 D, hencei (B))) 2 D and by definition (4), B 2 D . 1 1 0 Assume now that A 2 D , that is i (A) 2 D. Let us consider a result of uniform substitution 0 1 s(A) into A of formulas A for variables in A, where 1 6 i 6 n, for some n, that is, s(A) = A(a /A , . . . , a /A ), where a are all variables in A. By Lemma 1 we know that i (s(A)) = n n 1 1 i 1 (i (A))(a /i (A ), . . . , a /i (A )). Since D is a logic, so it is closed on substitution, so also 1 1 1 1 n 1 n (i (A))(a /i (A ), . . . , a /i (A )) 2 D. But the following equations hold (i (A))(a /i (A ), n n 1 1 1 1 1 1 1 1 1 . . . , a /i (A )) = (i (A)(a /i (A ), . . . , a /i (A ))) = i (s(A)), therefore s(A) 2 D . n 1 n 1 1 1 1 n 1 n 1 0 Axioms 2019, 8, 108 5 of 17 4.1. A Comparison with Some Classical Theses As one can easily see, none of the classical cases given below belong to D , although each of these formulas belong to D . To stress discussive interpretation we use the formulas from For . p ! p p ! p _ q p ^ q ! p d d p ! (q ! (p ^ q)) d d d (p ! (q ! r)) ! ((p ! q) ! (p ! r)) d d d d d d (p ! q) ! ((q ! r) ! (p ! r)) d d d d d ::p ! p p ! ::p Each of these formulas can be rejected semantically. We use standard completeness theorem with respect to Kripke semantics for the logic D. As an example, let us consider the fifth formula, known as Frege syllogism. One can easily see that the respective translation: ((p ! (q ! r)) ! ((p ! q) ! (p ! r))) is not a thesis of D, so the formula (p ! (q ! r)) ! ((p ! q) ! (p ! r)) does not belong d d d d d d to D . Similarly one falsifies the other cases. 5. A Kotas Style Deductive System for the Smallest Discussive Logic We will characterise a discussive logic being a result of the given variant of the discussive model; that is in the case that the relation is serial and no other condition is assumed as regards accessibility relation. We will give an adequacy result for the given deductive system. We will adopt a method of Kotas (see Reference [14]) that was used for indicating the way in which D could be axiomatized. (There are other axiomatisations of D . In Reference [15] there is 2 2 an axiomatisation of discussive logic but in a version with left discussive conjunction. For not so straight history of axiomatisation of D see References [16,17].) The same method was used inter alia in Reference [1] to axiomatize a variant of D with modal operators. Let us use the following notation: (Ai) denotesf, for (Ai) denoting f (6) -S = fA 2 For : A 2 Sg (7) -S is called an M-counterpart of S (see Reference [5, p. 70]). By definitions, for any normal logic S  D: S  -S It is known that (see Reference [5, p. 68]): Fact 4. -D = D (8) Axioms 2019, 8, 108 6 of 17 Consider the following axiomatisation of CL: p ! (q ! p) (A1) (p ! (q ! r)) ! ((p ! q) ! (p ! r)) (A2) p^ q ! p (A3) p^ q ! q (A4) p ! (q ! p^ q) (A5) p ! p_ q (A6) q ! p_ q (A7) (p ! q) ! ((r ! q) ! (p_ r ! q)) (A8) (p $ q) ! (p ! q) (A9) (p $ q) ! (q ! p) (A10) (p ! q) ! ((q ! p) ! (p $ q)) (A11) (:p ! :q) ! (q ! p) (A12) and formulas (p $ ::p) (df) ((p ! q) ! (p ! q)) (K) (p ! p) (D) (p ! p) (T) (p ! p) (5) Let W := f(Ai) : 1 6 i 6 12g [ f(df), (K), (D)g and let W := f(Ai) : 1 6 i 6 12g [ f(df), (K), (T), (5)g Let us recall a theorem that allows to formulate S5 syntactically with the use of the above mentioned formulas and rules. Fact 5 ([14]). 1. S5 is the smallest set including W and closed under (us) and the following rules: j, (j ! y) (mp) (rn) (rn ) 2. S5 is the smallest set including W and closed under (us), (mp) and (rn). 3. -S5 is the smallest set including W and closed under (us), (mp), (rn), (rn ) and (rp ): 1 ( (rp ) j Axioms 2019, 8, 108 7 of 17 But in a quite similar way, one can formulate the logic D. Let D denote the smallest set including W and closed under substitution, (rn), (mp), (rp ) and (mp ) j, (j ! y) (mp ) We will follow a custom used for modal logics of calling elements of D theses of a deductive system. So D is the set of theses with respect to a deductive system determined by the given axioms (Ai) : 1 6 i 6 12 and rules (rn), (mp), (mp ), (rp ) and an substitution. Lemma 2. D = D . Proof. We show that D  D. First, by the standard formulation of D and (rn) we see that W  D—it is enough to use necessitation for respective axioms of D. Besides by (8), D is closed on (rp ). We will prove that D is closed on (mp ). Assume that j,(j ! y) 2 D. By (rn),j 2 D, while by (D), we have(j ! y) 2 D hence using (3) we obtainj ! y 2 D. Thus, by modus ponensy 2 D and by (8), y 2 D. The fact that D is closed on (mp) follows by axiom (K) and modus ponens. Finally, D is closed on (rn) by necessitation. For the reverse direction let us assume that j 2 D. We can consider a proof j ,. . . , j = j of j in the standard axiomatisation of D. First observe that by (mp) and Ai, where, 1 6 i 6 12 we obtainy, for any classical tautology y — it is enough to consider a prove of y and the basis of the system with fAi : 1 6 i 6 12g as axioms, with modus ponens and substitution as rules of inference and next precede every element of the proof by  and observe that the obtained sequence j ,. . . , j is a proof ofy on the basis of the given system of D . Second, we see that any other axiom of D preceded by becomes an axiom of D ; besides, rules of (rn) and (mp) correspond respectively to necessitation and modes ponens in the original proof of j. Hence, using induction on the length of the proof we see that j has a mentioned proof in D . We extend the sequence j ,. . . , j = j to infer j. By (D) we have(j ! j) and so using (mp ) andj we getj, hence by (rp ) we infer j. Let us finally add that both sets are closed in substitution. In Reference [14] two translations were considered. i is a natural version of the first one adjusted to the considered here language. The translation i : For ! For given below is a version of i 2 m d 2 defined in Reference [14] where the case of is added: 1. i (a) = a, for any propositional letter a, 2. for any j, y 2 For : (a) i (:j) = :i (j), 2 2 (b) i (j) = :((:p _ p) ^ :i (j)), 2 2 (c) i (j) = (:p _ p) ^ i (j), 2 d 2 (d) i (j _ y) = i (j) _ i (y), 2 2 2 (e) i (j ^ y) = :(:i (j) _ :i (y)), 2 2 2 (f) i (j ! y) = :i (j) _ i (y), 2 2 2 (g) i (j $ y) = :(:(:i (j) _ i (y)) _ :(:i (y) _ i (j))). 2 2 2 2 2 The below Lemma is being proved similarly as Lemma 4.2 in Reference [1]. Lemma 3. For any j 2 For , i (i (j)) $ j 2 D. m 1 2 Proof. The proof goes by induction on the complexity of a given formula. If j is a variable, we have i (i (j)) = j, thus the thesis holds trivially. 1 2 Assume that the inductive thesis holds for formulas simpler than a given formula. Firstly, we have i (i (j_ y)) = i (i (j)_ i (y)) = i (i (j))_ i (i (y)). Thus, i (i (j_ y)) $ (j_ y) 2 D, 1 2 1 2 2 1 2 1 2 1 2 Axioms 2019, 8, 108 8 of 17 by CL. Similarly by definition, i (i (:j)) = i (:i (j)) = :i (i (j)), so the required equivalence 1 2 1 2 1 2 holds by CL. For the case of , we have: i (i (j)) = i (:((:p _ p) ^ :i (j))) = :((:p _ p) ^ 1 2 1 2 :i (i (j))), so the required equivalence holds by normality, in particular, by CL, extensionality and 1 2 due to the fact that ::p $ p 2 K. For the case of ‘’, we have: i (i (j)) = i ((:p _ p) ^ i (j)) = (:p _ p) ^ i (i (j)) so again, 1 2 1 d 2 1 2 the required equivalence holds by normality. Secondly, by CL and due to the following equations and equivalences, the inductive thesis holds for ‘^’, ‘!’ and ‘$’. For ‘^’: i (i (j^ y)) = i (:(:i (j) _ :i (y))) = :(:i (i (j)) _ :i (i (y))). But, of course, 1 2 1 2 2 1 2 1 2 :(:i (i (j)) _ :i (i (y))) $ (i (i (j))^ i (i (y))) 2 D. 1 2 1 2 1 2 1 2 For the case of ‘!’: i (i (j ! y)) = i (:i (j) _ i (y)) = :i (i (j)) _ i (i (y)). 1 2 1 2 2 1 2 1 2 But :i (i (j)) _ i (i (y)) $ i (i (j)) ! i (i (y)) 2 D. 1 2 1 2 1 2 1 2 For ‘$’: i (i (j $ y)) = i (:(:(:i (j) _ i (y)) _ :(:i (y) _ i (j)))) = :(:(:i (i (j)) 1 2 1 2 2 2 2 1 2 _ i (i (y))) _ :(:i (i (y)) _ i (i (j)))). However, :(:(:i (i (j)) _ i (i (y))) _ 1 2 1 2 1 2 1 2 1 2 :(:i (i (y)) _ i (i (j)))) $ (i (i (j)) $ i (i (y))) 2 D. 1 2 1 2 1 2 1 2 Due to Fact 4, we also have a connection similar to the relation between D and-S5: Lemma 4. 1. For any A 2 For : A 2 D iff i (A) 2 D. 0 1 2. For any j 2 D, we have i (j) 2 D . 2 0 3. If j 2 D and j $ y 2 D, then y 2 D. Proof. Ad 1. Let A 2 D . By the definition of D it means thati (A) 2 D, that is, i (A) 2 -D. Thus, 0 0 1 1 by Fact 4, i (A) 2 D. If i (A) 2 D, then by necessitation and (D),i (A) 2 D, so A 2 D . 1 1 0 Ad 2. Let j 2 D, that is,j 2 D. Then, by Lemma 3 and extensionality for D, we havei (i (j)) 2 D. 1 2 Thus, i (A) 2 D . 2 0 Point 3 is obvious. To make the following consideration easier to follow, for A, B 2 For , let us denote the formula d d d :A _ B as A ! B, and :((:p _ p) ^ :A) as A, (:p _ p) ^ A as A, and (A ! B)), that c c d d is :((:p _ p) ^ :(:A _ B)) as A J B. d d Let ` be the consequence relation determined by the set i (W) and the following formulas: i (i (q ^ r)) J (q ^ r) (B1) 2 1 d d d (i (i (q ! r)) J (q ! r)) (B2) 2 1 d d d (i (i (q $ r)) J (q $ r)) (B3) 2 1 d d d ((q ^ r) J i (i (q ^ r))) (C1) d d 2 1 d ((q ! r) J i (i (q ! r))) (C2) d d 2 1 d ((q $ r) J i (i (q $ r))) (C3) d d 2 1 d Axioms 2019, 8, 108 9 of 17 as axioms together with substitution and the following rules: A (A J B) ( mp ) str A (A J B) d 0 ( mp ) str ( rn) d d (rp ) The proof of the following lemma is straightforward by induction on the complexity of a modal formula j. Lemma 5. Let j, y , . . . , y be modal formulas and y be a result of substitution of y , . . . , y respectively 1 n 1 n for atoms a , . . . , a in j. Then the formula i (y) equals the result of substitution of i (y ), . . . , i (y ) for 1 n 2 2 1 2 n atoms a , . . . , a in i (j). 1 n 2 Directly from definitions and used notation, we have: Fact 6. For any j, y 2 For 1. i ((j)) =  (i (j)), 2 2 2. i ((j)) =  (i (j)), 2 2 3. i ((j ! y)) = i (j) J i (y). 2 2 d 2 Lemma 1. 1. For any j 2 CL, we have `  i (j). D 2 2. For any j 2 D, we have ` i (j). Proof. Ad 1. Assume that j 2 CL. Then there is a proof c , . . . , c , of j = c on the basis of n n d d (A1)–(A12), (mp) and substitution. Consider the sequence  i (c ), . . . ,  i (c ). By induction 2 1 2 n on the length of the sequence one can see that it is a proof on the basis of ` , since its elements are either elements of i (W) or arise by the application of ( mp ) or substitution. For the case of str substitution it is enough to use Lemma 5 and apply the substitution of i (y ), . . . , i (y ) for a , . . . , 2 1 2 1 a in i (c ), if in the initial proof a substitution of formulas y , . . . , y for atoms a , . . . , a in c m 2 i 1 m 1 m i was applied. Ad 2. Assume that j 2 D. Then there is a proof c , . . . , c of j, in the sense of the consequence 1 n d d d relation . Consider i (c ), . . . , i (c ), ( i (c ) J  i (c )), i (c ), i (c ) = i (j). By n n n n n 2 1 2 2 d 2 2 2 2 induction on 1 6 i 6 n, by the point 1 of this lemma and Fact 6, we can easily show that ` i (c ), 2 i d d d d that is,`  i (c ), while ( i (c ) J  i (c )) is an instance of i (D), i (c ) follows from n n n D 2 i 2 d 2 2 2 d d d 0 d d i (c ) and ( i (c ) J  i (c )) by ( mp ); and i (j) follows from i (c ) by (rp ). 2 n 2 n 2 n 2 2 n str ( Thus, we obtain that: Fact 7. The following formulas are theses with respect to ` : (i (i (:p)) J :p) (9) 2 1 d (i (i (p _ q)) J p _ q) (10) 1 d d d Proof. For (9), observe that (i (i (:p)) J :p) =  (i (i (:p)) ! :p) =  (:p ! :p) = 2 1 d 2 1 c c i (:p ! :p). So (9) follows by Lemma 1.1. 2 c Axioms 2019, 8, 108 10 of 17 For (10), one can see that (i (i (p _ q)) J p _ q) =  (i (i (p) _ i (q)) ! p _ q) = 2 1 2 1 1 c d d (i (i (p)) _ i (i (q)) ! p _ q) =  (p _ q ! p _ q). So again, the condition is obtained by c c 2 1 2 1 Lemma 1.1. The above fact can be extended for the case of any formulas used instead of p and q. Moreover, it can be generalised to any compound formula which results in the below Lemma. Its proof goes similarly as the proof of Reference [1, Fact 4.6]. However, there are essential changes for the case of discussive operators, so we present it for the sake of completeness of considerations. Fact 8. For any A 2 For , `  (i (i (A)) ! A) (11) 2 c D 1 `  (A ! i (i (A))). (12) D c 2 1 Proof. The proof goes simultaneously for both theses by induction on the complexity of a formula A. The case of atoms follows by Lemma 1.1. Assume that the inductive hypothesis holds for any formula of complexity smaller than the complexity of A. That is, for the following cases A = :B, A = B_ C, A = B ^ C, A = B ! C and A = B $ C, d d d where B, C 2 For we assume that: ` (i (i (B)) J B), D 1 d ` (i (i (C)) J C), D 2 1 d ` (B J i (i (B))), D d 1 ` (C J i (i (C))). D d 2 1 in other words `  (i (i (B)) ! B), (13) 2 c D 1 `  (i (i (C)) ! C), (14) D 2 1 c `  (B ! i (i (B))), (15) D c 2 1 `  (C ! i (i (C))). (16) c 2 D 1 For the case of ‘:’ let us notice that `  i (p ! q) ! (:q ! :p) , by Lemma 1(1), that is, ` ((p ! q) J (:q ! :p)). So, since :i (i (B)) = i (i (:B)), using the substitution p/B, c c D d 2 1 2 1 q/i (i (B)), (15) and ( mp ), we get: 2 1 str `  (i (i (:B)) ! :B). D 2 1 c Similarly, using the substitution p/i (i (B)), q/B, (13) and ( mp ) we obtain: 2 1 str `  (:B ! i (i (:B))). D 2 1 For the case of ‘_’ notice that `  i (p ! q) ! ( r ! s) ! ((p _ r) ! (q _ s))) , by Lemma 1(1), that is, `  ((p ! q) ! ((r ! s) ! ((p _ r) ! (q _ s)))) or equivalently D c c c c c (p ! q) J ((r ! s) ! ((p _ r) ! (q _ s))) (17) c c c c is a thesis with respect to ` . Thus, since i (i (B)) _ i (i (B)) = i (i (B _ C)), using the 2 1 2 1 2 1 substitution p/i (i (B)), q/B, r/i (i (C)), s/C into (17), by (13) and ( mp ), we get: 2 1 2 1 str `  ((i (i (C)) ! C) ! ((i (i (B)) _ i (i (C))) ! (B _ C))) c c c D 2 1 2 1 2 1 0 Axioms 2019, 8, 108 11 of 17 that is, ` (i (i (C)) ! C) J ((i (i (B)) _ i (i (C))) ! (B _ C)) c c D 2 1 d 2 1 2 1 And again, by (14) and ( mp ), we obtain: str `  i (i (B_ C)) ! (B _ C) . D 2 1 Similarly, using the substitution p/B, q/i (i (B)), r/C, s/i (i (C)), to (17), we obtain: 2 1 2 1 (B ! i (i (B))) J c 2 1 J ((C ! i (i (C))) ! ((B _ C) ! (i (i (B)) _ i (i (C))))) d c 2 1 c c 2 1 2 1 d d hence, by (15) and ( mp ), and again by (16) and ( mp ) we get: str str `  (B _ C) ! i (i (B_ C)) . c 2 1 For the case of ‘^ ’ first let us observe that i (i (B ^ C)) = i (i (B) ^ i (C)) = 2 1 d 2 1 1 :(:i (i (B)) _ :i (i (C))) = (18) 2 1 2 1 :(:i (i (B)) _ :((:p _ p) ^ i (i (C)))). 2 1 d 2 1 Hence by (B1) and definitions of i and i we get ` :(:q _ :((:p _ p) ^ r)) J (q ^ r). While 1 2 D d d d by (C1), similarly we obtain: ` (q ^ r) J :(:q _ :((:p _ p) ^ r)). Therefore, by substitution D d d d we obtain ` :(:B _ :((:p _ p) ^ C)) J (B ^ C) (19) D d d d and ` (B ^ C) J :(:B _ :((:p _ p) ^ C)) (20) D d d d Notice that ((t ! q) ! ((r ! s) ! (t ^ r ! q ^ s))) 2 D, so by Lemma 1(2) and Fact 6, `  (i ((p ! q) ! ((r ! s) ! (t ^ r ! q ^ s)))), that is, D 2 ` (t ! q) J D c d (21) ((r J s) ! (:(:t _ :((:p _ p) ^ r)) ! :(:q _ :((:p _ p) ^ s)))). c c d d d By substitution: t/i (i (B)), q/B, r/i (i (C)), s/C, (13) and ( mp ), we get: 2 1 2 1 str ((i (i (C)) J C) ! 2 c 1 d (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! :(:B _ :((:p _ p) ^ C)))) 2 1 d 2 1 c d But by ( rn) applied to (14) we have `  (i (i (C)) J C) D 2 1 d Therefore, again by ( mp ): str (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! :(:B _ :((:p _ p) ^ C))) 2 1 d 2 1 c d But by Lemma 1(1) we have ` (p ! q) J ((q ! r) ! (p ! r)), (22) c c c c D d 0 Axioms 2019, 8, 108 12 of 17 so by substitution p/:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))), q/:(:B _ :((:p _ p) ^ C)) 2 1 2 1 d d and r/(B ^ C), using ( mp ) we obtain: str ((:(:B _ :((:p _ p) ^ C)) ! (B ^ C)) ! d c d c (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! (B ^ C))) 2 2 c 1 d 1 d that is, (:(:B _ :((:p _ p) ^ C)) ! (B ^ C)) J d d d (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! (B ^ C)) 2 1 2 1 c d d Thus, from (19) using ( mp ) we infer str (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! (B ^ C)) 2 1 d 2 1 c d what is the required formula due to the observation (18). For the reverse implication, using (21) but substituting t/B, q/i (i (B)), r/C, s/i (i (C)) and next 2 1 2 1 appyling (15) and ( mp ) we infer str ((C J i (i (C))) ! 2 1 c (:(:B _ :((:p _ p) ^ C)) ! :(:i (i (B)) _ :((:p _ p) ^ i (i (C)))))) d c 2 1 d 2 1 While applying ( rn) for (16) we obtain `  (C J i (i (C))) 2 1 D d Thus, by ( mp ): str (:(:B _ :((:p _ p) ^ C)) ! :(:i (i (B)) _ :((:p _ p) ^ i (i (C))))) d c 2 1 d 2 1 Using an instance of (22), where p/(B ^ C), q/:(:B _ :((:p _ p) ^ C)) and r/:(:i (i (B)) _ d d 2 1 :((:p _ p) ^ i (i (C)))), by (20) and ( mp ), and then thanks to the above formula and again 2 1 str ( mp ) we obtain str ((B ^ C) ! :(:i (i (B)) _ :((:p _ p) ^ i (i (C))))) c 2 2 d 1 d 1 which is the required formula by the observation (18). The case of ‘! ’. By definitions, we have: i (i (B ! C)) = i (i (B) ! i (C)) = 2 1 2 1 1 (23) :((:p _ p) ^ i (i (B))) _ i (i (C)) d 2 1 2 1 Thus, by (B2) and (C2) we have :((:p _ p) ^ q) _ r J (q ! r)) d d d (q ! r) J :((:p _ p) ^ q) _ r d d d So by substitution we have :((:p _ p) ^ B) _ C J (B ! C)) (24) d d d (B ! C) J :((:p _ p) ^ B) _ C (25) d d d Axioms 2019, 8, 108 13 of 17 Let us notice that ((q ! r) ! (q ! r)) 2 K  D. Hence, by Lemma 1(2): ` i (((q ! r) ! (q ! r))), that is, by definition of i and by Fact 6: 2 2 d d d d d d `  (  (q ! r) !  ( q !  r)). c c c or equivalently d d d `   (q ! r) J  (((:p _ p) ^ q) ! ((:p _ p) ^ r)). (26) D c d d c d so by substitution q/B, r/i (i (B)), we obtain that 2 1 d d (B ! i (i (B))) J c 2 1 d (27) (((:p _ p) ^ B) ! ((:p _ p) ^ i (i (B)))). d c d 2 1 d d d d 0 is a thesis of D . Applying ( rn) to (15) we get  (B ! i (i (B))), hence by ( mp ) we infer 0 2 1 str (((:p _ p) ^ B) ! ((:p _ p) ^ i (i (B)))). c 2 1 d d By a substitution q/C, r/i (i (C)) in (26) and by ( rn) applied for (16) instead of (15) and finally by 2 1 d 0 ( mp ) we obtain: str (((:p _ p) ^ C) ! ((:p _ p) ^ i (i (C)))). (28) c 2 d d 1 As one can see,((q ! t) ! ((r ! s) ! ((t ! r) ! (q ! s)))) 2 K  D. Hence by Lemma 1(2) we obtain (((:p _ p) ^ q) ! ((:p _ p) ^ t)) J d d d (29) ((r ! s) ! ((((:p _ p) ^ t) ! r) ! (((:p _ p) ^ q) ! s))) c c d c c d c Now, we use the substitution: q/B, t/i (i (B)), r/i (i (C)), s/C and applying ( mp ) to (5) we 2 2 1 1 str infer (i (i (C)) ! C) J 2 1 d ((((:p _ p) ^ i (i (B))) ! i (i (C))) ! (((:p _ p) ^ B) ! C)) 2 1 c 2 1 c c d d and next by ( mp ) applied to (14) we have str (((:p _ p) ^ i (i (B))) ! i (i (C))) J (((:p _ p) ^ B) ! C) c c d 2 1 2 1 d d But by (23) it means that ` i (i (B ! C)) J (((:p _ p) ^ B) ! C) (30) 2 1 c D d d d Now, we use (22), (24) and the above formula and act similarly as in the case of ‘^ ’, we conclude that: ` i (i (B ! C)) J (B ! C) . D 2 1 d d d For the reverse implication we apply the following substitution to (29): q/i (i (B)), t/B, r/C, 2 1 s/i (i (C)) and we receive: 2 1 (((:p _ p) ^ i (i (B))) ! (:p _ p) ^ B)) J 2 1 c d d d J ((C ! i (i (C))) ! (31) d c 2 1 c ((((:p _ p) ^ B) ! C) ! (((:p _ p) ^ i (i (B))) ! i (i (C))))) c c 2 1 c 2 1 d d Axioms 2019, 8, 108 14 of 17 Similarly as (5) we obtain  (((:p _ p) ^ i (i (B))) ! ((:p _ p) ^ B)). Hence, applying 2 1 c d d ( mp ) to (31) we infer str (C ! i (i (C))) J c 2 1 d ((((:p _ p) ^ B) ! C) ! (((:p _ p) ^ i (i (B))) ! i (i (C)))) d c c d 2 1 c 2 1 So again by ( mp ) and (16) we obtain str (((:p _ p) ^ B) ! C) J (((:p _ p) ^ i (i (B))) ! i (i (C))) c c d d d 2 1 2 1 So acting as previously, by (22), (25), (23) and ( mp ) we obtain str `  (B ! C) ! i (i (B ! C)) . D d c 2 1 d For the case of ‘$ ’ notice that by Lemma 1(1), `  (i ((p ! q) ! ((q ! p) ! (p $ q)))), d D 2 that is, `  ((p ! q) ! ((q ! p) ! :(:(p ! q) _ :(q ! p)))). Thus, by substitutions, c c c c c c inductive hypotheses (13), (14), (15), (16) and applying ( mp ) and definition of i we get: str :(:(B ! i (i (B))) _ :(i (i (B)) ! B)) (32) c c 2 1 2 1 :(:(C ! i (i (C))) _ :(i (i (C)) ! C)) (33) c 2 1 2 1 c Hence, by the use of the following thesis of K  D: (r $ s) ! (t $ q) ! (r $ s) ! ((q ! s) ^ (s ! q)) ! ((t ! r) ^ (r ! t))) , by Lemma 1(2), Fact 6, (33), ( mp ) and substitution r/C, s/i (i (C)), t/B, q/i (i (B)) we get: 2 1 2 1 str d d :(:(B ! i (i (B))) _ :(i (i (B)) ! B)) ! c 2 1 2 1 c c d d :(:(:C _ i (i (C))) _ :(:i (i (C)) _ C)) 2 1 2 1 d d d ! :((: i (i (B)) ! i (i (C))) _ : ( i (i (C)) ! i (i (B)))) c 2 1 c 2 1 2 1 c 2 1 d d d ! :(:( B ! C) _ : ( C ! B))) c c c d d By the result of application of ( rn) to (33) and again ( mp ) we infer str d d d :(:(:C _ i (i (C))) _ :(:i (i (C)) _ C)) 2 1 2 1 d d d ! :((: i (i (B)) ! i (i (C))) _ : ( i (i (C)) ! i (i (B)))) c 2 1 c 2 1 2 1 c 2 1 d d d ! :(:( B ! C) _ : ( C ! B))) c c c d d Now we twice apply ( rn) to (33) and again use ( mp ), as a result we get: str d d d d (:(:( i (i (B)) ! i (i (C))) _ : ( i (i (C)) ! i (i (B)))) ! 2 1 c 2 1 2 1 c 2 1 c d d d :(:( B ! C) _ : ( C ! B))). c c Thus, since by definitions of the functions i and i , :(:( i (i (B)) ! i (i (C))) _ 1 2 2 1 2 1 d d : ( i (i (C)) ! i (i (B)))) = i ((i (B) ! i (C)) ^ (i (C) ! i (B))) = i (i (B $ 2 1 c 2 1 2 1 1 1 1 2 1 C)), we get: d d d d (i (i (B $ C)) ! :(:( B ! C) _ : ( C ! B))). 2 1 c c c d Axioms 2019, 8, 108 15 of 17 From axiom (B3) we obtain: d d d d (:(:( B ! C) _ : ( C ! B)) ! (B $ C)). c c c d Thus, again by a substitution to i  (p ! q) ! (q ! r) ! (p ! r)) and the application of ( mp ), we get: str `  i (i (B $ C)) ! (B $ C) . D 2 1 d c d Similarly we show: `  (B $ C) ! i (i (B $ C)) . D d 2 1 d By induction on the complexity of formulas, we obtain (11) and (12). Theorem 1. The set of theses with respect to the consequence relation ` equals D . Proof. Let A 2 D . By Lemma 4, i (A) 2 D. Thus, by Lemma 2, there is a proof c , . . . , c = i (A) 0 1 1 1 such that for each i 2 f1, . . . , ng, c is one of the formulas (A1)–(A12), (df), (D), (K) or c is i i a result of the application of substitution, (rn), (mp), (mp ), (rp ), for some formulas preceding c in the sequence. Let us consider the following sequence of formulas i (c ), . . . , i (c ), i (i (A)), i 2 1 2 n1 2 1 (i (i (A)) ! A), A. By induction on i we see that the fragment of the sequence i (c ), . . . , 2 1 c 2 1 i (c ) = i (i (A)) is a proof in the given axiomatic system, while the formula (i (i (A)) ! A) 2 n 2 1 2 1 c is a thesis of the system, by Fact 8. So the formula A completes the proof as a result of application of d 0 the rule ( mp ) to two preceding formulas. Thus, ` A str 0 Now, for the reverse direction, assume that for a given formula A there is a proof C , . . . , C = A of 1 n the formula A within the considered deductive system. By the definition of D , it is enough to prove that for any i 2 f1, . . . , ng,i (C ) 2 D or, equivalently, i (C ) 2 D. 1 i 1 i Firstly, let us consider the case of axioms. Suppose that C 2 i (W). For the case (A1)–(A12) that is, when C = i (j), for some j 2 CL  D—it is enough to apply Lemma 1(2). Then i 2 i (i (j)) $ j 2 D, by Lemma 3. Therefore, by Lemma 4(3), i (i (j)) = i (C ) 2 D. In the 1 2 1 2 1 case of other axioms from the set i (W), we act similarly. d d Ad(B1): i ( (i (i (q ^ r)) ! (q ^ r))) = i ( (i (q ^ r) ! (q ^ r))) = i (:((:p _ p) ^ 1 2 1 c 1 2 c 1 d d d d :(:(:q _ :((:p _ p) ^ r)) ! (q ^ r)))) = :((:p _ p) ^ :(:(:q _ :((:p _ p) ^ r)) ! d c d c (q ^ r))). But :((:p _ p) ^ :(:(:q _ :((:p _ p) ^ r)) ! (q ^ r))) $ ((q ^ r) ! (q ^ c c r)) belongs to D. Thus, (B1) 2 D , thanks to Lemma 4. Ad (B2): i ( (i (i (q ! r)) ! (q ! r))) = i (:((:p _ p) ^ :(((:p _ p) ^ q ! r) ! 2 c c c 1 1 d d 1 d d (q ! r)))) = :((:p _ p) ^ :(((:p _ p) ^ q ! r) ! (q ! r))). However, :((:p _ p) ^ d c c :(((:p _ p) ^ q ! r) ! (q ! r))) $ ((q ! r) ! (q ! r)) is a thesis of D. Thus, c c c c (B2) 2 D , by Lemma 4. d d Ad (B3): i ( (i (i (q $ r)) ! (q $ r))) = i ( (i ((q ! r) ^ (r ! q)) ! (q $ 2 c 2 c 1 1 d d 1 d r))) = i (:((:p _ p) ^ :(:(:((:p _ p) ^ q ! r) _ :((:p _ p) ^ ((:p _ p) ^ r ! q))) ! 1 d d c d d c c (q $ r)))) = :((:p _ p) ^ :(:(:((:p _ p) ^ q ! r) _ :((:p _ p) ^ ((:p _ p) ^ r ! c c q))) ! ((q ! r) ^ (r ! q)))). Notice that :((:p _ p) ^ :(:(:((:p _ p) ^ q ! r) _ c c :((:p _ p) ^ ((:p _ p) ^ r ! q))) ! ((q ! r) ^ (r ! q)))) $ ((q ! r) ^ (r ! c c c c q) ! ((q ! r) ^ (r ! q))). Thus, (B3) belongs to D , similarly, by Lemma 4. c 0 Ad (C1): i ( ((q ^ r) ! i (i (q ^ r)))) = :((:p _ p) ^ :((q ^ r) ! :(:q _ :((:p _ c 2 c 1 d 1 d p) ^ r)))). Thus again, (C1) 2 D . Ad (C2): i ((q ! r) J i (i (q ! r))) = :((:p _ p) ^ :((q ! r) ! ((:p _ p) ^ q ! r))). c c 1 d d 2 1 d Hence (C2) 2 D . Ad (C3): i ((q $ r) J i (i (q $ r))) = :((:p _ p) ^ :(((q ! r) ^ (r ! q)) ! 1 d d 2 1 d :(:((:p _ p) ^ q ! r) _ :((:p _ p) ^ ((:p _ p) ^ r ! q))))). As one can see (C3) 2 D . c c 0 d d d Ad ( mp ). Assume that  A and  (A ! B) belong to D , that is, i (:((:p _ p) ^ :A)) 0 1 d str and i (:((:p _ p) ^ :(A ! B))) are theses of D. By Fact 4 equivalently, (:((:p _ p) ^ 1 d c Axioms 2019, 8, 108 16 of 17 :i (A))) 2 D and (:((:p _ p) ^ :(i (A) ! i (B)))) 2 D, in other words i (A) 2 D and 1 1 c 1 1 (i (A) ! i (B)) 2 D, hence of course i (B) 2 D. Equivalently, ::i (B) 2 D and :((:p _ 1 1 1 1 p) ^ :i (B)) 2 D, but by definition of i , :((:p _ p) ^ :i (B)) = i (:((:p _ p) ^ :B), hence 1 1 1 1 also i (:((:p _ p) ^ :B)) 2 D, therefore B 2 D . 1 d 0 d 0 d d Ad ( mp ). Suppose that A and (A ! B) belong to D , that is,i (A) andi ( (A ! B)) c 0 1 1 c str belong to D; and so(:((:p _ p) ^ :(:i (A) _ i (B)))) 2 D. Therefore,(i (A) ! i (B)) 2 1 1 1 1 D and by Fact 4: (i (A) ! i (B)) 2 D. Hencei (B) 2 D, so B 2 D . by definition of D. 1 1 1 0 d d Ad ( rn): Let  A 2 D , that is, i (:((:p _ p) ^ :A)) 2 D; and in other words (:((:p _ 0 1 d p) ^ :i (A))) 2 D. But this means that i (A) 2 D and by Fact 4, also i (A) 2 D. Hence 1 1 1 by necessitationi (A) 2 D, so again by necessitation and (D) alsoi (A) 2 D. Equivalently, 1 1 ::::i (A) 2 D. This can be rewritten as :((:p _ p) ^ ::((:p _ p) ^ :i (A))) 2 1 1 d d D. That is i (:((:p _ p) ^ ::((:p _ p) ^ :A))) 2 D. Hence i (  A) 2 D, that 1 d d 1 d d is,  A 2 D . d d Ad (rp ): Let  A 2 D , that is, i ((:p _ p) ^ A) 2 D, equivalently (:p _ p) ^ i (A) 2 D,; 0 1 d 1 and soi (A) 2 D. Then by Fact 4, alsoi (A) 2 D; and so A 2 D . 1 1 0 Finally, we consider the case of substitution. Assume that A belongs to D , that is,i (A) is a thesis 0 1 of D. Now, let us consider a substitution of formulas A ,. . . , A for variables a ,. . . , a in A. Let 1 n 1 n us also consider i (A)(a /i (A ), . . . , a /i (A )) the result of substitution of i (A ),. . . , i /A for 1 1 1 1 n 1 n 1 1 n n variables a ,. . . , a in i (A). By Lemma 1 the following holds: (i (A))(a /i (A ),. . . , a /i (A )) = 1 n 1 1 1 1 1 n 1 n i (A(a /A ,. . . , a /A )). Since D as a modal logic is closed on substitution, (i (A))(a /A ,. . . , 1 1 1 n n 1 1 1 a /A ) 2 D, but by the last equation and the features of substitution, (i (A))(a /i (A ),. . . , n n 1 1 1 1 a /i (A )) = ((i (A))(a /i (A ),. . . , a /i (A ))) = i (A(a /A ,. . . , a /A )). By definition n 1 n 1 1 1 1 n 1 n 1 1 1 n n of D , it means that A(a /A ,. . . , a /A ) 2 D . 0 n n 0 1 1 6. Conclusions We gave a syntactic characterisation of the minimal discussive logic. This is as an initial step in our investigations on other variants of discussive logics obtained by other cases of relations that connect participants of a discussion. Author Contributions: Conceptualization, K.M.-N. and M.N.; formal analysis, K.M.-N. and M.N.; investigation, K.M.-N. and M.N.; methodology, K.M.-N.; validation, K.M.-N.; writing–original draft preparation, K.M.-N. and M.N.; writing–review and editing, K.M.-N. and M.N.; supervision, M.N.; funding acquisition, M.N. Funding: The authors of this work benefited from support provided by Polish National Science Centre (Narodowe Centrum Nauki), grant number 2016/23/B/HS1/00344. Conflicts of Interest: The authors declare no conflict of interest. References 1. Mruczek-Nasieniewska, K.; Nasieniewski, M.; Pietruszczak, A. A modal extension of Jaskowski’s ´ discussive logic D . Log. J. IGPL 2019, 27, 451–477, doi:10.1093/jigpal/jzz014. 2. Błaszczuk, J. J.; Dziobiak, W. An axiomatization of M -counterparts for some modal logics. Reports Math. Log. 1976, 6, 3–6. 3. Furmanowski, T. Remarks on discussive propositional calculus. Studia Log. 1975, 34, 39–43, doi:10.1007/ BF02314422. 4. Błaszczuk, J. J.; Dziobiak, W. Remarks on Perzanowski’s modal system. Bull. Sect. Log. 1975, 4, 57–64. 5. Perzanowski, J. On M-fragments and L-fragments of normal modal propositional logics. Reports Math. Log. 1975, 5, 63–72. 6. Nasieniewski, M.; Pietruszczak, A. A method of generating modal logics defining Jasko ´ wski’s discussive logic D2. Studia Logica 2011, 97, 161–182, doi:10.1007/s11225-010-9302-2. 7. Nasieniewski, M.; Pietruszczak, A. On the weakest modal logics defining Jaskowski’s ´ logic D2 and the D2-consequence. Bull. Sect. Log. 2012, 41, 215–232. Axioms 2019, 8, 108 17 of 17 8. Nasieniewski, M.; Pietruszczak, A. A method of generating modal logics defining Jasko ´ wski’s discussive D2-consequence. In Logic, Reasoning & Rationality, Weber, E., Wouters, D., Meheus, J., Eds.; Springer: Dordrecht, the Netherlands, 2014; Logic, Argumentation & Reasoning; Volume 5, pp. 95–123, doi:10.1007/ 978-94-017-9011-6_6. 9. Urchs, M. On the role of adjunction in para(in)consistent logic. In Paraconsistency: The Logical Way to the Inconsistent, Proceedings of the Second World Congress on Paraconsistency, São Paulo, Brazil, May 12–19, 2000; Carnielli, W. A., Coniglio, M. E., Loffredo D’Ottaviano, I. M., Eds.; Marcel Dekker: New York, NY, USA, 2002; pp. 487–499. 10. Jaskowski, ´ S. Rachunek zdan ´ dla systemów dedukcyjnych sprzecznych. Studia Societatis Scientiarum Torunensis 1948, Sect. A, vol. I (5), 57–77. In English: Propositional calculus for contradictory deductive systems. Studia Logica 1969, 24, 143–157. doi:10.1007/BF02134311. A propositional Calculus for inconsistent deductive systems. Logic and Logical Philosophy 1999, 7, 35–56, doi: 10.12775/LLP.1999.003 11. Jaskowski, ´ S. O koniunkcji dyskusyjnej w rachunku zdan ´ dla systemów dedukcyjnych sprzecznych. Studia Societatis Scientiarum Torunensis 1949, Sect. A, 1, 171–172. In English: On the discussive conjunction in the propositional calculus for inconsistent deductive systems. Log. Log. Philos. 1999, 7, 57–59, doi:10.12775/LLP. 1999.004. 12. Bull, R. A.; Segerberg, K. Basic Modal Logic. In Handbook of Philosophical Logic; Gabbay, D. M., Guenthner, F., Eds.; D. Reidel Publishing Company: Dordrecht, Holland, 1984; Volume 3, pp. 1–88, doi:10. 1007/978-94-009-6259-0_1 13. Segerberg, K. An Essay in Classical Modal Logic; Uppsala Universitet: Uppsala, Sweded, 1971; Volume I and II. 14. Kotas, J. The axiomatization of S. Jaskowski’s ´ discussive system. Studia Logica 1974, 33, 195–200, doi:10.1007/ BF02120494. 15. da Costa, N.C.A.; Dubikajtis, L. On Jaskowski ´ discussive logic. In Non-Classical Logics, Model Theory and Computability; Arruda, A. I., da Costa, N. C. A., Chuaqui, R., Eds.; North-Holland: New York, NY, USA, 1977; pp. 37–56. 16. Ciuciura, J. A new real axiomatization of the discursive logic D2. In Handbook of Paraconsistency; Beziau, J. Y., Carnielli, W., Gabbay, D. M., Eds.; College Publications: London, UK, 2007; pp. 427–437. 17. Omori, H.; Alama, J. Axiomatizing Jaskowski’s ´ Discussive Logic D . Studia Logica 2018, 106, 1163–1180, doi:10.1007/s11225-017-9780-6. 2019 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (http://creativecommons.org/licenses/by/4.0/). http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Axioms Multidisciplinary Digital Publishing Institute

A Kotas-Style Characterisation of Minimal Discussive Logic

Download PDF
17 pages

Loading next page...
 
/lp/multidisciplinary-digital-publishing-institute/a-kotas-style-characterisation-of-minimal-discussive-logic-ScLL5LXLUW
Publisher
Multidisciplinary Digital Publishing Institute
Copyright
© 1996-2019 MDPI (Basel, Switzerland) unless otherwise stated Terms and Conditions Privacy Policy
ISSN
2075-1680
DOI
10.3390/axioms8040108
Publisher site
See Article on Publisher Site

Abstract

axioms Article A Kotas-Style Characterisation of Minimal Discussive Logic 1, ,† 2, ,† Krystyna Mruczek-Nasieniewska * and Marek Nasieniewski * Department of Logic, Nicolaus Copernicus University in Torun, ´ ul. Moniuszki 16/20, 87-100 Torun, ´ Poland * Correspondence: mruczek@umk.pl (K.M.-N.); mnasien@umk.pl (M.N.) † These authors contributed equally to this work. Received: 26 August 2019; Accepted: 27 September 2019; Published: 1 October 2019 Abstract: In this paper, we discuss a version of discussive logic determined by a certain variant of Jaskowski’s ´ original model of discussion. The obtained system can be treated as the minimal discussive logic. It is determined by frames with serial accessibility relation. As the smallest one, this logic can be treated as a basis which could be extended to richer discussive logics that are obtained by varying accessibility relation and resulting in a lattice of discussive logics. One has to remember that while formulating discussive logics there is no one-to-one determination of discussive logics by modal logics. For example, it is proved that Jaskowski’s ´ logic D can be expressed by other than S5 modal logics. In this paper we consider a deductive system for the sketchily described minimal logic. While formulating the deductive system, we apply a method of Kotas that was used to axiomatize D . The obtained system determines a logic D as a set of theses that is contained in D . Moreover, 2 0 2 any discussive logic that would be expressed by means of the provided model of discussion would contain D , so it is the smallest discussive logic. Keywords: discussive logics; the smallest discussive logic; discussive operators; seriality; accessibility relation; Kotas’ method; modal logic 1. Introduction Stanisław Jaskowski’s ´ aim was to propose a calculus that would allow for explication of inconsistent theories by means of some consistent framework. As a result Jaskowski ´ developed a logic denoted as D that was meant to be a basis for calculus that would not lead in general to overfull set of conclusions when applied to inconsistent set of premisses. He used the scenario of a discussion as a model case. Intuitively, during discussions participants can contradict each other, but a possible external observer as well as particular participants would not conclude that everything follows from such discussion. (Some analysis on this matter can be found in [1].) Interactions that take place between participants of a discussion are expressed formally by discussive counterparts of implication, conjunction and equivalence. Moreover, in Jaskowski’s ´ intuitive model, operators take only auxiliary role and modal operators are not present in the object language of the discussive logic. Such a variant seems to be natural and has been considered in [1]. Our aim is to indicate the weakest logic that arises from a natural variant of Jaskowski ´ model of discussion and moreover, give an adequate deductive system for such a logic. 2. D and the Minimal Variant of Discussive Logic In the original formulation, Jaskowski ´ considered a situation in which there is no restriction on possible reactions of participants of a discussion, in other words he considered a model, where every two participants of the discussion are connected. It corresponds to the full accessibility relation that semantically allows to determine the logic S5. However, it is known that not every thesis is in fact used Axioms 2019, 8, 108; doi:10.3390/axioms8040108 www.mdpi.com/journal/axioms Axioms 2019, 8, 108 2 of 17 or needed to express discussive theses. What is only used, is the so-called M-counterpart of the logic S5 (for investigations on this notion see [2]). In various papers it has been shown (see [3–7]) that to be able to formulate D , one can use various modal logics. (Jaskowski’s ´ logic was meant to be a basis for a consequence relation and also in this case there can be given other systems than S5 which also allow to express D -consequence relation (see [8]).) Moreover, one can introduce a general discussive consequence relation framework, in which D would be the set of theses of one of its special cases (for details see [9]). However, this does not mean that any modal logic would be equally good to obtain D . We will keep original Jaskowski’s ´ meaning of discussive connectives of implication and conjunction. Jaskowski’s ´ discussive implication denoted here as ! , is meant to be read as “if anyone states that p, then q” (see [10] p. 150, 1969), in modal terms: p ! q. Discussive conjunction is usually interpreted as saying “p and someone said q”, in the modal Jaskowski’s ´ interpretation it is read as p ^ q. (The disjunction conjunction was introduced in the second Jaskowski ´ paper on discussive logic [11].) In both cases is originally interpreted as possibility that can refer to any participant of discussion. In our interpretation it will refer only to those participants, who are connected by the accessibility relation. In particular, it means that statements of participants, who are not connected to any disputant, make the whole discussion (since we are interested in expressing what logically follows, so we ought to consider each world — or in the nomenclature of the model of the discussion — each point of view) meaningless. As Jaskowski ´ says, every thesis of the discussive system during its interpretation ought to be preceded by the reservation: “in accordance with the opinion of one of the participants in the discourse”, so “if a thesis is recorded in a discursive system, its intuitive sense ought to be interpreted so as if it were preceded by the symbol Pos” ([10] p. 149, 1969), which nowadays is denoted standardly by ‘’. Taking into account what has been said, the minimal requirement for the considered model of discussion is that the ‘outer ’ possibility ought to be ruled by a serial accessibility condition. From the formal point of view, the underlying modal logic that will be used for the formulation of the proposed variant of discussive logic, will be the deontic normal logic D. As it is known, it is semantically expressed by the class of frames with serial accessibility relation (where seriality means that for every world w there is a world v such that wRu). To strictly formulate the presented idea we will need two formal languages: modal and discussive. 3. Modal and Discussive Languages Throughout the paper we will use modal formulas that are formed in the standard way from propositional letters: ‘p’, ‘q’, ‘r’, ‘s’, ‘t’, ‘p ’, ‘p ’, ‘p ’, . . . ; truth-value operators: ‘:’, ‘_’, ‘^’, ‘!’, 0 1 2 and ‘$’ (connectives of negation, disjunction, conjunction, material implication and material equivalence, respectively); modal operators: the necessity and possibility operators ‘’ and ‘’; and the brackets. Let For denote the set of all modal formulas. Of course, the set For includes m m the set of all classical formulas (without the use of ‘’ and ‘’), in particular the set of all classical tautologies denoted as CL. The modal language plays only an auxiliary role in the formulation of discussive logic. Its object language is built again from propositional letters, truth-value operators ‘:’ and ‘_’ and discussive implication (! ), discussive conjunction (^ ) and discussive equivalence d d ($ ). The set of all discussive formulas is denoted by ‘For ’. d d 3.1. Basics of Normal Modal Logics A normal modal logic is a set M  For that fulfils the following conditions: 1. CL  M, 2. M is closed under modus ponens (mp), uniform substitution (us) and necessitation rule (rn): if j and (j ! y) belong of M, so does y. (mp) if j 2 M then s(j) 2 M, (us) if j 2 M thenj 2 M, (rn) Axioms 2019, 8, 108 3 of 17 3. M contains formulas (df) and (K) p $ ::p (df) (p ! q) ! (p ! q) (K) As it is known, every normal modal logic contains the following formulas (p ! q) ! (p ! q) (1) (p ! q) ! (p ! q) (2) (p ! q) ! (p ! q) (3) D is the smallest normal logic containing (D): p ! p (D) Standardly, K is the smallest normal modal logic and S5 = KT5, that is, S5 is the smallest normal modal logic containing (T) and (5), where p ! p (T) p ! p (5) 4. Discussive Logics In the original formulation every two participants are connected one to another—in fact, for the explication of discussive implication one reads: ‘if anyone states that p’. The same idea is applied for the modality that is corresponding to possibility expressing the point of view of an external observer. Hence, Jaskowski’s ´ discussive logic D is defined by means of S5 as follows: D := f A 2 For : i (A) 2 S5g , 2 d 1 where i is a translation of discussive formulas into the modal language, that is, i is a function from 1 1 For into For such that: d m 1. i (a) = a, for any propositional letter a, 2. for any A, B 2 For : (a) i (:A) = :i (A), 1 1 (b) i (A _ B) = i (A) _ i (B), 1 1 1 (c) i (A ^ B) = i (A) ^ i (B), 1 d 1 1 (d) i (A ! B) = i (A) ! i (B). 1 d 1 1 (e) i (A $ B) = (i (A) ! i (B)) ^ (i (B) ! i (A)). 1 d 1 1 1 1 One can also consider a more general case. Let S be any normal modal logic. Now, we can define D := f A 2 For : i (A) 2 Sg . (4) S d 1 We easily see that in the case where there is no formula of the form(A) that would belong to a given modal logic S, then we have D = ?. In particular, for any modal logic S that is determined by a class of Kripke frames, whose accessibility relation does not fulfil seriality condition, we obtain D = ?. (We use standard results from modal logic, for details see for example, References [12,13].) Of course, if for a given normal modal logic S, we have (D) 2 S, then D  S. It is known (see Reference [6]) that one can consider various accessibility relations but the resulting discussive logic would be still the same. By definition, D = D . We easily see that S5 2 Axioms 2019, 8, 108 4 of 17 Fact 1. For any modal logics S and S , if S  S , then 1 2 1 2 D  D S S 1 2 By induction on the complexity of a formula j 2 For , we can obtain: Fact 2. For every j 2 For , there is A 2 For such that i (A) $ j 2 K. m d 1 In this paper we focus on the case where in the condition (4), D is taken as the modal system S. We denote the resulting system as D . Thus, by definition D := f A 2 For : i (A) 2 Dg . (5) 0 d 1 In the context of the definition of D , first, let us observe that: Lemma 1. For any A, A , . . . , A 2 For and any variables a , . . . , a , 1 n d 1 n (i (A))(a /i (A ), . . . , a /i (A )) = i (A(a /A , . . . , a /A )) 2 D. n n n n 1 1 1 1 1 1 1 1 Proof. The proof goes by induction on the complexity of a formula A. For the initial case, let A = a . We have: (i (a ))(a /i (A ), . . . , a /i (A )) = i (A ) = i (a (a /A , n n i 1 i 1 1 1 1 1 i 1 i 1 1 . . . , a /A )). If A is a variable that does not belong to fa , . . . , a g, we have (i (A))(a /i (A ), . . . , n n 1 n 1 1 1 1 a /i (A )) = A = i (A(a /A , . . . , a /A )). n n n n 1 1 1 1 For the inductive step assume that inductive hypothesis holds for B and C. For the case of discussive conjunction observe that the following equations hold: (i (B ^ 1 d C))(a /i (A ), . . . , a /i (A )) = (i (B) ^ i (C))(a /i (A ), . . . , a /i (A )) = 1 1 1 n 1 n 1 1 1 1 1 n 1 n (i (B))(a /i (A ), . . . ,a /i (A )) ^ (i (C))(a /i (A ), . . . , a /i (A )). Using n n n n 1 1 1 1 1 1 1 1 1 1 inductive hypothesis and features of substitution, we have (i (B))(a /i (A ), . . . , 1 1 1 1 a /i (A )) ^ (i (C))(a /i (A ), . . . , a /i (A )) = (i (B))(a /i (A ), . . . , a /i (A )) ^ n n n n n n 1 1 1 1 1 1 1 1 1 1 1 ((i (C))(a /i (A ), . . . , a /i (A ))) = i (B(a /A , . . . , a /A )) ^ i (C(a /A , . . . , 1 1 1 1 n 1 n 1 1 1 n n 1 1 1 a /A )) = i ((B(a /A , . . . , a /A ) ^ C(a /A , . . . , a /A ))) = i ((B ^ C)(a /A , . . . , a /A )). n n n n n n n n 1 1 1 d 1 1 1 d 1 1 Similarly, also the proofs for :, _, ! and $ are straightforward. d d Fact 3. The set D is closed under substitution and modus ponens with respect to ! . 0 d Proof. Let A 2 D and A ! B 2 D , that is i (A) 2 D and i (A ! B) 2 D, so (i (A) ! 0 0 1 1 1 i (B))) 2 D, by the distributivity of with respect to ! i (A) ! i (B) 2 D, but by normality 1 1 1 i (A) 2 D, hencei (B))) 2 D and by definition (4), B 2 D . 1 1 0 Assume now that A 2 D , that is i (A) 2 D. Let us consider a result of uniform substitution 0 1 s(A) into A of formulas A for variables in A, where 1 6 i 6 n, for some n, that is, s(A) = A(a /A , . . . , a /A ), where a are all variables in A. By Lemma 1 we know that i (s(A)) = n n 1 1 i 1 (i (A))(a /i (A ), . . . , a /i (A )). Since D is a logic, so it is closed on substitution, so also 1 1 1 1 n 1 n (i (A))(a /i (A ), . . . , a /i (A )) 2 D. But the following equations hold (i (A))(a /i (A ), n n 1 1 1 1 1 1 1 1 1 . . . , a /i (A )) = (i (A)(a /i (A ), . . . , a /i (A ))) = i (s(A)), therefore s(A) 2 D . n 1 n 1 1 1 1 n 1 n 1 0 Axioms 2019, 8, 108 5 of 17 4.1. A Comparison with Some Classical Theses As one can easily see, none of the classical cases given below belong to D , although each of these formulas belong to D . To stress discussive interpretation we use the formulas from For . p ! p p ! p _ q p ^ q ! p d d p ! (q ! (p ^ q)) d d d (p ! (q ! r)) ! ((p ! q) ! (p ! r)) d d d d d d (p ! q) ! ((q ! r) ! (p ! r)) d d d d d ::p ! p p ! ::p Each of these formulas can be rejected semantically. We use standard completeness theorem with respect to Kripke semantics for the logic D. As an example, let us consider the fifth formula, known as Frege syllogism. One can easily see that the respective translation: ((p ! (q ! r)) ! ((p ! q) ! (p ! r))) is not a thesis of D, so the formula (p ! (q ! r)) ! ((p ! q) ! (p ! r)) does not belong d d d d d d to D . Similarly one falsifies the other cases. 5. A Kotas Style Deductive System for the Smallest Discussive Logic We will characterise a discussive logic being a result of the given variant of the discussive model; that is in the case that the relation is serial and no other condition is assumed as regards accessibility relation. We will give an adequacy result for the given deductive system. We will adopt a method of Kotas (see Reference [14]) that was used for indicating the way in which D could be axiomatized. (There are other axiomatisations of D . In Reference [15] there is 2 2 an axiomatisation of discussive logic but in a version with left discussive conjunction. For not so straight history of axiomatisation of D see References [16,17].) The same method was used inter alia in Reference [1] to axiomatize a variant of D with modal operators. Let us use the following notation: (Ai) denotesf, for (Ai) denoting f (6) -S = fA 2 For : A 2 Sg (7) -S is called an M-counterpart of S (see Reference [5, p. 70]). By definitions, for any normal logic S  D: S  -S It is known that (see Reference [5, p. 68]): Fact 4. -D = D (8) Axioms 2019, 8, 108 6 of 17 Consider the following axiomatisation of CL: p ! (q ! p) (A1) (p ! (q ! r)) ! ((p ! q) ! (p ! r)) (A2) p^ q ! p (A3) p^ q ! q (A4) p ! (q ! p^ q) (A5) p ! p_ q (A6) q ! p_ q (A7) (p ! q) ! ((r ! q) ! (p_ r ! q)) (A8) (p $ q) ! (p ! q) (A9) (p $ q) ! (q ! p) (A10) (p ! q) ! ((q ! p) ! (p $ q)) (A11) (:p ! :q) ! (q ! p) (A12) and formulas (p $ ::p) (df) ((p ! q) ! (p ! q)) (K) (p ! p) (D) (p ! p) (T) (p ! p) (5) Let W := f(Ai) : 1 6 i 6 12g [ f(df), (K), (D)g and let W := f(Ai) : 1 6 i 6 12g [ f(df), (K), (T), (5)g Let us recall a theorem that allows to formulate S5 syntactically with the use of the above mentioned formulas and rules. Fact 5 ([14]). 1. S5 is the smallest set including W and closed under (us) and the following rules: j, (j ! y) (mp) (rn) (rn ) 2. S5 is the smallest set including W and closed under (us), (mp) and (rn). 3. -S5 is the smallest set including W and closed under (us), (mp), (rn), (rn ) and (rp ): 1 ( (rp ) j Axioms 2019, 8, 108 7 of 17 But in a quite similar way, one can formulate the logic D. Let D denote the smallest set including W and closed under substitution, (rn), (mp), (rp ) and (mp ) j, (j ! y) (mp ) We will follow a custom used for modal logics of calling elements of D theses of a deductive system. So D is the set of theses with respect to a deductive system determined by the given axioms (Ai) : 1 6 i 6 12 and rules (rn), (mp), (mp ), (rp ) and an substitution. Lemma 2. D = D . Proof. We show that D  D. First, by the standard formulation of D and (rn) we see that W  D—it is enough to use necessitation for respective axioms of D. Besides by (8), D is closed on (rp ). We will prove that D is closed on (mp ). Assume that j,(j ! y) 2 D. By (rn),j 2 D, while by (D), we have(j ! y) 2 D hence using (3) we obtainj ! y 2 D. Thus, by modus ponensy 2 D and by (8), y 2 D. The fact that D is closed on (mp) follows by axiom (K) and modus ponens. Finally, D is closed on (rn) by necessitation. For the reverse direction let us assume that j 2 D. We can consider a proof j ,. . . , j = j of j in the standard axiomatisation of D. First observe that by (mp) and Ai, where, 1 6 i 6 12 we obtainy, for any classical tautology y — it is enough to consider a prove of y and the basis of the system with fAi : 1 6 i 6 12g as axioms, with modus ponens and substitution as rules of inference and next precede every element of the proof by  and observe that the obtained sequence j ,. . . , j is a proof ofy on the basis of the given system of D . Second, we see that any other axiom of D preceded by becomes an axiom of D ; besides, rules of (rn) and (mp) correspond respectively to necessitation and modes ponens in the original proof of j. Hence, using induction on the length of the proof we see that j has a mentioned proof in D . We extend the sequence j ,. . . , j = j to infer j. By (D) we have(j ! j) and so using (mp ) andj we getj, hence by (rp ) we infer j. Let us finally add that both sets are closed in substitution. In Reference [14] two translations were considered. i is a natural version of the first one adjusted to the considered here language. The translation i : For ! For given below is a version of i 2 m d 2 defined in Reference [14] where the case of is added: 1. i (a) = a, for any propositional letter a, 2. for any j, y 2 For : (a) i (:j) = :i (j), 2 2 (b) i (j) = :((:p _ p) ^ :i (j)), 2 2 (c) i (j) = (:p _ p) ^ i (j), 2 d 2 (d) i (j _ y) = i (j) _ i (y), 2 2 2 (e) i (j ^ y) = :(:i (j) _ :i (y)), 2 2 2 (f) i (j ! y) = :i (j) _ i (y), 2 2 2 (g) i (j $ y) = :(:(:i (j) _ i (y)) _ :(:i (y) _ i (j))). 2 2 2 2 2 The below Lemma is being proved similarly as Lemma 4.2 in Reference [1]. Lemma 3. For any j 2 For , i (i (j)) $ j 2 D. m 1 2 Proof. The proof goes by induction on the complexity of a given formula. If j is a variable, we have i (i (j)) = j, thus the thesis holds trivially. 1 2 Assume that the inductive thesis holds for formulas simpler than a given formula. Firstly, we have i (i (j_ y)) = i (i (j)_ i (y)) = i (i (j))_ i (i (y)). Thus, i (i (j_ y)) $ (j_ y) 2 D, 1 2 1 2 2 1 2 1 2 1 2 Axioms 2019, 8, 108 8 of 17 by CL. Similarly by definition, i (i (:j)) = i (:i (j)) = :i (i (j)), so the required equivalence 1 2 1 2 1 2 holds by CL. For the case of , we have: i (i (j)) = i (:((:p _ p) ^ :i (j))) = :((:p _ p) ^ 1 2 1 2 :i (i (j))), so the required equivalence holds by normality, in particular, by CL, extensionality and 1 2 due to the fact that ::p $ p 2 K. For the case of ‘’, we have: i (i (j)) = i ((:p _ p) ^ i (j)) = (:p _ p) ^ i (i (j)) so again, 1 2 1 d 2 1 2 the required equivalence holds by normality. Secondly, by CL and due to the following equations and equivalences, the inductive thesis holds for ‘^’, ‘!’ and ‘$’. For ‘^’: i (i (j^ y)) = i (:(:i (j) _ :i (y))) = :(:i (i (j)) _ :i (i (y))). But, of course, 1 2 1 2 2 1 2 1 2 :(:i (i (j)) _ :i (i (y))) $ (i (i (j))^ i (i (y))) 2 D. 1 2 1 2 1 2 1 2 For the case of ‘!’: i (i (j ! y)) = i (:i (j) _ i (y)) = :i (i (j)) _ i (i (y)). 1 2 1 2 2 1 2 1 2 But :i (i (j)) _ i (i (y)) $ i (i (j)) ! i (i (y)) 2 D. 1 2 1 2 1 2 1 2 For ‘$’: i (i (j $ y)) = i (:(:(:i (j) _ i (y)) _ :(:i (y) _ i (j)))) = :(:(:i (i (j)) 1 2 1 2 2 2 2 1 2 _ i (i (y))) _ :(:i (i (y)) _ i (i (j)))). However, :(:(:i (i (j)) _ i (i (y))) _ 1 2 1 2 1 2 1 2 1 2 :(:i (i (y)) _ i (i (j)))) $ (i (i (j)) $ i (i (y))) 2 D. 1 2 1 2 1 2 1 2 Due to Fact 4, we also have a connection similar to the relation between D and-S5: Lemma 4. 1. For any A 2 For : A 2 D iff i (A) 2 D. 0 1 2. For any j 2 D, we have i (j) 2 D . 2 0 3. If j 2 D and j $ y 2 D, then y 2 D. Proof. Ad 1. Let A 2 D . By the definition of D it means thati (A) 2 D, that is, i (A) 2 -D. Thus, 0 0 1 1 by Fact 4, i (A) 2 D. If i (A) 2 D, then by necessitation and (D),i (A) 2 D, so A 2 D . 1 1 0 Ad 2. Let j 2 D, that is,j 2 D. Then, by Lemma 3 and extensionality for D, we havei (i (j)) 2 D. 1 2 Thus, i (A) 2 D . 2 0 Point 3 is obvious. To make the following consideration easier to follow, for A, B 2 For , let us denote the formula d d d :A _ B as A ! B, and :((:p _ p) ^ :A) as A, (:p _ p) ^ A as A, and (A ! B)), that c c d d is :((:p _ p) ^ :(:A _ B)) as A J B. d d Let ` be the consequence relation determined by the set i (W) and the following formulas: i (i (q ^ r)) J (q ^ r) (B1) 2 1 d d d (i (i (q ! r)) J (q ! r)) (B2) 2 1 d d d (i (i (q $ r)) J (q $ r)) (B3) 2 1 d d d ((q ^ r) J i (i (q ^ r))) (C1) d d 2 1 d ((q ! r) J i (i (q ! r))) (C2) d d 2 1 d ((q $ r) J i (i (q $ r))) (C3) d d 2 1 d Axioms 2019, 8, 108 9 of 17 as axioms together with substitution and the following rules: A (A J B) ( mp ) str A (A J B) d 0 ( mp ) str ( rn) d d (rp ) The proof of the following lemma is straightforward by induction on the complexity of a modal formula j. Lemma 5. Let j, y , . . . , y be modal formulas and y be a result of substitution of y , . . . , y respectively 1 n 1 n for atoms a , . . . , a in j. Then the formula i (y) equals the result of substitution of i (y ), . . . , i (y ) for 1 n 2 2 1 2 n atoms a , . . . , a in i (j). 1 n 2 Directly from definitions and used notation, we have: Fact 6. For any j, y 2 For 1. i ((j)) =  (i (j)), 2 2 2. i ((j)) =  (i (j)), 2 2 3. i ((j ! y)) = i (j) J i (y). 2 2 d 2 Lemma 1. 1. For any j 2 CL, we have `  i (j). D 2 2. For any j 2 D, we have ` i (j). Proof. Ad 1. Assume that j 2 CL. Then there is a proof c , . . . , c , of j = c on the basis of n n d d (A1)–(A12), (mp) and substitution. Consider the sequence  i (c ), . . . ,  i (c ). By induction 2 1 2 n on the length of the sequence one can see that it is a proof on the basis of ` , since its elements are either elements of i (W) or arise by the application of ( mp ) or substitution. For the case of str substitution it is enough to use Lemma 5 and apply the substitution of i (y ), . . . , i (y ) for a , . . . , 2 1 2 1 a in i (c ), if in the initial proof a substitution of formulas y , . . . , y for atoms a , . . . , a in c m 2 i 1 m 1 m i was applied. Ad 2. Assume that j 2 D. Then there is a proof c , . . . , c of j, in the sense of the consequence 1 n d d d relation . Consider i (c ), . . . , i (c ), ( i (c ) J  i (c )), i (c ), i (c ) = i (j). By n n n n n 2 1 2 2 d 2 2 2 2 induction on 1 6 i 6 n, by the point 1 of this lemma and Fact 6, we can easily show that ` i (c ), 2 i d d d d that is,`  i (c ), while ( i (c ) J  i (c )) is an instance of i (D), i (c ) follows from n n n D 2 i 2 d 2 2 2 d d d 0 d d i (c ) and ( i (c ) J  i (c )) by ( mp ); and i (j) follows from i (c ) by (rp ). 2 n 2 n 2 n 2 2 n str ( Thus, we obtain that: Fact 7. The following formulas are theses with respect to ` : (i (i (:p)) J :p) (9) 2 1 d (i (i (p _ q)) J p _ q) (10) 1 d d d Proof. For (9), observe that (i (i (:p)) J :p) =  (i (i (:p)) ! :p) =  (:p ! :p) = 2 1 d 2 1 c c i (:p ! :p). So (9) follows by Lemma 1.1. 2 c Axioms 2019, 8, 108 10 of 17 For (10), one can see that (i (i (p _ q)) J p _ q) =  (i (i (p) _ i (q)) ! p _ q) = 2 1 2 1 1 c d d (i (i (p)) _ i (i (q)) ! p _ q) =  (p _ q ! p _ q). So again, the condition is obtained by c c 2 1 2 1 Lemma 1.1. The above fact can be extended for the case of any formulas used instead of p and q. Moreover, it can be generalised to any compound formula which results in the below Lemma. Its proof goes similarly as the proof of Reference [1, Fact 4.6]. However, there are essential changes for the case of discussive operators, so we present it for the sake of completeness of considerations. Fact 8. For any A 2 For , `  (i (i (A)) ! A) (11) 2 c D 1 `  (A ! i (i (A))). (12) D c 2 1 Proof. The proof goes simultaneously for both theses by induction on the complexity of a formula A. The case of atoms follows by Lemma 1.1. Assume that the inductive hypothesis holds for any formula of complexity smaller than the complexity of A. That is, for the following cases A = :B, A = B_ C, A = B ^ C, A = B ! C and A = B $ C, d d d where B, C 2 For we assume that: ` (i (i (B)) J B), D 1 d ` (i (i (C)) J C), D 2 1 d ` (B J i (i (B))), D d 1 ` (C J i (i (C))). D d 2 1 in other words `  (i (i (B)) ! B), (13) 2 c D 1 `  (i (i (C)) ! C), (14) D 2 1 c `  (B ! i (i (B))), (15) D c 2 1 `  (C ! i (i (C))). (16) c 2 D 1 For the case of ‘:’ let us notice that `  i (p ! q) ! (:q ! :p) , by Lemma 1(1), that is, ` ((p ! q) J (:q ! :p)). So, since :i (i (B)) = i (i (:B)), using the substitution p/B, c c D d 2 1 2 1 q/i (i (B)), (15) and ( mp ), we get: 2 1 str `  (i (i (:B)) ! :B). D 2 1 c Similarly, using the substitution p/i (i (B)), q/B, (13) and ( mp ) we obtain: 2 1 str `  (:B ! i (i (:B))). D 2 1 For the case of ‘_’ notice that `  i (p ! q) ! ( r ! s) ! ((p _ r) ! (q _ s))) , by Lemma 1(1), that is, `  ((p ! q) ! ((r ! s) ! ((p _ r) ! (q _ s)))) or equivalently D c c c c c (p ! q) J ((r ! s) ! ((p _ r) ! (q _ s))) (17) c c c c is a thesis with respect to ` . Thus, since i (i (B)) _ i (i (B)) = i (i (B _ C)), using the 2 1 2 1 2 1 substitution p/i (i (B)), q/B, r/i (i (C)), s/C into (17), by (13) and ( mp ), we get: 2 1 2 1 str `  ((i (i (C)) ! C) ! ((i (i (B)) _ i (i (C))) ! (B _ C))) c c c D 2 1 2 1 2 1 0 Axioms 2019, 8, 108 11 of 17 that is, ` (i (i (C)) ! C) J ((i (i (B)) _ i (i (C))) ! (B _ C)) c c D 2 1 d 2 1 2 1 And again, by (14) and ( mp ), we obtain: str `  i (i (B_ C)) ! (B _ C) . D 2 1 Similarly, using the substitution p/B, q/i (i (B)), r/C, s/i (i (C)), to (17), we obtain: 2 1 2 1 (B ! i (i (B))) J c 2 1 J ((C ! i (i (C))) ! ((B _ C) ! (i (i (B)) _ i (i (C))))) d c 2 1 c c 2 1 2 1 d d hence, by (15) and ( mp ), and again by (16) and ( mp ) we get: str str `  (B _ C) ! i (i (B_ C)) . c 2 1 For the case of ‘^ ’ first let us observe that i (i (B ^ C)) = i (i (B) ^ i (C)) = 2 1 d 2 1 1 :(:i (i (B)) _ :i (i (C))) = (18) 2 1 2 1 :(:i (i (B)) _ :((:p _ p) ^ i (i (C)))). 2 1 d 2 1 Hence by (B1) and definitions of i and i we get ` :(:q _ :((:p _ p) ^ r)) J (q ^ r). While 1 2 D d d d by (C1), similarly we obtain: ` (q ^ r) J :(:q _ :((:p _ p) ^ r)). Therefore, by substitution D d d d we obtain ` :(:B _ :((:p _ p) ^ C)) J (B ^ C) (19) D d d d and ` (B ^ C) J :(:B _ :((:p _ p) ^ C)) (20) D d d d Notice that ((t ! q) ! ((r ! s) ! (t ^ r ! q ^ s))) 2 D, so by Lemma 1(2) and Fact 6, `  (i ((p ! q) ! ((r ! s) ! (t ^ r ! q ^ s)))), that is, D 2 ` (t ! q) J D c d (21) ((r J s) ! (:(:t _ :((:p _ p) ^ r)) ! :(:q _ :((:p _ p) ^ s)))). c c d d d By substitution: t/i (i (B)), q/B, r/i (i (C)), s/C, (13) and ( mp ), we get: 2 1 2 1 str ((i (i (C)) J C) ! 2 c 1 d (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! :(:B _ :((:p _ p) ^ C)))) 2 1 d 2 1 c d But by ( rn) applied to (14) we have `  (i (i (C)) J C) D 2 1 d Therefore, again by ( mp ): str (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! :(:B _ :((:p _ p) ^ C))) 2 1 d 2 1 c d But by Lemma 1(1) we have ` (p ! q) J ((q ! r) ! (p ! r)), (22) c c c c D d 0 Axioms 2019, 8, 108 12 of 17 so by substitution p/:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))), q/:(:B _ :((:p _ p) ^ C)) 2 1 2 1 d d and r/(B ^ C), using ( mp ) we obtain: str ((:(:B _ :((:p _ p) ^ C)) ! (B ^ C)) ! d c d c (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! (B ^ C))) 2 2 c 1 d 1 d that is, (:(:B _ :((:p _ p) ^ C)) ! (B ^ C)) J d d d (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! (B ^ C)) 2 1 2 1 c d d Thus, from (19) using ( mp ) we infer str (:(:i (i (B)) _ :((:p _ p) ^ i (i (C)))) ! (B ^ C)) 2 1 d 2 1 c d what is the required formula due to the observation (18). For the reverse implication, using (21) but substituting t/B, q/i (i (B)), r/C, s/i (i (C)) and next 2 1 2 1 appyling (15) and ( mp ) we infer str ((C J i (i (C))) ! 2 1 c (:(:B _ :((:p _ p) ^ C)) ! :(:i (i (B)) _ :((:p _ p) ^ i (i (C)))))) d c 2 1 d 2 1 While applying ( rn) for (16) we obtain `  (C J i (i (C))) 2 1 D d Thus, by ( mp ): str (:(:B _ :((:p _ p) ^ C)) ! :(:i (i (B)) _ :((:p _ p) ^ i (i (C))))) d c 2 1 d 2 1 Using an instance of (22), where p/(B ^ C), q/:(:B _ :((:p _ p) ^ C)) and r/:(:i (i (B)) _ d d 2 1 :((:p _ p) ^ i (i (C)))), by (20) and ( mp ), and then thanks to the above formula and again 2 1 str ( mp ) we obtain str ((B ^ C) ! :(:i (i (B)) _ :((:p _ p) ^ i (i (C))))) c 2 2 d 1 d 1 which is the required formula by the observation (18). The case of ‘! ’. By definitions, we have: i (i (B ! C)) = i (i (B) ! i (C)) = 2 1 2 1 1 (23) :((:p _ p) ^ i (i (B))) _ i (i (C)) d 2 1 2 1 Thus, by (B2) and (C2) we have :((:p _ p) ^ q) _ r J (q ! r)) d d d (q ! r) J :((:p _ p) ^ q) _ r d d d So by substitution we have :((:p _ p) ^ B) _ C J (B ! C)) (24) d d d (B ! C) J :((:p _ p) ^ B) _ C (25) d d d Axioms 2019, 8, 108 13 of 17 Let us notice that ((q ! r) ! (q ! r)) 2 K  D. Hence, by Lemma 1(2): ` i (((q ! r) ! (q ! r))), that is, by definition of i and by Fact 6: 2 2 d d d d d d `  (  (q ! r) !  ( q !  r)). c c c or equivalently d d d `   (q ! r) J  (((:p _ p) ^ q) ! ((:p _ p) ^ r)). (26) D c d d c d so by substitution q/B, r/i (i (B)), we obtain that 2 1 d d (B ! i (i (B))) J c 2 1 d (27) (((:p _ p) ^ B) ! ((:p _ p) ^ i (i (B)))). d c d 2 1 d d d d 0 is a thesis of D . Applying ( rn) to (15) we get  (B ! i (i (B))), hence by ( mp ) we infer 0 2 1 str (((:p _ p) ^ B) ! ((:p _ p) ^ i (i (B)))). c 2 1 d d By a substitution q/C, r/i (i (C)) in (26) and by ( rn) applied for (16) instead of (15) and finally by 2 1 d 0 ( mp ) we obtain: str (((:p _ p) ^ C) ! ((:p _ p) ^ i (i (C)))). (28) c 2 d d 1 As one can see,((q ! t) ! ((r ! s) ! ((t ! r) ! (q ! s)))) 2 K  D. Hence by Lemma 1(2) we obtain (((:p _ p) ^ q) ! ((:p _ p) ^ t)) J d d d (29) ((r ! s) ! ((((:p _ p) ^ t) ! r) ! (((:p _ p) ^ q) ! s))) c c d c c d c Now, we use the substitution: q/B, t/i (i (B)), r/i (i (C)), s/C and applying ( mp ) to (5) we 2 2 1 1 str infer (i (i (C)) ! C) J 2 1 d ((((:p _ p) ^ i (i (B))) ! i (i (C))) ! (((:p _ p) ^ B) ! C)) 2 1 c 2 1 c c d d and next by ( mp ) applied to (14) we have str (((:p _ p) ^ i (i (B))) ! i (i (C))) J (((:p _ p) ^ B) ! C) c c d 2 1 2 1 d d But by (23) it means that ` i (i (B ! C)) J (((:p _ p) ^ B) ! C) (30) 2 1 c D d d d Now, we use (22), (24) and the above formula and act similarly as in the case of ‘^ ’, we conclude that: ` i (i (B ! C)) J (B ! C) . D 2 1 d d d For the reverse implication we apply the following substitution to (29): q/i (i (B)), t/B, r/C, 2 1 s/i (i (C)) and we receive: 2 1 (((:p _ p) ^ i (i (B))) ! (:p _ p) ^ B)) J 2 1 c d d d J ((C ! i (i (C))) ! (31) d c 2 1 c ((((:p _ p) ^ B) ! C) ! (((:p _ p) ^ i (i (B))) ! i (i (C))))) c c 2 1 c 2 1 d d Axioms 2019, 8, 108 14 of 17 Similarly as (5) we obtain  (((:p _ p) ^ i (i (B))) ! ((:p _ p) ^ B)). Hence, applying 2 1 c d d ( mp ) to (31) we infer str (C ! i (i (C))) J c 2 1 d ((((:p _ p) ^ B) ! C) ! (((:p _ p) ^ i (i (B))) ! i (i (C)))) d c c d 2 1 c 2 1 So again by ( mp ) and (16) we obtain str (((:p _ p) ^ B) ! C) J (((:p _ p) ^ i (i (B))) ! i (i (C))) c c d d d 2 1 2 1 So acting as previously, by (22), (25), (23) and ( mp ) we obtain str `  (B ! C) ! i (i (B ! C)) . D d c 2 1 d For the case of ‘$ ’ notice that by Lemma 1(1), `  (i ((p ! q) ! ((q ! p) ! (p $ q)))), d D 2 that is, `  ((p ! q) ! ((q ! p) ! :(:(p ! q) _ :(q ! p)))). Thus, by substitutions, c c c c c c inductive hypotheses (13), (14), (15), (16) and applying ( mp ) and definition of i we get: str :(:(B ! i (i (B))) _ :(i (i (B)) ! B)) (32) c c 2 1 2 1 :(:(C ! i (i (C))) _ :(i (i (C)) ! C)) (33) c 2 1 2 1 c Hence, by the use of the following thesis of K  D: (r $ s) ! (t $ q) ! (r $ s) ! ((q ! s) ^ (s ! q)) ! ((t ! r) ^ (r ! t))) , by Lemma 1(2), Fact 6, (33), ( mp ) and substitution r/C, s/i (i (C)), t/B, q/i (i (B)) we get: 2 1 2 1 str d d :(:(B ! i (i (B))) _ :(i (i (B)) ! B)) ! c 2 1 2 1 c c d d :(:(:C _ i (i (C))) _ :(:i (i (C)) _ C)) 2 1 2 1 d d d ! :((: i (i (B)) ! i (i (C))) _ : ( i (i (C)) ! i (i (B)))) c 2 1 c 2 1 2 1 c 2 1 d d d ! :(:( B ! C) _ : ( C ! B))) c c c d d By the result of application of ( rn) to (33) and again ( mp ) we infer str d d d :(:(:C _ i (i (C))) _ :(:i (i (C)) _ C)) 2 1 2 1 d d d ! :((: i (i (B)) ! i (i (C))) _ : ( i (i (C)) ! i (i (B)))) c 2 1 c 2 1 2 1 c 2 1 d d d ! :(:( B ! C) _ : ( C ! B))) c c c d d Now we twice apply ( rn) to (33) and again use ( mp ), as a result we get: str d d d d (:(:( i (i (B)) ! i (i (C))) _ : ( i (i (C)) ! i (i (B)))) ! 2 1 c 2 1 2 1 c 2 1 c d d d :(:( B ! C) _ : ( C ! B))). c c Thus, since by definitions of the functions i and i , :(:( i (i (B)) ! i (i (C))) _ 1 2 2 1 2 1 d d : ( i (i (C)) ! i (i (B)))) = i ((i (B) ! i (C)) ^ (i (C) ! i (B))) = i (i (B $ 2 1 c 2 1 2 1 1 1 1 2 1 C)), we get: d d d d (i (i (B $ C)) ! :(:( B ! C) _ : ( C ! B))). 2 1 c c c d Axioms 2019, 8, 108 15 of 17 From axiom (B3) we obtain: d d d d (:(:( B ! C) _ : ( C ! B)) ! (B $ C)). c c c d Thus, again by a substitution to i  (p ! q) ! (q ! r) ! (p ! r)) and the application of ( mp ), we get: str `  i (i (B $ C)) ! (B $ C) . D 2 1 d c d Similarly we show: `  (B $ C) ! i (i (B $ C)) . D d 2 1 d By induction on the complexity of formulas, we obtain (11) and (12). Theorem 1. The set of theses with respect to the consequence relation ` equals D . Proof. Let A 2 D . By Lemma 4, i (A) 2 D. Thus, by Lemma 2, there is a proof c , . . . , c = i (A) 0 1 1 1 such that for each i 2 f1, . . . , ng, c is one of the formulas (A1)–(A12), (df), (D), (K) or c is i i a result of the application of substitution, (rn), (mp), (mp ), (rp ), for some formulas preceding c in the sequence. Let us consider the following sequence of formulas i (c ), . . . , i (c ), i (i (A)), i 2 1 2 n1 2 1 (i (i (A)) ! A), A. By induction on i we see that the fragment of the sequence i (c ), . . . , 2 1 c 2 1 i (c ) = i (i (A)) is a proof in the given axiomatic system, while the formula (i (i (A)) ! A) 2 n 2 1 2 1 c is a thesis of the system, by Fact 8. So the formula A completes the proof as a result of application of d 0 the rule ( mp ) to two preceding formulas. Thus, ` A str 0 Now, for the reverse direction, assume that for a given formula A there is a proof C , . . . , C = A of 1 n the formula A within the considered deductive system. By the definition of D , it is enough to prove that for any i 2 f1, . . . , ng,i (C ) 2 D or, equivalently, i (C ) 2 D. 1 i 1 i Firstly, let us consider the case of axioms. Suppose that C 2 i (W). For the case (A1)–(A12) that is, when C = i (j), for some j 2 CL  D—it is enough to apply Lemma 1(2). Then i 2 i (i (j)) $ j 2 D, by Lemma 3. Therefore, by Lemma 4(3), i (i (j)) = i (C ) 2 D. In the 1 2 1 2 1 case of other axioms from the set i (W), we act similarly. d d Ad(B1): i ( (i (i (q ^ r)) ! (q ^ r))) = i ( (i (q ^ r) ! (q ^ r))) = i (:((:p _ p) ^ 1 2 1 c 1 2 c 1 d d d d :(:(:q _ :((:p _ p) ^ r)) ! (q ^ r)))) = :((:p _ p) ^ :(:(:q _ :((:p _ p) ^ r)) ! d c d c (q ^ r))). But :((:p _ p) ^ :(:(:q _ :((:p _ p) ^ r)) ! (q ^ r))) $ ((q ^ r) ! (q ^ c c r)) belongs to D. Thus, (B1) 2 D , thanks to Lemma 4. Ad (B2): i ( (i (i (q ! r)) ! (q ! r))) = i (:((:p _ p) ^ :(((:p _ p) ^ q ! r) ! 2 c c c 1 1 d d 1 d d (q ! r)))) = :((:p _ p) ^ :(((:p _ p) ^ q ! r) ! (q ! r))). However, :((:p _ p) ^ d c c :(((:p _ p) ^ q ! r) ! (q ! r))) $ ((q ! r) ! (q ! r)) is a thesis of D. Thus, c c c c (B2) 2 D , by Lemma 4. d d Ad (B3): i ( (i (i (q $ r)) ! (q $ r))) = i ( (i ((q ! r) ^ (r ! q)) ! (q $ 2 c 2 c 1 1 d d 1 d r))) = i (:((:p _ p) ^ :(:(:((:p _ p) ^ q ! r) _ :((:p _ p) ^ ((:p _ p) ^ r ! q))) ! 1 d d c d d c c (q $ r)))) = :((:p _ p) ^ :(:(:((:p _ p) ^ q ! r) _ :((:p _ p) ^ ((:p _ p) ^ r ! c c q))) ! ((q ! r) ^ (r ! q)))). Notice that :((:p _ p) ^ :(:(:((:p _ p) ^ q ! r) _ c c :((:p _ p) ^ ((:p _ p) ^ r ! q))) ! ((q ! r) ^ (r ! q)))) $ ((q ! r) ^ (r ! c c c c q) ! ((q ! r) ^ (r ! q))). Thus, (B3) belongs to D , similarly, by Lemma 4. c 0 Ad (C1): i ( ((q ^ r) ! i (i (q ^ r)))) = :((:p _ p) ^ :((q ^ r) ! :(:q _ :((:p _ c 2 c 1 d 1 d p) ^ r)))). Thus again, (C1) 2 D . Ad (C2): i ((q ! r) J i (i (q ! r))) = :((:p _ p) ^ :((q ! r) ! ((:p _ p) ^ q ! r))). c c 1 d d 2 1 d Hence (C2) 2 D . Ad (C3): i ((q $ r) J i (i (q $ r))) = :((:p _ p) ^ :(((q ! r) ^ (r ! q)) ! 1 d d 2 1 d :(:((:p _ p) ^ q ! r) _ :((:p _ p) ^ ((:p _ p) ^ r ! q))))). As one can see (C3) 2 D . c c 0 d d d Ad ( mp ). Assume that  A and  (A ! B) belong to D , that is, i (:((:p _ p) ^ :A)) 0 1 d str and i (:((:p _ p) ^ :(A ! B))) are theses of D. By Fact 4 equivalently, (:((:p _ p) ^ 1 d c Axioms 2019, 8, 108 16 of 17 :i (A))) 2 D and (:((:p _ p) ^ :(i (A) ! i (B)))) 2 D, in other words i (A) 2 D and 1 1 c 1 1 (i (A) ! i (B)) 2 D, hence of course i (B) 2 D. Equivalently, ::i (B) 2 D and :((:p _ 1 1 1 1 p) ^ :i (B)) 2 D, but by definition of i , :((:p _ p) ^ :i (B)) = i (:((:p _ p) ^ :B), hence 1 1 1 1 also i (:((:p _ p) ^ :B)) 2 D, therefore B 2 D . 1 d 0 d 0 d d Ad ( mp ). Suppose that A and (A ! B) belong to D , that is,i (A) andi ( (A ! B)) c 0 1 1 c str belong to D; and so(:((:p _ p) ^ :(:i (A) _ i (B)))) 2 D. Therefore,(i (A) ! i (B)) 2 1 1 1 1 D and by Fact 4: (i (A) ! i (B)) 2 D. Hencei (B) 2 D, so B 2 D . by definition of D. 1 1 1 0 d d Ad ( rn): Let  A 2 D , that is, i (:((:p _ p) ^ :A)) 2 D; and in other words (:((:p _ 0 1 d p) ^ :i (A))) 2 D. But this means that i (A) 2 D and by Fact 4, also i (A) 2 D. Hence 1 1 1 by necessitationi (A) 2 D, so again by necessitation and (D) alsoi (A) 2 D. Equivalently, 1 1 ::::i (A) 2 D. This can be rewritten as :((:p _ p) ^ ::((:p _ p) ^ :i (A))) 2 1 1 d d D. That is i (:((:p _ p) ^ ::((:p _ p) ^ :A))) 2 D. Hence i (  A) 2 D, that 1 d d 1 d d is,  A 2 D . d d Ad (rp ): Let  A 2 D , that is, i ((:p _ p) ^ A) 2 D, equivalently (:p _ p) ^ i (A) 2 D,; 0 1 d 1 and soi (A) 2 D. Then by Fact 4, alsoi (A) 2 D; and so A 2 D . 1 1 0 Finally, we consider the case of substitution. Assume that A belongs to D , that is,i (A) is a thesis 0 1 of D. Now, let us consider a substitution of formulas A ,. . . , A for variables a ,. . . , a in A. Let 1 n 1 n us also consider i (A)(a /i (A ), . . . , a /i (A )) the result of substitution of i (A ),. . . , i /A for 1 1 1 1 n 1 n 1 1 n n variables a ,. . . , a in i (A). By Lemma 1 the following holds: (i (A))(a /i (A ),. . . , a /i (A )) = 1 n 1 1 1 1 1 n 1 n i (A(a /A ,. . . , a /A )). Since D as a modal logic is closed on substitution, (i (A))(a /A ,. . . , 1 1 1 n n 1 1 1 a /A ) 2 D, but by the last equation and the features of substitution, (i (A))(a /i (A ),. . . , n n 1 1 1 1 a /i (A )) = ((i (A))(a /i (A ),. . . , a /i (A ))) = i (A(a /A ,. . . , a /A )). By definition n 1 n 1 1 1 1 n 1 n 1 1 1 n n of D , it means that A(a /A ,. . . , a /A ) 2 D . 0 n n 0 1 1 6. Conclusions We gave a syntactic characterisation of the minimal discussive logic. This is as an initial step in our investigations on other variants of discussive logics obtained by other cases of relations that connect participants of a discussion. Author Contributions: Conceptualization, K.M.-N. and M.N.; formal analysis, K.M.-N. and M.N.; investigation, K.M.-N. and M.N.; methodology, K.M.-N.; validation, K.M.-N.; writing–original draft preparation, K.M.-N. and M.N.; writing–review and editing, K.M.-N. and M.N.; supervision, M.N.; funding acquisition, M.N. Funding: The authors of this work benefited from support provided by Polish National Science Centre (Narodowe Centrum Nauki), grant number 2016/23/B/HS1/00344. Conflicts of Interest: The authors declare no conflict of interest. References 1. Mruczek-Nasieniewska, K.; Nasieniewski, M.; Pietruszczak, A. A modal extension of Jaskowski’s ´ discussive logic D . Log. J. IGPL 2019, 27, 451–477, doi:10.1093/jigpal/jzz014. 2. Błaszczuk, J. J.; Dziobiak, W. An axiomatization of M -counterparts for some modal logics. Reports Math. Log. 1976, 6, 3–6. 3. Furmanowski, T. Remarks on discussive propositional calculus. Studia Log. 1975, 34, 39–43, doi:10.1007/ BF02314422. 4. Błaszczuk, J. J.; Dziobiak, W. Remarks on Perzanowski’s modal system. Bull. Sect. Log. 1975, 4, 57–64. 5. Perzanowski, J. On M-fragments and L-fragments of normal modal propositional logics. Reports Math. Log. 1975, 5, 63–72. 6. Nasieniewski, M.; Pietruszczak, A. A method of generating modal logics defining Jasko ´ wski’s discussive logic D2. Studia Logica 2011, 97, 161–182, doi:10.1007/s11225-010-9302-2. 7. Nasieniewski, M.; Pietruszczak, A. On the weakest modal logics defining Jaskowski’s ´ logic D2 and the D2-consequence. Bull. Sect. Log. 2012, 41, 215–232. Axioms 2019, 8, 108 17 of 17 8. Nasieniewski, M.; Pietruszczak, A. A method of generating modal logics defining Jasko ´ wski’s discussive D2-consequence. In Logic, Reasoning & Rationality, Weber, E., Wouters, D., Meheus, J., Eds.; Springer: Dordrecht, the Netherlands, 2014; Logic, Argumentation & Reasoning; Volume 5, pp. 95–123, doi:10.1007/ 978-94-017-9011-6_6. 9. Urchs, M. On the role of adjunction in para(in)consistent logic. In Paraconsistency: The Logical Way to the Inconsistent, Proceedings of the Second World Congress on Paraconsistency, São Paulo, Brazil, May 12–19, 2000; Carnielli, W. A., Coniglio, M. E., Loffredo D’Ottaviano, I. M., Eds.; Marcel Dekker: New York, NY, USA, 2002; pp. 487–499. 10. Jaskowski, ´ S. Rachunek zdan ´ dla systemów dedukcyjnych sprzecznych. Studia Societatis Scientiarum Torunensis 1948, Sect. A, vol. I (5), 57–77. In English: Propositional calculus for contradictory deductive systems. Studia Logica 1969, 24, 143–157. doi:10.1007/BF02134311. A propositional Calculus for inconsistent deductive systems. Logic and Logical Philosophy 1999, 7, 35–56, doi: 10.12775/LLP.1999.003 11. Jaskowski, ´ S. O koniunkcji dyskusyjnej w rachunku zdan ´ dla systemów dedukcyjnych sprzecznych. Studia Societatis Scientiarum Torunensis 1949, Sect. A, 1, 171–172. In English: On the discussive conjunction in the propositional calculus for inconsistent deductive systems. Log. Log. Philos. 1999, 7, 57–59, doi:10.12775/LLP. 1999.004. 12. Bull, R. A.; Segerberg, K. Basic Modal Logic. In Handbook of Philosophical Logic; Gabbay, D. M., Guenthner, F., Eds.; D. Reidel Publishing Company: Dordrecht, Holland, 1984; Volume 3, pp. 1–88, doi:10. 1007/978-94-009-6259-0_1 13. Segerberg, K. An Essay in Classical Modal Logic; Uppsala Universitet: Uppsala, Sweded, 1971; Volume I and II. 14. Kotas, J. The axiomatization of S. Jaskowski’s ´ discussive system. Studia Logica 1974, 33, 195–200, doi:10.1007/ BF02120494. 15. da Costa, N.C.A.; Dubikajtis, L. On Jaskowski ´ discussive logic. In Non-Classical Logics, Model Theory and Computability; Arruda, A. I., da Costa, N. C. A., Chuaqui, R., Eds.; North-Holland: New York, NY, USA, 1977; pp. 37–56. 16. Ciuciura, J. A new real axiomatization of the discursive logic D2. In Handbook of Paraconsistency; Beziau, J. Y., Carnielli, W., Gabbay, D. M., Eds.; College Publications: London, UK, 2007; pp. 427–437. 17. Omori, H.; Alama, J. Axiomatizing Jaskowski’s ´ Discussive Logic D . Studia Logica 2018, 106, 1163–1180, doi:10.1007/s11225-017-9780-6. 2019 by the authors. Licensee MDPI, Basel, Switzerland. This article is an open access article distributed under the terms and conditions of the Creative Commons Attribution (CC BY) license (http://creativecommons.org/licenses/by/4.0/).

Journal

Axioms – Multidisciplinary Digital Publishing Institute

Published: Oct 1, 2019

There are no references for this article.