Ryuta Arisaka

Gradual Classical Logic for Attributed Objects

There is knowledge. There is belief. And there is tacit agreement.' 'We may talk about objects. We may talk about attributes of the objects. Or we may talk both about objects and their attributes.' This work inspects tacit agreements on assumptions about the relation between objects and their attributes, and studies a way of expressing them, presenting as the result what we term gradual logic in which the sense of truth gradually shifts. It extends classical logic instances with a new logical connective capturing the object-attribute relation. A formal semantics is presented. Decidability is proved. Paraconsistent/epistemic/conditional/intensional/description/combined logics are compared.

I. INTRODUCTION

A short description There is a book. It is on desk. It is titled 'Meditations and Other Metaphysical Writings'. It, or the document from which the English translation was borne, is written by René Descartes. Period I1 have just described a book, not some freely arbitrary book but one with a few pieces of information: that it is on desk, that it has the said title, and that it is authored by Descartes. Let us suppose that I am with a friend of mine. If I simply said There is a book irrespective of being fully conscious that the book that I have spotted is the described book and none others, the friend of mine, who is here supposed oblivious of any articles on the desk, would have no reason to go against imagining whatever that is considered a book, say 'Les Misérables'. The short statement by itself does not forestall such a possibility. By contrast, if, as in the description provided at the beginning, I ask him to think of a laid-on-desk René Descartes book titled 'Meditations and Other Metaphysical Writings', then there would be certain logical dissonance if he should still think of 'Les Misérables' as a possible option that conforms to the given description. In innumerable occasions like this example, adjectives (or adverbs or whatever terms that fulfil the same purpose) are utilised to disambiguate terms that may denote more than what we intend to communicate.

This feature of natural languages, allowing formulation of a precise enough concept through coordination of (1) broad concepts and (2) attributes that narrow down their possibilities, is a very economical and suitable one for us. For imagine otherwise that every word exactly identifies a unique and indivisible object around us, then we would have no abstract concepts such as generalisation or composition since generalisation must assume specificity and composition decomposability of what result from the process, neither of which accords with the proposed code of the alternative language. While it is certain that concepts expressible in the alternative language sustain no degree of ambiguity in what they refer to, and in this sense it may be said to have an advantage to our languages, the absence of abstract concepts that we so often rely upon for reasoning is rather grave a backlash that would stem its prospect for wide circulation, because -after all -who is capable of showing knowledge of an object that (s)he has never seen before; then who could confidently assert that his/her listener could understand any part of his/her speech on a matter that only he/she knows of if all of us were to adopt the alternative language? By contrast, concepts in our languages, being an identifier of a group rather than an individual, allow generation of a vast domain of discourse with a relatively small number of them in aggregation, e.g. 'book' and 'title' cover anything that can be understood as a book and/or a title, and they at the same time enable refinement, e.g. 'title'd 'book' denotes only those books that are titled. The availability of mutually influencing generic concepts adds to so much flexibility in our languages.

In this document, we will be interested in primitively representing the particular relation between objects/concepts (no special distinction between the two hereafter) and what may form their attributes, which will lead to development of a new logic. Our domain of discourse will range over certain set of (attributed) objects (which may themselves be an attribute to other (attributed) objects) and pure attributes that presuppose existence of some (attributed) object as their host. Needless to say, when we talk about or even just imagine an object with some explicated attribute, the attribute must be found among all that can become an attribute to it. To this extent it is confined within the presumed existence of the object. The new logic intends to address certain phenomena around attributed objects which I think are reasonably common to us but which may not be reasonably expressible in classical logic. Let us turn to an example for illustration of the peculiar behaviour that attributed objects often present to us.

A. On peculiarity of attributed objects as observed in negation, and on the truth 'of' classical logic

Episode Imagine that there is a tiny hat shop in our town, having the following in stock:

1) 3 types of hats: orange hats, green hats ornamented with some brooch, and blue hats decorated with some white hat-shaped accessory, of which only the green and the blue hats are displayed in the shop. 2) 2 types of shirts: yellow and blue, of which only the blue shirts are displayed in the shop.

Imagine also that a young man has come to the hat shop. After a while he asks the shop owner, a lady of many a year of experience in hat-making; "Have you got a yellow hat?" Well, obviously there are no yellow hats to be found in her shop. She answers; "No, I do not have it in stock," negating the possibility that there is one in stock at her shop at the present point of time. Period But "what is she actually denying about?" is the inquiry that I consider pertinent to this writing. We ponder; in delivering the answer, the question posed may have allowed her to infer that the young man was looking for a hat, a yellow hat in particular. Then the answer may be followed by she saying; ". . . but I do have hats with different colours including ones not currently displayed." That is, while she denies the presence of a yellow hat, she still presumes the availability of hats of which she reckons he would like to learn. It does not appear so unrealistic, in fact, to suppose such a thought of hers that he may be ready to compromise his preference for a yellow hat with some non-yellow one, possibly an orange one in stock, given its comparative closeness in hue to yellow.

Now, what if the young man turned out to be a townfamous collector of yellow articles? Then it may be that from his question she had divined instead that he was looking for something yellow, a yellow hat in particular, in which case her answer could have been a contracted form of "No, I do not have it in stock, but I do have a yellow shirt nonetheless (as you are looking after, I suppose?)"

Either way, these somewhat-appearing-to-be partial negations contrast with classical negation with which her answer can be interpreted only as that she does not have a yellow hat, nothing less, nothing more, with no restriction in the range of possibilities outside it.

An analysis that I attempt regarding this sort of usual everyday phenomenon around concepts and their attributes, which leads for example to a case where negation of some concept with attributes does not perforce entail negation of the concept itself but only that of the attributes, is that presupposition of a concept often becomes too strong in our mind to be invalidated. Let us proceed in allusion to logical/computer science terminologies. In classical reasoning that we are familiar with, 1 -truth -is what we should consider is our truth and 0 -falsehood -is what we again should consider is our nontruth. When we suppose a set of true atomic propositions p, q, r, • • • under some possible interpretation of them, the truth embodied in them does -by definition -neither transcend the truth that the 1 signifies nor go below it. The innumerable true propositions miraculously sit on the given definition of what is true, 1. By applying alternative interpretations, we may have a different set of innumerable true propositions possibly differing from the p, q, r, • • • . However, no interpretations are meant to modify the perceived significance of the truth which remains immune to them. Here what renders the truth so immutable is the assumption of classical logic that no propositions that cannot be given a truth value by means of the laws of classical logic may appear as a proposition: there is nothing that is 30 % true, and also nothing that is true by the probability of 30 % unless, of course, the probability of 30 % should mean to ascribe to our own confidence level, which I here assume is not part of the logic, of the proposition being true.

However, one curious fact is that the observation made so far can by no means preclude a deduction that, therefore and no matter how controversial it may appear, the meaning of the truth, so long as it can be observed only through the interpretations that force the value of propositions to go coincident with it and only through examination on the nature2 of those propositions that were made true by them, must be invariably dependant on the delimiter of our domain of discourse, the set of propositions; on the presupposition of which are sensibly meaningful the interpretations; on the presupposition of which, in turn, is possible classical logic. Hence, quite despite the actuality that for any set of propositions as can form a domain of discourse for classical logic it is sufficient that there be only one truth, it is not a priori possible that we find by certainty any relation to hold between such individual truths and the universal truth, if any, whom we cannot hope to successfully invalidate. Nor is it a priori possible to sensibly impose a restriction on any domain of discourse for classical reasoning to one that is consistent with the universal truth, provided again that such should exist. But, then, it is not by the force of necessity that, having a pair of domains of discourse, we find one individual truth and the other wholly interchangeable. In tenor, suppose that truths are akin to existences, then just as there are many existences, so are many truths, every one of which can be subjected to classical reasoning, but no distinct pairs of which a priori exhibit a trans-territorial compatibility. But the lack of compatibility also gives rise to a possibility of dependency among them within a meta-classical-reasoning that recognises the many individual truths at once. In situations where some concepts in a domain of discourse over which reigns a sense of truth become too strong an assumption to be feasibly falsified, the existence of the concepts becomes nonfalsifiable during the discourse of existences of their attributes (which form another domain of discourse); it becomes a delimiter of classical reasoning, that is, it becomes a 'truth' for them.

B. Gradual classical logic: a logic for attributed objects

It goes hopefully without saying that what I wished to impart through the above fictitious episode was not so much about which negation should take a precedence over the others as about the distinction of objects and what may form their attributes, i.e. about the inclusion relation to hold between the two and about how it could restrict domains of discourse. If we are to assume attributed objects as primitive entities in a logic, we for example do not just have the negation that negates the presence of an attributed object (attributed-object negation); on the other hand, the logic should be able to express the negation that applies to an attribute only (attribute negation) and, complementary, we may also consider the negation that applies to an object only (object negation). We should also consider what it may mean to conjunctively/disjunctively have several attributed objects and should attempt a construction of the logic according to the analysis. I call the logic derived from all these analysis gradual classical logic in which the 'truth', a very fundamental property of classical logic, gradually shifts by domains of discourse moving deeper into attributes of (attributed) objects. For a special emphasis, here the gradation in truth occurs only in the sense that is spelled out in the previous sub-section. One in particular should not confuse this logic with multi-valued logics [START_REF] Gottwald | Many-valued Logic[END_REF], [START_REF] Hájek | Fuzzy Logic[END_REF] that have multiple truth values in the same domain of discourse, for any (attributed) object in gradual classical logic assumes only one out of the two usual possibilities: either it is true (that is, because we shall essentially consider conceptual existences, it is synonymous to saying that it exists) or it is false (it does not exist). In this sense it is indeed classical logic. But in some sense -because we can observe transitions in the sense of the 'truth' within the logic itself -it has a bearing of meta-classical logic. As for inconsistency, if there is an inconsistent argument within a discourse on attributed objects, wherever it may be that it is occurring, the reasoning part of which is inconsistent cannot be said to be consistent. For this reason it remains in gradual classical logic just as strong as is in standard classical logic.

