As a PS to my last email: I've been thinking more about the last point, i.e., whether []([]A -> A) indeed captures an inhabitation law shared by both comonadic and most monadic operators. It is not really the case. For normal comonadic ones, it trivially holds, as I discussed before. But I realized that monadic examples already mentioned by Andrej are rather special. Without going into the full generality of monads on aribitrary categories, it's enough to have a look at the building blocks of nuclei on a frame. Harold Simmons denotes these as u_a(x) := a \vee x v_a(x) := a -> x w_a(x) := (x -> a) -> a As Andrej noticed in his third example, v_a(v_a(x) -> x) = \top for any a. w_a generalizes double negation, so with a = \bot it turns into Andrej's second example. But for other a, it is not in general not true that w_a(w_a(x) -> x) = \top. Just consider the three-element Heyting algebra, call the middle element * and note that w_*(w_*(\bot) -> \bot) = * And u_a(u_a(x) -> x) = \top can be also refuted in the three-element Heyting algebra. So if one wants f to be monadic, one cannot generalize Andrej's examples too much. On 18/08/16 14:07, Tadeusz Litak wrote:
Dear Andrej,
as you mentioned modal logic, here are three modal cents.
All the examples you mention are not only monotone, but also are what modal logicians would call "normal boxes" or "dual operators", i.e., the satisfy the law
f (A -> B) -> f A -> f B
and the "necessitation" or "G??del" rule A/ f A
Is it actually, intended that these laws should hold?
(Actually, all your examples also satisfy the inflationary law A -> f A, which is commonly thought to be more typical of "diamonds" or "operators", which led some researchers to, e.g., reconstruct such beasts in terms of combinations of boxes an diamonds. But from my point of view, as long as you satisfy the normality laws, you're a perfectly good box).
At any rate, when one is talking about normal boxes, your law []([]A -> A) holds in all extensions of the modal logic T: the modal logic of reflexive relations, axiomatized by []A -> A, i.e., a "deboxed" variant of your formula. This is obviously thanks to that "necessitation" or "G??del" rule.
Your axiom even has what modal logicians call a "local" FO counterpart, i.e., a first-order formula \phi(x), which is satisfied by a given point in a Kripke structure iff the original modal formula holds at that point under all valuations. This formula is "all successors are reflexive", i.e.,
\forall y. (x R y -> y R y)
(I'm omitting here correspondence for intuitionistic modal logics, but can do it in another mail if you care. It isn't much more complicated than that)
This means that your axiom holds in many typical modal logics, esp. S4 a.k.a. the "comonadic" logic or the logic of Kuratowski's interior operator or the logic of all (finite) preorders or the logic of partial orders. Extensions of S4, in turn, include the Grzegorczyk logic of all finite partial orders/finite trees or S5, the logic of all (finite) equivalence relations.
On the other hand, the L??b axiom is a wrong route to go in your case. Adding your axiom to the L??b logic would trivialize the box into the "verum" operator: []A would be true for every A. In the provability setting, one sometimes adds (following Solovay) []A -> A to the L??b system, but even then one is not closing under necessitation.
What is more curious, though, is that all your examples are monadic in nature, whereas the T axiom and its extensions have "comonadic" character. I've never realized that an axiom like yours can provide a common ground for both; nice!
HTH, best, t.
On 15/08/16 22:05, Andrej Bauer wrote:
Dear all,
I have come accross a certain kind of operators, and I wonder if they have a name or have been encountered before.
We work internally in a topos with a subobject classifier ??. For the purposes of this discussion, call a monotone map f : ?? ??? ?? *good* if
(*) ??? p : ??, f (f p ??? p)
is valid in the topos.
Some examples of good maps are:
1. The identity map. 2. The double negation map. 3. For any q ??? ??, the j-operator p ??? (q ??? p).
Is the condition (*) known? Can you think of other examples of good maps (perhaps in specific toposes)?
I have so far just one connection: in provability logic condition (*) appears (without the universal quantifier) as the antecedent of L??b's theorem, which sttates that ??? (??? p ??? p) ??? ??? p.
With kind regards,
Andrej
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]