Dear Andrej, On Mon, Aug 15, 2016 at 10:05:50PM +0200, Andrej Bauer wrote:

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. [...] Is the condition (*) known? Can you think of other examples of good maps (perhaps in specific toposes)?

I don't know whether the condition is known, but I do know a further connection. Recall that for any j-operator, there is a generalization of the double negation translation (see for instance Aczel's /The Russel???Prawitz modality/). I'll write phi^j for the translation of a formula phi. It's known and easy to show that for geometric formulas phi, phi^j implies j(phi). In the case that j fulfills condition (*), a slightly stronger statement is true: The formula phi may contain implications, provided that for their antecedents psi it holds that psi ==> psi^j. To verify this, it's convenient to use the following equivalent reformulation of condition (*): forall p, q : Omega, (p ==> j(q)) ==> j(p ==> q). Note that the reverse implication, forall p, q : Omega, (p ==> j(q)) <== j(p ==> q), is satisfied by any j-operator. Best regards, Ingo -- Ingo Blechschmidt Lehrstuhl f??r Algebra und Zahlentheorie Universit??t Augsburg Tel.: 0821/598-5601 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

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/ ]