C. Structure of this work

Shown below is the organisation of this work.

• Development of gradual classical logic (Sections I and II).

• A formal semantics of gradual classical logic and a proof that it is not para-consistent/inconsistent (Section III).

• Decidability of gradual classical logic (Section IV).

• Conclusion and discussion on related thoughts: paraconsistent logics, epistemic/conditional logics, intensional/description logics, and combined logic (Section V).

II. GRADUAL CLASSICAL LOGIC: LOGICAL PARTICULARS

In this section we shall look into logical particulars of gradual classical logic. Some familiarity with propositional classical logic, in particular with how the logical connectives behave, is presumed. Mathematical transcriptions of gradual classical logic are found in the next section.

A. Logical connective for object/attribute and interactions with negation (⋗ and ¬)

It was already mentioned that the inclusion relation that is implicit when we talk about an attributed object shall be primitive in the proposed gradual classical logic. We shall dedicate the symbol ⋗ to represent it. The usage of the new connective is fixed to take either of the forms Object 1 ⋗ Object 2 or Object 1 ⋗ Attribute2. Both denote an attributed object. In the first case, Object 1 is a more generic object than Object 1 ⋗Object 2 (Object 2 acting as an attribute to Object 1 makes Object 1 more specific). In the second case, we have a pure attribute which is not itself an object. Either way a schematic reading is as follows: "It is true that Object 1 is, and it is true that Object 1 has an attribute of Object 2 (, or of Attribute2)." Given an attributed object Object 1 ⋗ Ojbect 2 (or Object 1 ⋗ Attribute2), ¬(Object 1 ⋗ Object 2 ) expresses its attributed object negation, ¬Object 1 ⋗ Object 2 its object negation and Object 1 ⋗ ¬Object 2 its attribute negation. Again schematic readings for them are, respectively;

• It is false that the attributed object Object 1 ⋗ Object 2 is (Cf. above for the reading of 'an attribute object is').

• It is false that Object 1 is, but it is true that some non-

B. Object/attribute relation and conjunction (⋗ and ∧)

We examine specific examples first involving ⋗ and ∧ (conjunction), and then observe what the readings imply.

1) Hat ⋗ Green ∧ Brooch: It is true that hat is, and it is true that it is green and brooched. 2) (Hat ⋗ Green) ∧ (Hat ⋗ Brooch): for one, it is true that hat is, and it is true that it is green; for one, it is true that hat is, and it is true that it is brooched. 3) (Hat ∧ Shirt) ⋗ Yellow: It is true that hat and shirt are, and it is true that they are yellow. 4) (Hat ⋗ Yellow) ∧ (Shirt ⋗ Yellow): for one, it is true that hat is, and it is true that it is yellow; for one, it is true that shirt is, and it is true that it is yellow. By now it has hopefully become clear that by existential facts as truths I do not mean how many of a given (attributed) object exist: in gradual classical logic, cardinality of objects, which is an important pillar in the philosophy of linear logic [START_REF] Girard | Linear logic[END_REF] and that of its kinds of so-called resource logics, is not what it must be responsible for, but only the facts themselves of whether any of them exist in a given domain of discourse, which is in line with classical logic. 5 Hence they univocally assume a singular than plural form, as in the examples inscribed so far. That the first and the second, and the third and the fourth, equate is then a trite observation. Nevertheless, it is still important that we analyse them with a sufficient precision. In the third and the fourth where the same attribute is shared among several objects, the attribute of being yellow ascribes to all of them. Therefore those expressions are a true statement only if [START_REF] Arlo-Costa | The Logic of Conditionals[END_REF] there is an existential fact that both hat and shirt are and (2) being yellow is true for the existential fact (formed by existence of hat and that of shirt). Another example is found in Figure 1.

Brooch Shirt Hat Large Yellow Hat (Object) (Attribute) ( ⋗ ) Fig. 1: Illustration of an expression ((Brooch ∧ Shirt) ⋗ Large) ∧ ((Brooch ∧ Shirt ∧ Hat) ⋗ Yellow) ∧ (Hat ⋗ Hat):
the existential fact of the attribute large depends on the existential facts of brooch and shirt; the existential fact of the attribute of being yellow depends on the existential facts of brooch, shirt and hat; and the existential fact of the attribute hat depends on the existential fact of hat to which it is an attribute.

C. Object/attribute relation and disjunction (⋗ and ∨)

We look at examples first. 1) Hat ⋗ (Hat ∨ Brooch): It is true that hat is, and it is true that it is either hatted or brooched. 2) (Hat ⋗ Hat) ∨ (Hat ⋗ Brooch): At least either that it is true that hat is and it is true that it is hatted, or that it is true that hat is and it is true that it is brooched. 3) (Hat ∨ Shirt) ⋗ Yellow: It is true that at least either hat or shirt is, and it is true that whichever is existing (or both) is (or are) yellow. 4) (Hat ⋗ Yellow) ∨ (Shirt ⋗ Yellow): At least either it is true that hat is and it is true that it is yellow, or it is true that shirt is and it is true that it is yellow. Just as in the previous sub-section, here again 1) and 2), and 3) and 4) are equivalent. However, in the cases of 3) and 4) here, we have that the existential fact of the attribute yellow depends on that of hat or shirt, whichever is existing, or that of both if they both exist. 6

D. Nestings of object/attribute relations

An expression of the kind (Object 1 ⋗ Object 2 ) ⋗ Object 3 is ambiguous. But we begin by listing examples and then move onto analysis of the readings of the nesting of the relations.

1) (Hat ⋗ Brooch) ⋗ Green: It is true that hat is, and it is true that it is brooched. It is true that the object thus described is green.

2) Hat ⋗ (Hat ⋗ White): It is true that hat is, and it is true that it has the attribute of which it is true that hat is and that it is white. (More simply, it is true that hat is, and it is true that it is white-hatted.) 3) ¬(Hat ⋗ Yellow) ⋗ Brooch: Either it is false that hat is, or else it is true that hat is but it is false that it is yellow. 7 If it is false that hat is, then it is true that brooched object (which obviously cannot be hat) is. If it is true that hat is but it is false that it is yellow, then it is true that the object thus described is brooched. Note that to say that Hat ⋗ Brooch (brooched hat) is being green, we must mean to say that the object to the attribute of being green, i.e. hat, is green. It is on the other hand unclear if green brooched hat should or should not mean that the brooch, an accessory to hat, is also green. But common sense about adjectives dictates that such be simply indeterminate. It is reasonable for (Hat ⋗ Brooch) ⋗ Green, while if we have (Hat ⋗ Large) ⋗ Green, ordinarily speaking it cannot be the case that the attribute of being large is green. Therefore we enforce that (Object 1 ⋗ Object 2 ) ⋗ Object 3 amounts to

(Object 1 ⋗ Object 3 ) ∧ ((Object 1 ⋗ Object 2 ) ∨ (Object 1 ⋗ (Object 2 ⋗ Object 3 )
)) in which disjunction as usual captures the indeterminacy. 2) poses no ambiguity. 3) is understood in the same way as 1).

E. Two nullary logical connectives ⊤ and ⊥

Now we examine the nullary logical connectives ⊤ and ⊥ which denote, in classical logic, the concept of the truth and that of the inconsistency. In gradual classical logic ⊤ denotes the concept of the presence and ⊥ denotes that of the absence. Several examples for the readings are;

1) ⊤ ⋗ Yellow: It is true that yellow object is.

2) Hat ⋗ (⊤ ⋗ Yellow): It is true that hat is, and it is true that it has the following attribute of which it is true that it is yellow object. 3) ⊥ ⋗ Yellow: It is true that nothingness is, and it is true that it is yellow. 4) Hat ⋗ ⊤: It is true that hat is. 5) Hat ⋗ ⊥: It is true that hat is, and it is true that it has no attributes. 6) ⊥ ⋗ ⊥: It is true that nothingness is, and it is true that it has no attributes. 1) and 2) illustrate how the sense of the 'truth' is constrained by the object to which it acts as an attribute. For the rest, however, there is a point around the absence which is not so vacuous as not to merit a consideration, and to which I in fact append the following postulate.

Postulate 1: That which cannot have any attribute is not. Conversely, anything that remains once all the attributes have been removed from a given object is nothingness for which any scenario where it comes with an attribute is inconceivable. With it, 3) which asserts the existence of nothingness is contradictory. 4) then behaves as expected in that Hat which is asserted with the presence of attribute(s) is just as generic a term as Hat itself is. 5) which asserts the existence of an object with no attributes again contradicts Postulate 1. 6) illustrates that any attributed object in some part of which has turned out to be contradictory remains contradictory no matter how it is to be extended: a ⊥ cannot negate another ⊥.

But how plausible is the postulate itself? Let us imagine hat. If the word evoked in our mind any specific hat with specific colour and shape, we first remove the colour out of it. If the process should make it transparent, we then remove the transparentness away from it. And if there should be still some things that are by some means perceivable as have originated from it, then because they are an attribute of the hat, we again remove any one of them. If the humanly no longer detectable something is not nothingness is not itself contradictory, then there must be still some quality originating in the hat that makes the something differ from nothingness. But the quality must again be an attribute to the hat, which we decisively remove away. Therefore, at least intuition solidifies the validity of Postulate 1. A further pursuit on this topic may be useful. For now, however, we shall draw a direct support from -among others -Transcendental Aesthetic in Critique of Pure Reason (English translation [START_REF] Kant | Critique of Pure Reason[END_REF]), and close the scene.

F. Sub-Conclusion

Gradual classical logic was developed in Section I and Section II. The next two sections Section III and Section IV study its mathematical aspects.

III. MATHEMATICAL MAPPINGS: SYNTAX AND SEMANTICS

In this section a semantics of gradual classical logic is formalised. We assume in the rest of this document;

• N denotes the set of natural numbers including 0.

• ∧ † and ∨ † are two binary operators on Boolean arithmetic.

The following laws hold;

1 ∨ † 1 = 1 ∨ † 0 = 0 ∨ † 1 = 1, 0 ∧ † 0 = 0 ∧ † 1 = 1 ∧ † 0 = 0, and 1 ∧ † 1 = 1.
• ∧ † , ∨ † → † , ¬ † , ∃ and ∀ are meta-logical connectives: conjunction, disjunction,8 material implication, negation, existential quantification and universal quantification, whose semantics follow those of standard classical logic. We abbreviate

(A → † B) ∧ † (B → † A) by A ↔ † B.
• Binding strength of logical or meta-logical connectives is, in the order of decreasing precedence;

[¬] ≫ [∧ ∨] ≫ [⋗] ≫ [∀ ∃] ≫ [¬ † ] ≫ [∧ † ∨ † ] ≫ [→ † ] ≫ [↔ † ].
• For any binary connectives ?, for any i, j ∈ N and for !0, !1, • • • , !j that are some recognisable entities, ? j i=0 !i is an abbreviation of (!0)?(!1)? • • •?(!j ).

• For the unary connective ¬, ¬¬! for some recognisable entity ! is an abbreviation of ¬(¬!). Further, ¬ k ! for some k ∈ N and some recognisable entity ! is an abbreviation

of ¬ • • • ¬ k !.

A. Development of semantics

The set of literals in gradual classical logic is denoted by A whose elements are referred to by a with or without a subscript. This set has a countably many number of literals. Given a literal a ∈ A, its complement is denoted by a c which is in A. As usual, we have ∀a ∈ A.(a c ) c = a. The set A ∪ {⊤} ∪ {⊥} where ⊤ and ⊥ are the two nullary logical connectives is denoted by S. Its elements are referred to by s with or without a sub-script. Given s ∈ S, its complement is denoted by s c which is in S. Here we have ⊤ c = ⊥ and ⊥ c = ⊤. The set of formulas is denoted by F whose elements, F with or without a sub-/super-script, are finitely constructed from the following grammar;

F := s | F ∧ F | F ∨ F | ¬F | F ⋗ F
We now develop semantics. This is done in two parts: we do not outright jump to the definition of valuation (which we could, but which we simply do not choose in anticipation for later proofs). Instead, just as we only need consider negation normal form in classical logic because every classical logic formula definable has a reduction into a normal form, so shall we first define rules for formula reductions (for any

F1, F2, F3 ∈ F): • ∀s ∈ S.¬s → s c (¬ reduction 1). • ¬(F1 ∧ F2) → ¬F1 ∨ ¬F2 (¬ reduction 2). • ¬(F1 ∨ F2) → ¬F1 ∧ ¬F2 (¬ reduction 3). • ¬(s ⋗ F2) → s c ∨ (s ⋗ ¬F2) (¬ reduction 4). • (F1 ⋗ F2) ⋗ F3 → (F1 ⋗ F3) ∧ ((F1 ⋗ F2) ∨ (F1 ⋗ F2 ⋗ F3)) (⋗ reduction 1). • (F1 ∧ F2) ⋗ F3 → (F1 ⋗ F3) ∧ (F2 ⋗ F3) (⋗ reduction 2). • (F1 ∨ F2) ⋗ F3 → (F1 ⋗ F3) ∨ (F2 ⋗ F3) (⋗ reduction 3). • F1 ⋗ (F2 ∧ F3) → (F1 ⋗ F2) ∧ (F1 ⋗ F3) (⋗ reduction 4). • F1 ⋗ (F2 ∨ F3) → (F1 ⋗ F2) ∨ (F1 ⋗ F3) (⋗ reduction 5).
Definition 1 (Valuation frame): Let S * denote the set union of (A) the set of finite sequences of elements of S 9 and (B) a singleton set {ǫ} denoting an empty sequence. We define a valuation frame as a 2-tuple: (I, J), where I :

S * × S → {0, 1}
is what we call local interpretation and J : S * \{ǫ} → {0, 1} is what we call gloal interpretation. The following are defined to satisfy.

Regarding local interpretation

• [I(s0. . . . .s k-1 , ⊤) = 1] 10 (I valuation of ⊤). • [I(s0. . . . .s k-1 , ⊥) = 0] (That of ⊥). • [I(s0. . . . .s k-1 , a k ) = 0] ∨ † [I(s0. . . . .s k-1 , a k ) = 1]
(That of a literal).

• [I(s0. . . . .s k-1 , a k ) = 0] ↔ † [I(s0. . . . .s k-1 , a c k ) = 1]
(That of a complement). 9 Simply for a presentation purpose, we use comma such as s * 1 .s 10 When k = 0, we assume that [I(s0. . . . .s k-1 , s k ) = I(ǫ, s0)]. Same applies in the rest.

• [I(s0. . . . .s k-1 , s k ) = I(s ′ 0 . . . . .s ′ k-1 , s k )]
(Synchronization condition on I interpretation; this reflects the dependency of the existential fact of an attribute to the existential fact of objects to which it is an attribute). Regarding global interpretation

• [J(s0. . . . .s k ) = 1] ↔ † ∀i ∈ N. †k i=0 [I(s0. . . . .si-1, si) = 1]
(Noncontradictory J valuation).

• [J(s0. . . . .s k ) = 0] ↔ † ∃i ∈ N.[i ≤ k] ∧ † [I(s0. . . . .si-1, si) = 0] (Contradictory J valua- tion).
Note that global interpretation is completely characterised by local interpretations, as clear from the definition.

Definition 2 (Valuation): Suppose a valuation frame M = (I, J). The following are defined to hold for all F1, F2 ∈ F and for all k ∈ N:

• [M |= s0 ⋗ s1 ⋗ • • • ⋗ s k ] = J(s0.s1. . . . .s k ). • [M |= F1 ∧ F2] = [M |= F1] ∧ † [M |= F2]. • [M |= F1 ∨ F2] = [M |= F1] ∨ † [M |= F2].
The notions of validity and satisfiability are as usual.

Definition 3 (Validity/Satisfiability):

A formula F ∈ F is said to be satisfiable in a valuation frame M iff 1 = [M |= F ];
it is said to be valid iff it is satisfiable for all the valuation frames; it is said to be invalid iff 0 = [M |= F ] for some valuation frame M; it is said to be unsatisfiable iff it is invalid for all the valuation frames.

B. Study on the semantics

We have not yet formally verified some important points. Are there, firstly, any formulas F ∈ F that do not reduce into some value-assignable formula? Secondly, what if both If the first should hold, the semantics -the reductions and valuations as were presented in the previous sub-sectionwould not assign a value (values) to every member of F even with the reduction rules made available. If the second should hold, we could gain 1 = [M |= F ∧ ¬F ], which would relegate this gradual logic to a family of para-consistent logics [START_REF] João | Logics of Formal Inconsistency[END_REF] quite out of keeping with my intention. And the third should never hold, clearly.

Hence it must be shown that these unfavoured situations do not arise. An outline to the completion of the proofs is; 1) to establish that every formula has a reduction through ¬ reductions and ⋗ reductions into some formula F for which it holds that ∀M.[M |= F ] ∈ {0, 1}, to settle down the first inquiry. 2) to prove that any formula F to which a value 0/1 is assignable without the use of the reduction rules satisfies for every valuation frame (a) that

[M |= F ] ∨ † [M |= ¬F ] = 1 and [M |= F ] ∧ † [M |= ¬F ] = 0; and (b) either that 0 = 1 = [M |= F ] or that 1 = 0 = [M |= F ],
to settle down the other inquiries partially. 3) to prove that the reduction through ¬ reductions and ⋗ reductions on any formula F ∈ F is normal in that, in whatever order those reduction rules are applied to F , any Freduced in the set of possible formulas it reduces into satisfies for every valuation frame either that [M |= Freduced] = 1, or that [M |= Freduced ] = 0, for all such Freduced, to conclude. 1) Every formula is 0/1-assignable: We state several definitions for the first objective of ours.

Definition 4 (Chains/Unit chains): A chain is defined to be any formula

F ∈ F such that F = F0 ⋗ F1 ⋗ • • • ⋗ F k+1 for k ∈ N.
A unit chain is defined to be a chain for which Fi ∈ S for all 0 ≤ i ≤ k + 1. We denote the set of unit chains by U. By the head of a chain F ∈ F, we mean some formula Fa ∈ F satisfying (1) that Fa is not in the form F b ⋗ Fc for some F b , Fc ∈ F and (2) that F = Fa ⋗ F d for some F d ∈ F. By the tail of a chain F ∈ F, we then mean some formula F d ∈ F such that F = Fa ⋗ F d for some Fa as the head of F .

Definition 5 (Unit chain expansion): Given any F ∈ F, we say that F is expanded in unit chains only if any chain that occurs in F is a unit chain.

Definition 6 (Formula size): The size of a formula is defined inductively. Let F be some arbitrary formula, and let f size(F ) be the formula size of F . Then it holds that;

• f size(F ) = 1 if F ∈ S. • f size(F ) = f size(F1) + f size(F2) + 1 if F = F1 ∧ F2, F = F1 ∨ F2, or F = F1 ⋗ F2. • f size(F ) = f size(F1) + 1 if F = ¬F1.
Definition 7 (Maximal number of ¬ nestings): Given a formula F ∈ F, we denote by neg max(F ) a maximal number of ¬ nestings in F , whose definition goes as follows;

• If F0 = s, then neg max(F0) = 0. • If F0 = F1 ∧ F2 or F0 = F1 ∨ F2 or F0 = F1 ⋗ F2, then
neg max(F0) = max(neg max(F1), neg max(F2)).

• If F0 = ¬F1, then neg max(F0) = 1 + neg max(F1).

We now work on the main results.

Lemma 1 (Linking principle): Let F1 and F2 be two formulas in unit chain expansion. Then it holds that F1 ⋗ F2 has a reduction into a formula in unit chain expansion.

Proof: In Appendix A. Lemma 2 (Reduction without negation): Any formula F0 ∈ F in which no ¬ occurs reduces into some formula in unit chain expansion.

Proof: By induction on formula size. For inductive cases, consider what F0 actually is:

1) F0 = F1∧F2 or F0 = F1∨F2: Apply induction hypothesis on F1 and F2. Hence we obtain the desired result for the first objective.

Proposition 1: To any F ∈ F corresponds at least one formula Fa in unit chain expansion into which F reduces. It holds for any such Fa that [M |= Fa] ∈ {0, 1} for any valuation frame.

For the next sub-section, the following observation about negation on a unit chain comes in handy. Let us state a procedure.

Definition 8 (Procedure recursiveReduce): The procedure given below takes as an input a formula F in unit chain expansion. Description of recursiveReduce(F ) 1) Replace ∧ in F with ∨, and ∨ with ∧. These two operations are simultaneous. 2) Replace all the non-chains s ∈ S in F simultaneously with s c (∈ S). 3) For every chain Fa in F with its head s ∈ S for some s and its tail Ftail, replace Fa with (s c ∨ (s ⋗ (recursiveReduce(Ftail)))).

4) Reduce F via ⋗ reductions in unit chain expansion. Then we have the following result.

Proposition 2 (Reduction of negated unit chain expansion): Let F be a formula in unit chain expansion. Then ¬F reduces via the ¬ and ⋗ reductions into recursiveReduce(F ). Moreover recursiveReduce(F ) is the unique reduction of ¬F . Proof: For the uniqueness, observe that only ¬ reductions and ⋗ reduction 5 are used in reduction of ¬F , and that at any point during the reduction, if there occurs a sub-formula in the form ¬Fx, the sub-formula Fx cannot be reduced by any reduction rules. Then the proof of the uniqueness is straightforward.

2) Unit chain expansions form Boolean algebra:

We make use of disjunctive normal form in this sub-section for simplification of proofs.

Definition 9 (Disjunctive/Conjunctive normal form):

A formula F ∈ F is defined to be in disjunctive normal form only if ∃i, j, k ∈ N ∃h0, • • • , hi ∈ N ∃f00, . . . , f kh k ∈ U ∪ S.F = ∨ k i=0 ∧ h i j=0 fij . Dually, a formula F ∈ F is defined to be in conjunctive normal form only if ∃i, j, k ∈ N ∃h0, • • • , hi ∈ N ∃f00, . . . , f kh k ∈ U ∪ S.F = ∧ k i=0 ∨ h i j=0 fij .
Now, for the second objective of ours, we prove that U ∪ S, recursiveReduce, ∨ † and ∧ † form a Boolean algebra (Cf. [START_REF]Boolean algebra[END_REF] for the laws of Boolean algebra), from which follows the required outcome. Proposition 3 (Annihilation/Identity): For any formula F in unit chain expansion and for any valuation frame, it holds (1) that

[M |= ⊤∧F ] = [M |= F ]; (2) that [M |= ⊤∨F ] = [M |= ⊤]; (3) that [M |= ⊥ ∧ F ] = [M |= ⊥]; and (4) that [M |= ⊥ ∨ F ] = [M |= F ].

Lemma 5 (Elementary complementation):

For any s0 ⋗s1 ⋗ • • • ⋗ s k ∈ U ∪ S for some k ∈ N, if for a given valuation frame it holds that [M |= s0 ⋗ s1 ⋗ • • • ⋗ s k ] = 1, then it also holds that [M |= recursiveReduce(s0 ⋗ s1 ⋗ • • • ⋗ s k )] = 0; or if it holds that [M |= s0 ⋗ s1 ⋗ • • • ⋗ s k ] = 0, then it holds that [M |= recursiveReduce(s0 ⋗ s1 ⋗ • • • ⋗ s k )] = 1.
These two events are mutually exclusive.

Proof: In Appendix C. Proposition 4 (Associativity/Commutativity/Distributivity): Given any formulas F1, F2, F3 ∈ F in unit chain expansion and any valuation frame M, the following hold:

1

) [M |= F1] ∧ † ([M |= F2] ∧ † [M |= F3]) = ([M |= F1] ∧ † [M |= F2]) ∧ † [M |= F3] (associativity 1). 2) [M |= F1] ∨ † ([M |= F2] ∨ † [M |= F3]) = ([M |= F1] ∨ † [M |= F2]) ∨ † F3 (associativity 2). 3) [M |= F1] ∧ † [M |= F2] = [M |= F2] ∧ † [M |= F1] (commutativity 1). 4) [M |= F1] ∨ † [M |= F2] = [M |= F2] ∨ † [M |= F1] (commutativity 2). 5) [M |= F1] ∧ † ([M |= F2] ∨ † [M |= F3]) = ([M |= F1] ∧ † [M |= F2]) ∨ † ([M |= F1] ∧ † [M |= F3]) (distributivity 1). 6) [M |= F1] ∨ † ([M |= F2] ∧ † [M |= F3]) = ([M |= F1] ∨ † [M |= F2]) ∧ † ([M |= F1] ∨ † [M |= F3]) (distributivity 2
). Proof: Make use of Lemma 5. Details are in Appendix D.

Proposition 5 (Idempotence and Absorption): Given any formula F1, F2 ∈ F in unit chain expansion, for any valuation frame it holds that

[M |= F1] ∧ † [M |= F1] = [M |= F1] ∨ † [M |= F1] = [M |= F1] (idempotence); and that [M |= F1]∧ † ([M |= F1]∨ † [M |= F2]) = [M |= F1] ∨ † ([M |= F1] ∧ † [M |= F2]) = [M |= F1] (absorption).
Proof: Both F1, F2 are assigned one and only one value v ∈ {0, 1} (Cf. Appendix D). Trivial to verify.

We now prove laws involving recursiveReduce.

Lemma 6 (Elementary double negation): Proof: Make use of disjunctive normal form, Lemma 5 and Lemma 6. Details are in Appendix F.

Let F denote s0 ⋗ s1 ⋗ • • • ⋗ s k ∈ U ∪ S for some k ∈ N.
Theorem 1: Denote by X the set of the expressions comprising all [M |= fx] for fx ∈ U ∪ S. Then for every valuation frame, (X, recursiveReduce, ∧ † , ∨ † ) defines a Boolean algebra.

Proof: Follows from earlier propositions and lemmas.

3) Gradual classical logic is neither para-consistent nor inconsistent :

To achieve the last objective we assume two notations.

Definition 10 (Sub-formula notation): Given a formula F ∈ F, we denote by F [Fa] the fact that Fa occurs as a sub-formula in F . Here the definition of a sub-formula of a formula follows one that is found in standard textbooks on logic [START_REF] Stephen | Introduction to META-MATHEMATICS[END_REF]. F itself is a sub-formula of F .

Definition 11 (Small step reductions): By F1 F2 for some formulas F1 and F2 we denote that F1 reduces in one reduction step into F2. By F1 r F2 we denote that the reduction holds explicitly by a reduction rule r (which is either of the 7 rules). By F1 * F2 we denote that F1 reduces into F2 in a finite number of steps including 0 step in which case F1 is said to be irreducible. By F1 k F2 we denote that the reduction is in exactly k steps. By

F1 * {r 1 ,r 2 ,••• } F2 or F1 k {r 1 ,r 2 ,••• } F2
we denote that the reduction is via those specified rules r1, r2, • • • only.

Along with them, we also enforce that F(F ) denote the set of formulas in unit chain expansion that F ∈ F can reduce into. A stronger result than Lemma 2 follows.

Lemma 7 (Bisimulation without negation): Assumed below are pairs of formulas in which ¬ does not occur. F ′ differs from F only by the shown sub-formulas, i.e. F ′ derives from F by replacing the shown sub-formula for F ′ with the shown sub-formula for F and vice versa. Then for each pair (F, F ′ ) below, it holds for every valuation frame that

[M |= F1] = [M |= F2] for all F1 ∈ F(F ) and for all F2 ∈ F(F ′ ). F [(Fa ∧ F b ) ⋗ Fc] , F ′ [(Fa ⋗ Fc) ∧ (F b ⋗ Fc)] F [(Fa ∨ F b ) ⋗ Fc] , F ′ [(Fa ⋗ Fc) ∨ (F b ⋗ Fc)] F [Fa ⋗ (F b ∧ Fc)] , F ′ [(Fa ⋗ F b ) ∧ (Fa ⋗ Fc)] F [Fa ⋗ (F b ∨ Fc)] , F ′ [(Fa ⋗ F b ) ∨ (Fa ⋗ Fc)] F [(Fa ⋗ F b ) ⋗ Fc] , F ′ [(Fa ⋗ Fc) ∧ ((Fa ⋗ F b ) ∨ (Fa ⋗ F b ⋗ Fc))]
Proof: By induction on the number of reduction steps and a sub-induction on formula size in each direction of bisimulation. Details are in Appendix G.

Lemma 8 (Other bisimulations): For each pair (F ∈ F, F ′ ∈ F) below, it holds for every valuation frame [START_REF] Arlo-Costa | The Logic of Conditionals[END_REF]

that ∀F1 ∈ F(F ).∃F2 ∈ F(F ′ ).[M |= F1] = [M |= F2] and (2) that ∀F2 ∈ F(F ′ ).∃F1 ∈ F(F ).[M |= F1] = [M |= F2].
Once again, F and F ′ differ only by the shown sub-formulas.

F [¬(Fa ∧ F b )] , F ′ [¬Fa ∨ ¬F b ] F [¬(Fa ∨ F b )] , F ′ [¬Fa ∧ ¬F b ] F [s ∨ s] , F ′ [s] F [s ∨ Fa ∨ s] , F ′ [s ∨ Fa] F [s ∧ s] , F ′ [s] F [s ∧ Fa ∧ s] , F ′ [s ∧ Fa] F [s c ] , F ′ [¬s]
Proof: By simultaneous induction on the number of reduction steps and a sub-induction on formula size. Details are in Appendix H.

Lemma 9 (Normalisation without negation): Given a formula F ∈ F, if ¬ does not occur in F , then it holds for every valuation frame either that [M |= Fa] = 1 for all Fa ∈ F(F ) or else that [M |= Fa] = 0 for all Fa ∈ F(F ).

Proof: Consequence of Lemma 7. Theorem 2 (Normalisation): Given a formula F ∈ F, denote the set of formulas in unit chain expansion that it can reduce into by F1. Then it holds for every valuation frame either that [M |= Fa] = 1 for all Fa ∈ F1 or else that [M |= Fa] = 0 for all Fa ∈ F1.

Proof: By induction on maximal number of ¬ nestings and a sub-induction on formula size. We quote Lemma 9 for base cases. Details are in Appendix I.

By the result of Theorem 1 and Theorem 2, we may define implication: F1 ⊃ F2 to be an abbreviation of ¬F1∨F2exactly the same -as in classical logic.

IV. DECIDABILITY

We show a decision procedure for universal validity of some input formula F . Here, z : Z for some z and Z denotes a variable z of type Z. Also assume a terminology of 'object level', which is defined inductively. Given F in unit chain expansion, (A) if s ∈ S in F occurs as a non-chain or as a head of a unit chain, then it is said to be at the 0-th object level. (B) if it occurs in a unit chain as s0 ⋗ EXTRACT(F : F, object level : N) returning F ′ : F L0:

• • • ⋗ s k ⋗ s or as s0 ⋗ • • • ⋗ s k ⋗ s ⋗ ...
F ′ := F . L1: For every s0 ⋗ s1 ⋗ • • • ⋗ s k for some k ∈ N
greater than or equal to object level and some s0, s1, . . . ,

s k ∈ S occurring in F ′ , replace it with s0 ⋗ • • • ⋗ sobject level . L2: return F ′ .
COUNT DISTINCT(F : F) returning n : N L0: return n := (number of distinct members of A in F ). UNSAT(F : F, I : I) returning true or false L0: return true if, for the given interpretation I, [(I, J) |= F ] = 0. Otherwise, return false. REWRITE(F : F, I : I, object level : N) returning F ′ : F L0: F ′ := F . L1: remove all the non-unit-chains and unit chains shorter than or equal to object level from F ′ . The removal is in the following sense: if fx ∧ Fx, Fx ∧ fx, fx ∨ Fx or Fx ∨ fx occurs as a sub-formula in F ′ for fx those just specified, then replace them not simultaneously but one at a time to Fx until no more reductions are possible. L2 0 : For each unit chain f in F ′ , Do: L2 1 : if the head of f is 0 under I, then remove the unit chain from F ′ ; else replace the head of f with ⊤.

L2 2 : End of For Loop. L3: return F ′ . The intuition of the procedure is found within the proof below.

Proposition 7 (Decidability of gradual classical logic): Complexity of (F, 0) is at most EXPTIME.

Proof: We show that it is a decision procedure. That the complexity bound cannot be worse than EXPTIME is clear from the semantics (for L0) and from the procedure itself. Consider L0 of the main procedure. This reduces a given formula into a formula in unit chain expansion. In L1 of the main procedure, we get a snapshot of the input formula. We extract from it components of the 0-th object level, and check if it is (un)satisfiable. The motivation for this operation is as follows: if the input formula is contradictory at the 0th-object level, the input formula is contradictory by the definition of J. Since we are considering validity of a formula, we need to check all the possible valuation frames. The number is determined by distinct A elements. L2 gets the number (n). The For loop starting at L3 0 iterates through the 2 n distinct interpretations. If the snapshot is unsatisfiable for any such valuation frame, it cannot be valid, which in turn implies that the input formula cannot be valid (L3 1 ). If the snapshot is satisfiable and if the maximum object-level in the input formula is the 0th, i.e. the snapshot is the input formula, then the input formula is satisfiable for this particular valuation frame, and so we check the remaining valuation frames (L3 2 ). Otherwise, if it is satisfiable and if the maximum object-level in the input formula is not the 0th, then we need to check that snapshots in all the other object-levels of the input formula are satisfiable by all the valuation frames. We do this check by recursion (L3 3 ). Notice the first parameter REWRITE(Fa, I, object level) here. This returns some formula F ′ . At the beginning of the sub-procedure, F ′ is a duplicated copy of Fa (not F b ). Now, under the particular 0-th object level interpretation I, some unit chain in Fa may be already evaluated to 0. Then we do not need consider them at any deeper object-level. So we remove them from F ′ . Otherwise, in all the remaining unit chains, the 0-th object gets local interpretation of 1. So we replace the S element at the 0-th object level with ⊤ which always gets 1. Finally, all the non-chain S constituents and all the chains shorter than or equal to object level in Fa are irrelevant at a higher object-level. So we also remove them (from F ′ ). We pass this F ′ and an incremented object level to the main procedure for the recursion.

The recursive process continues either until a sub-formula passed to the main procedure turns out to be invalid, in which case the recursive call returns 0 (L2 2 and L4 in the main procedure) to the caller who assigns 0 to o (L2 4 ) and again returns 0, and so on until the first recursive caller. The caller receives 0 once again to conclude that F is invalid, as expected. Otherwise, we have that F is valid, for we considered all the valuation frames. The number of recursive calls cannot be infinite.

V. CONCLUSION AND RELATED THOUGHTS

There are many existing logics to which gradual classical logic can relate, including ones below. "G(g)radual classical logic" is abbreviated by Grad.

A. Para-consistent Logic

In classical logic a contradictory statement implies just anything expressible in the given domain of discourse. Not so in the family of para-consistent logics where it is distinguished from other forms of inconsistency [START_REF] João | Logics of Formal Inconsistency[END_REF]; what is trivially the case in classical logic, say a1 ∧ a c 1 ⊃ a2 for any propositions a1 and a2, is not an axiom. Or, if my understanding about them is sufficient, it actually holds in the sense that to each contradiction expressible in a para-consistent logic associates a sub-domain of discourse within which it entails anything; however, just as Grad internalises classical logic, so do paraconsistent logics, revealing the extent of the explosiveness of contradiction within them. In some sense para-consistent logics model parallel activities as seen in concurrency. What Grad on the other hand aims to model is conceptual scoping. As they do not pose an active conflict to each other, it should be possible to derive an extended logic which benefits from both features.

B. Epistemic Logic/Conditional Logic

Epistemic logic concerns knowledge and belief, augmenting propositional logic with epistemic operators Kc for knowledge and Bc for belief such that Kca/Bca means that a proposition a is known/believed to be true by an agent c. [START_REF] Hendricks | Epistemic Logic[END_REF]. Grad has a strong link to knowledge and belief, being inspired by tacit agreement on assumptions about attributed objects. To seek a correspondence, we may tentatively assign to a0 ⋗ a1 a mapping of a0 ∧ Kc/Bca1. However, this mapping is not very adequate due to the fact that Kc/Bc enforces a global sense of knowledge/belief that does not update in the course of discourse. The relation that ⋗ expresses between a0 and a1 is not captured this way. A more proximate mapping is achieved with the conditional operator > in conditional logics [START_REF] Arlo-Costa | The Logic of Conditionals[END_REF] with which we may map a0 ⋗ a1 into a0 ∧ (a0 > a1). But by this mapping the laws of > will no longer follow any of normal, classical, monotonic or regular (Cf. [START_REF] Chellas | Modal Logic: An Introduction[END_REF] or Section 3 in [START_REF] Arlo-Costa | The Logic of Conditionals[END_REF]; note that the small letters a, b, c, ... in the latter reference are not literals but propositional formulas) conditional logics'. RCEA holds safely, but all the rest: RCEC; RCM; RCR and RCK fail since availability of some b and c equivalent in one sub-domain of discourse of Grad does not imply their equivalence in another sub-domain. Likewise, the axioms listed in Section 3 of [START_REF] Arlo-Costa | The Logic of Conditionals[END_REF] fail save CC (understand it by a ∧ (a > b) ∧ a ∧ (a > c) ⊃ a ∧ (a > b ∧ c)), CMon and CM. Further studies should be useful in order to unravel a logical perspective into how some facts that act as pre-requisites for others could affect knowledge and belief.

C. Intensional Logic/Description Logic

Conditional logics were motivated by counterfactuals [START_REF] Lewis | Counterfactuals[END_REF], [START_REF] Plumpton | General Propositions and Causality[END_REF], e.g. "If X were the case, then Y would be the case." According to the present comprehension of the author's about reasoning about such statements as found in Appendix J in the form of an informal essay, the reasoning process involves transformation of one's consciousness about the antecedent that he/she believes is impossible. However, even if we require the said transformation to be minimal in its rendering the impossible X possible, we still cannot ensure that we obtain a unique representation of X, so long as X is not possible. Hence it is understood to be not what it is unconditionally, but only what it is relative to a minimal transformation that applied. The collection of the possible representations is sometimes described as the extension of X. Of course, one may have certain intention, under which X refers to some particular representations of X. They are termed intension of X for contrast.

The two terms are actively differentiated in Intensional Logic [START_REF] Carnap | Meaning and Necessity[END_REF], [START_REF] Church | A Formulation of the Logic of Sense and Denotation[END_REF], [START_REF] Montague | On the Nature of Certain Philosophical Entities[END_REF]. For example, suppose that we have two concepts denoting collections U and V such that their union is neither U nor V. Then, although U is certainly not equal to V, if, for instance, we regard every concept as a designator of an element of the collection, then U is V if U → u and V → v such that u = v. For a comparison, Grad does not treat intension explicitly, for if some entity equals another in Grad, then they are always extensionally equal: if the morning star is the evening star, it cannot be because the two terms designate the planet Venus that Grad says they are equal, but because they are the same. But it expresses the distinction passively in the sense that we can meta-logically observe it. To wit, consider an expression (⊤ ⋗ Space ⋗ Wide) ∧ (Space ⋗ Wide). Then, depending on what the given domain of discourse is, the sense of Space in ⊤ ⋗ Space ⋗ Wide may not be the same as that of Space in Space ⋗ Wide. Similarly for Wide. (Incidentally, note that ⋗ is not the type/sub-type relation.)

The intensionality in the earlier mentioned conditional logics is, provided counterfactual statements are reasoned in line with the prescription in Appendix J, slightly more explicit: the judgement of Y depends on intension of X. But in many of the ontic conditional logics in [START_REF] Arlo-Costa | The Logic of Conditionals[END_REF], it does not appear to be explicitly distinguished from extension.

It could be the case that Grad, once extended with predicates, may be able to express intensionality in a natural way, e.g. we may say ∃Intension(Adjective ⋗ Sheep) = Ovine (in some, and not necessarily all, sub-domains of discourse). At any rate, how much we should care for the distinction of intensionality and extensionality probably owes much to personal tastes. We may study intensionality as an independent component to be added to extensional logics. We may alternatively study a logic in which extensionality is deeply intertwined with intensionality. It should be the sort of applications we have in mind that favours one to the other.

Of the logics that touch upon concepts, also worth mentioning are a family of description logics [START_REF]The Description Logic Handbook: Theory, implementation, and applications[END_REF] that have influence in knowledge representation. They are a fragment of the firstorder logic specialised in setting up knowledge bases, in reasoning about their contents and in manipulating them [START_REF] Baader | Basic description logics[END_REF]. The domain of discourse, a knowledge base, is formed of two components. One called TBox stores knowledge that does not usually change over time: [START_REF] Arlo-Costa | The Logic of Conditionals[END_REF] concepts (corresponding to unary predicates in the first-order logic) and ( 2) roles (corresponding to binary predicates), specifically. The other one, ABox, stores contingent knowledge of assertions about individuals, e.g. Mary, an individual, is mother, a general concept. Given the domain of discourse, there then are reasoning facilities in description logics responsible for checking satisfiability of an expression as well as for judging whether one description is a sub-/super-concept of another (here a super-concept of a concept is not "a concept of a concept" in the term of [START_REF] Church | A Formulation of the Logic of Sense and Denotation[END_REF]).

Description logics were developed from specific applications, and capture a rigid sense of the concept. It should be of interest to see how Grad may be specialised for applications in computer science. To see if the use of ⋗ as a meta-relation on description logic instances can lead to results that have been conventionally difficult to cope with is another hopeful direction.

D. Combined Logic

Grad is a particular kind of combined logic [START_REF] Caleiro | Fibring of logics as a universal construction[END_REF], [START_REF] Carnielli | Combining logics[END_REF], [START_REF] Gabbay | Fibred semantics and the weaving of logics: Part 1[END_REF] combining the same logic over and over finitely many times. The presence of the extra logical connective ⋗ scarcely diverts it from the philosophy of combined logics. Instead of regarding base logics 11 as effectively bearing the same significance in footing, however, this work recognised certain sub-ordination between base logics, as the new logical connective characterised. Object-attribute negation also bridges across the base logics. Given these, a finite number of the base logic combinations at once made more sense than combinations of two base logics finitely many times, for the latter approach may not be able to adequately represent the meta-base-logic logical connectives with the intended semantics of gradual classical logic. Investigation into this sub-set of combined logics could have merits of its own.

E. Conclusion

This work presented Grad as a logic for attributed objects. Its mechanism should be easily integrated into many non-intuitionistic logics. Directions to future research were also suggested at lengths through comparisons. Considering its variations should be also interesting. For applications of gradual logics, program analysis/verification, databases, and artificial intelligence come into mind.

F ′′′ and F ′

x differ only by the shown sub-formulas, we repeat the rest of simulation on F ′

x and F ′′′ . Induction hypothesis. 5) If a reduction takes place on a sub-formula Fp of F in which the shown sub-formula of F occurs as a strict sub-formula, then similar to the 1) f) sub-case in Lemma 7. The second case is similar. For the third case; 1) If no reduction is applicable, then vacuously

[M |=D F ] = [M |=D F ′ ].
2) If a reduction takes place on a sub-formula which neither is a sub-formula of the shown sub-formula nor has as its sub-formula the shown sub-formula, then we reduce the same sub-formula in F ′ . Induction hypothesis. 3) If a reduction takes place on a sub-formula Fp of F in which the shown sub-formula of F occurs as a strict sub-formula, then; a) If the applied reduction is ¬ reduction 2 or 4, then straightforward. b) If the applied reduction is ¬ reduction 3 such that

(F = Fa[¬(Fx ∨ s ∨ s ∨ Fy)]) (F b [¬Fx ∧ ¬s ∧ ¬s ∧ ¬Fy] = Fc[¬s ∧ ¬s]) F d [s c ∧ s c ]
for some Fx and Fy (the last transformation does not cost generality due to simultaneous induction), then we reduce F ′ as follows:

(F ′ = F ′ a [¬(Fx ∨ s ∨ Fy)]) (F ′ b [¬Fx ∧ ¬s ∧ ¬Fy] = F ′ c [¬s]) F ′ d [s c ].
Induction hypothesis. Any other cases are straightforward. c) If the applied reduction is ⋗ reduction 1-4, then straightforward. Similarly for the remaing ones.

APPENDIX I: PROOF OF THEOREM 2

By induction on maximal number of ¬ nestings and a subinduction on formula size. We quote Lemma 9 for base cases. For inductive cases, assume that the current theorem holds true for all the formulas with neg max(F0) of up to k. Then we conclude by showing that it still holds true for all the formulas with neg max(F0) of k + 1. First we note that there applies no ¬ reductions on ¬Fx if Fx is a chain whose head is not an element of S. But this is straightforward from the descriptions of the reduction rules.

On this observation we show that if we have a sub-formula ¬Fx such that no ¬ occurs in Fx, then Fx can be reduced into a formula in unit chain expansion with no loss of generality, prior to the reduction of the outermost ¬. Then we have the desired result by induction hypothesis and the results in the previous sub-section. But suppose otherwise. Let us denote by F the set of formulas in unit chain expansion that ¬F ′

x reduces into where F ′

x is a unit chain expansion of Fx. Now suppose there exists Fy in unit chain expansion that ¬Fx can reduce into if the outermost ¬ reduction applies before Fx has reduced into a formula in unit chain expansion such as to satisfy that Hence for our supposition to hold, it must satisfy that there exists no bisimulation between F ′ z and ¬Fz. But because it is trivially provable that to each reduction on F ′ z corresponds reduction(s) on ¬Fz (, for we can choose to apply the ¬ reduction on ¬Fz to gain F ′ z ,) it must in fact satisfy that not to each reduction on ¬Fz corresponds reduction(s) on F ′ z . Consider what reduction applies on a sub-formula of ¬Fz:

[M |=D Fy] = [M |=D F β ] for some F β ∈ F.
1) any ¬ reduction: Then the reduction generates F ′ z . A contradiction to supposition has been drawn. 2) ⋗ reduction 1: Consider how Fz looks like: a) Fz = F1[(Fu ⋗ Fv) ⋗ Fw] ∧ F2: But then the same reduction can take place on

F ′ z = ¬F1[(Fu ⋗ Fv) ⋗ Fw] ∨ ¬F2. Contradiction. b) Fz = F1 ∧ F2[(Fu ⋗ Fv) ⋗ Fw]: Similar. c) Fz = F1[(Fu ⋗ Fv) ⋗ Fw] ∨ F2: Similar. d) Fz = F1 ∨ F2[(Fu ⋗ Fv) ⋗

COUNTERFACTUALS

Conditional logics were motivated by counterfactuals. What follows is but a personal viewpoint on the process of reasoning about counterfactuals. Earlier ideas in the line of Stalnaker's and others' [START_REF] Arlo-Costa | The Logic of Conditionals[END_REF] helped sharpen this view. An essential purpose of reasoning about counterfactuals is, to the author at least, in conducting a partial examination on the faculty of our imagination. A 'flying emu' which is considered to be non-existing can be, despite all the contradictions that the term causes against what we find within the knowledge, accommodated in our imagination. There what the knowledge says is the state of being flying and what it says is something that is an emu are refined into combinable forms so that a flying emu comes to existence within the parallel consciousness. But because it does not exist in the knowledge, taken two volunteers who are for simplicity supposed sharing the same knowledge, even if the flying emu in imagination of one of them does not coincide in features with that in the other, they cannot be said to be unjustifiable as a proper representation for the mismatch found between them, since no definition of a flying emu is in any case found in the knowledge. Taken countably many volunteers, it comes of no surprise if the number of representations of a flying emu is also countably many, each one of which is justified as a proper in each respective imagination space. Therefore, for counterfactuals in particular out of other forms that imagination enables us, if we have "If there were a flying emu, then Y would be the case," one plausible way of obtaining the truth value for this expression is as stated in the following pseudocode: Let us mean by refinement of an element in imagination its enlargement by means of any element(s) that are presently found in imagination acting upon it in the manner lawful to D. In this term of refinement, keep refining elements of imagination insofar as such refinement is strictly necessary to generate a flying emu in the imagination. Call the state of the updated imagination Im if it is not inconsistent. Here, by such a refinement being strictly necessary, we mean that (1) the flying emu in Im ceases to exist if the last change that was taken to derive Im is undone, and that (2) any changes made to the elements of (Im\{flying emu})\(knowledge) cannot be any smaller for the particular flying emu to not cease to exist. L4 1 If there is no such Im, that is, if no imagination space in which a flying emu exists derives from the duplicated knowledge following the prescribed alteration process such that it be contained within the boundary of D, then return true. L4 2 For each such Im, do: L4 3 If Y is not the case in Im, then return false. L4 4 End of For loop L5 Return true. A couple of relevant points are: (1) If a counterfactual a > b is true as judged by the above pseudo-code, then it is true by the sense delimited by D. (2) A counterfactual is an impossible case: if it were possible, it would not be a counterfactual. Hence if by a possible world we mean to refer to a world which may just as feasibly exist as our own world, there is no possible world that makes the antecedent of the counterfactual true, for if in some possible alternative world the antecedent were true, the statement would not be a counterfactual to the reasoning body, which goes against the supposition that it is a counterfactual. The antecedent is always false in every alternative world that a reasoning body could consider possible. (3) Under the stated truth judgement, we have that ¬(a > b) is true if and only if it is not the case that a > b is true.

(Pre-

  1 = [M |= F ] and 1 = [M |= ¬F ], or both 0 = [M |= F ] and 0 = [M |= ¬F ] for some F ∈ F under some M? Thirdly, should it happen that [M |= F ] = 0 = 1 for any formula F , given a valuation frame?

  Then for any valuation frame it holds that [M |= F ] = [M |= recursiveReduce(recursiveReduce(F ))]. Proof: recursiveReduce(recursiveReduce(F )) is in conjunctive normal form. Transform this to disjunctive normal form, and observe that almost all the clauses are assigned 0. Details are in Appendix E. Proposition 6 (Complementation/Double negation): For any F in unit chain expansion and for any valuation frame, it holds that 1 = [M |= F ∨ recursiveReduce(F )] and that 0 = [M |= F ∧ recursiveReduce(F )] (complementation). Also, for any F ∈ F in unit chain expansion and for any valuation frame it holds that [M |= F ] = [M |= recursiveReduce(recursiveReduce(F ))] (double negation).

  for some k ∈ N and some s0, . . . , s k ∈ S, then it is said to be at the (k+1)-th object level. Further, assume a function toSeq : N → S * satisfying toSeq(0) = ǫ andtoSeq(k + 1) = ⊤. . . . .⊤ k+1 . (F : F, object level : N)returning either 0 or 1 \\ This pseudo-code uses n, o : N, Fa, F b : F. L0: Duplicate F and assign the copy to Fa. If Fa is not already in unit chain expansion, then reduce it into a formula in unit chain expansion. L1: F b := EXTRACT(Fa, object level). L2: n := COUNT DISTINCT(F b ). L3 0 : For each I : toSeq(object level) × S distinct for the n elements of S at the given object level, Do: L3 1 : If UNSAT(F b , I), then go to L5.

L3 2 :

 2 Else if no unit chains occur in Fa, go to L3 5 . L3 3 : o := (REWRITE(Fa, I, object level), object level + 1).

L3 4 : 5 :

 45 If o = 0, go to L5. L3 End of For Loop. L4: return 1. \\ Yes. L5: return 0. \\ No.

  Fw]: Similar. e) Fz = (Fu ⋗Fv)⋗Fw: This case is impossible due to the observation given earlier in the current proof. f) Fz = (F1[(Fu ⋗ Fv) ⋗ Fw] ⋗ F2) ⋗ F3: Similar. g) The rest: all similar. 3) ⋗ reduction 2: Similar. 4) ⋗ reduction 3: Similar. 5) ⋗ reduction 4: Consider how Fz looks like: a) Fz = s⋗(F1∧F2): Then ¬Fz ¬((s⋗F1)∧(s⋗F2)).But by Lemma 8, it does not cost generality if we reduce the ¬ to have;¬((s ⋗ F1) ∧ (s ⋗ F2)) ¬(s⋗F1)∨¬(s⋗F2). Meanwhile F ′ z = s c ∨(s⋗¬(F1∧F2)). By Lemma 8, it does not cost generality if we haveF ′′ z = s c ∨ (s ⋗ (¬F1 ∨ ¬F2)) instead of F ′ z .But it also does not cost generality (by Lemma 7) if we haveF ′′′ z = s c ∨ (s ⋗ ¬F1) ∨ (s ⋗ ¬F2) instead of F ′′ z .But by Lemma 8, it again does not cost generality if we haveF ′′′′ z = s c ∨ (s ⋗ ¬F1) ∨ s c ∨ (s ⋗ ¬F2) instead.Therefore we can conduct bisimulation between ¬(s ⋗ F1) and s c ∨ (s ⋗ ¬F1) and between ¬(s⋗F2) and s c ∨(s⋗¬F2). Since each of ¬(s ⋗ F1) and ¬(s ⋗ F2) has a strictly smaller formula size than ¬(s ⋗ (F1 ∧ F2)), (sub-)induction hypothesis. Contradiction. b) The rest: Trivial. 6) ⋗ reduction 5: Similar.APPENDIX J: AN ESSAY ON REASONING ABOUT

  Object 1 is which has an attribute of Object 2 .• It is true that Object 1 is, but it is false that it has an attribute of Object 2 .

	The presence of negation flips "It is true that . . . " into "It
	is false that . . . " and vice versa. But it should be also noted
	how negation acts in attribute negations and object/attribute
	negations. Several specific examples 3 constructed parodically
	from the items in the hat shop episode are;
	1) Hat ⋗ Yellow: It is true that hat is, and it is true that it is
	yellow(ed).
	2) Yellow ⋗ Hat: It is true that yellow is, and it is true that
	it is hatted.
	3) Hat ⋗ ¬Yellow: It is true that hat is, but it is false that it
	is yellow(ed). 4
	4) ¬Hat ⋗ Yellow: It is false that hat is, but it is true that
	yellow object (which is not hat) is.
	5) ¬(Hat ⋗ Yellow): Either it is false that hat is, or if it is
	true that hat is, then it is false that it is yellow.

  Any formula F0 ∈ F reduces into some formula in unit chain expansion.Proof: By induction on maximal number of ¬ nestings and a sub-induction on formula size. Lemma 2 for base cases. Details are in Appendix B.Lemma 4: For any F ∈ F expanded in unit chains, there exists v ∈ {0, 1} such that [M |= F ] = v for any valuation frame.Proof: Since a value 0/1 is assignable to any element of S ∪ U by Definition 2, it is (or they are if more than one in {0, 1}) assignable to [M |= F ].

	Lemma 3 (Reduction):

2) F0 = F1 ⋗ F2: Apply induction hypothesis on F1 and F2 to get F ′ 1 ⋗ F ′ 2 where F ′ 1 and F ′ 2 are formulas in unit chain expansion. Then apply Lemma 1.

  condition) Some domain of discourse D is given. For intuition, assume that D represents the mind of an individual. D is assumed to be a logical space. Knowledge is what holds in D in which, like in gradual classical logic, nothing can designate a unique and indivisible object (Cf. Introduction and Postulate 1): any one of them may be precise enough but never unique. We suppose that 'emu' and 'the state of being flying' are in the knowledge.

	L1	If either 'flying emu' or Y holds in knowledge, then
		return false.
	L2	Duplicate knowledge. Apply a function F: knowl-
		edge → knowledge such that F(duplicated space) ⊆
		knowledge. The F(duplicated space) is what we here
		call imagination.
	L3

'We' is preferred throughout this document save where the use of the term is most unnatural.

Philosophical, that is, real, reading of the symbols p, q, r, . . . .

I do not pass judgement on what is reasonable and what is not here, as my purpose is to illustrate the reading of ⋗. So there are ones that ordinarily appear to be not very reasonable.

In the rest, this -ed to indicate an adjective is assumed clear and is omitted another emphasis.

That proposition A is true and that proposition A is true mean that proposition A is true; the subject of this sentence is equivalent to the object of its.

In classical logic, that proposition A or proposition B is true means that at least one of the proposition A or the proposition B is true though both can be true. Same goes here.

This is the reading of ¬(Hat ⋗ Yellow).

These two symbols are overloaded. Save whether truth values or the ternary values are supplied as arguments, however, the distinction is clear from the context in which they are used.• For the binary connective ⋗, !0⋗!1⋗!2 for some three recognisable entities is an abbreviation of !0 ⋗ (!1⋗!2). On this preamble we shall begin.

A base logic of a combined logic is one that is used to derive the combined logic.

APPENDIX A: PROOF OF LEMMA 1 First apply ⋗ reductions 2 and 3 on F1 ⋗F2 into a formula in which the only occurrences of the chains are f0 ⋗ F2, f1 ⋗ F2, . . . , f k ⋗ F2 for some k ∈ N and some f0, f1, . . . , f k ∈ U ∪ S. Then apply ⋗ reductions 4 and 5 to each of those chains into a formula in which the only occurrences of the chains are: f0 ⋗ g0, f0 ⋗ g1, . . . , f0 ⋗ gj , f1 ⋗ g0, . . . , f1 ⋗ gj, . . . , f k ⋗ g0, . . . , f k ⋗ gj for some j ∈ N and some g0, g1, . . . , gj ∈ U. To each such chain, apply ⋗ reduction 1 as long as it is applicable. This process cannot continue infinitely since any formula is finitely constructed and since, under the premise, we can apply induction on the number of elements of S occurring in gx, 0 ≤ x ≤ j. The straightforward inductive proof is left to readers. The result is a formula in unit chain expansion. APPENDIX B: PROOF OF LEMMA 3 By induction on maximal number of ¬ nestings and a subinduction on formula size. We quote Lemma 2 for base cases. For inductive cases, assume that the current lemma holds true for all the formulas with neg max(F0) of up to k. Then we conclude by showing that it still holds true for all the formulas with neg max(F0) of k+1. Now, because any formula is finitely constructed, there exist sub-formulas in which occur no ¬. By Lemma 2, those sub-formulas have a reduction into a formula in unit chain expansion. Hence it suffices to show that those formulas ¬F ′ with F ′ already in unit chain expansion reduce into a formula in unit chain expansion, upon which inductive hypothesis applies for a conclusion. Consider what F ′ is: 1) s: then apply ¬ reduction 1 on ¬F ′ to remove the ¬ occurrence. 2) Fa ∧F b : apply ¬ reduction 2. Then apply (sub-)induction hypothesis on ¬Fa and ¬F b . 3) Fa ∨F b : apply ¬ reduction 3. Then apply (sub-)induction hypothesis on ¬Fa and ¬F b . 4) s ⋗ F ∈ U: apply ¬ reduction 4. Then apply (sub-)induction hypothesis on ¬F .

APPENDIX C: PROOF OF LEMMA 5

(Note again that we are assuming well-formed formulas only.) For the first one,

For the second obligation,

Again by the definition of I, we have the required result. That these two events are mutually exclusive is trivial.

APPENDIX D: PROOF OF PROPOSITION 4

Let us generate a set of expressions finitely constructed from the following grammar;

Then first of all it is straightforward to show that [M |=D Fi] = Xi for each i ∈ {1, 2, 3} for some X1, X2, X3 that the above grammar recognises. By Lemma 5 each atomic expression ([M |=D fx] for some fx ∈ U ∪ S) is assigned one and only one value v ∈ {0, 1} (again note that we are considering wellformed formulas only). Then since

and 1 ∧ † 1 = 1 by definition given at the beginning of this section, it is also the case that [M |=D Fi] is assigned one and only one value vi ∈ {0, 1} for each i ∈ {1, 2, 3}. Then the proof for the current proposition is straightforward.

Here, assume that the right hand side of the equation which is in conjunctive normal form is ordered, the number of terms, from left to right, strictly increasing from 1 to k + 1. Then as the result of a transformation of the conjunctive normal form into disjunctive normal form we will have 1 (the choice from the first conjunctive clause which contains only one term s0) × 2 (a choice from the second conjunctive clause with 2 terms s c 0 and s0 ⋗ s1) × . . . × (k + 1) clauses. But almost all the clauses in [M |=D (the disjunctive normal form)] will be assigned 0 (trivial; the proof left to readers) so that we gain

APPENDIX F: PROOF OF PROPOSITION 6 Firstly

By Proposition 4, F has a disjunctive normal form:

j=0 recursiveReduce(fij ), which, if transformed into a disjunctive normal form, will have (h0 + 1) [a choice from recursiveReduce(f00), recursiveReduce(f01), . . . , recursiveReduce(f 0h 0 )] × (h1 + 1) [a choice from recursiveReduce(f10), recursiveReduce(f11), . . . , By induction on the number of reduction steps and a subinduction on formula size, we first establish that F(F1) = F(F2) (by bisimulation). Into one way to show that to each reduction on F ′ corresponds reduction(s) on F is straightforward, for we can choose to reduce F into F ′ , thereafter we synchronize both of the reductions. Into the other way to show that to each reduction on F corresponds reduction(s) on F ′ , we consider each case:

1) The first pair. a) If a reduction takes place on a sub-formula which neither is a sub-formula of the shown sub-formula nor has as its sub-formula the shown sub-formula, then we reduce the same sub-formula in F ′ . Induction hypothesis (note that the number of reduction steps is that of F into this direction). b) If it takes place on a sub-formula of Fa or F b then we reduce the same sub-formula of Fa or F b in F ′ . Induction hypothesis. c) If it takes place on a sub-formula of Fc then we reduce the same sub-formula of both occurrences of Fc in F ′ . Induction hypothesis. d) If ⋗ reduction 2 takes place on F such that we have;

where F and Fx differ only by the shown subformulas, 12 then do nothing on F ′ . And Fx = F ′ . Vacuous thereafter. e) If ⋗ reduction 2 takes place on F such that we have;

where F d = Fa and F d = F b , then without loss of generality assume that

Then we apply ⋗ reduction 2 on the

such that F ′′′ and F ′ x differ only by the shown subformulas, we repeat the rest of simulation on F ′ x and F ′′′ . Induction hypothesis. f) If a reduction takes place on a sub-formula Fp of F in which the shown sub-formula of F occurs as a strict sub-formula (F

But we have 12 This note 'where . . . ' is assumed in the remaining.

Therefore we apply the same reduction on F ′ p to gain;

Induction hypothesis.

2) The second, the third and the fourth pairs: Similar.

3) The fifth pair: a) If a reduction takes place on a sub-formula which neither is a sub-formula of the shown sub-formula nor has as its sub-formula the shown sub-formula, then we reduce the same sub-formula in F ′ . Induction hypothesis. b) If it takes place on a sub-formula of Fa, F b or Fc, then we reduce the same sub-formula of all the occurrences of the shown Fa, F b or Fc in F ′ . Induction hypothesis. c) If ⋗ reduction 4 takes place on F such that we have;

then do nothing on F ′ . And Fx = F ′ . Vacuous thereafter. d) If a reduction takes place on a sub-formula Fp of F in which the shown sub-formula of F occurs as a strict sub-formula, then similar to the case 1) f). By the result of the above bisimulation, we now have F(F ) = F(F ′ ). However, without ¬ occurrences in F it takes only those 5 ⋗ reductions to derive a formula in unit chain expansion; hence we in fact have F(F ) = F(Fx) for some formula Fx in unit chain expansion. But then by Theorem 1, there could be only one value out of {0, 1} assigned to [M |=D Fx] if Fx is well-formed; otherwise, illFormed is assigned.

APPENDIX H: PROOF OF LEMMA 8

By simultaneous induction on reduction steps and by a sub-induction on formula size. One way is trivial. Into the direction to showing that to every reduction on F corresponds reduction(s) on F ′ , we consider each case. For the first case;

1) If a reduction takes place on a sub-formula which neither is a sub-formula of the shown sub-formula nor has as its sub-formula the shown sub-formula, then we reduce the same sub-formula in F ′ . Induction hypothesis. 2) If it takes place on a sub-formula of Fa or F b then we reduce the same sub-formula of Fa or F b in F ′ . Induction hypothesis. 3) If ¬ reduction 2 takes place on F such that we have;

Fx[¬Fa ∨ ¬F b ], then do nothing on F ′ . And Fx = F ′ . Vacuous thereafter. 4) If ¬ reduction 2 takes place on F such that we have;

Fx[¬F d ∨ ¬Fe] where F d = Fa and F d = F b , then without loss of generality assume that F d ∧ F β = Fa and that F β ∧ F b = Fe. Then we apply ¬ reduction 2 on the ¬(F d ∧ F β ) in F ′ so that we have;