For a local operator (that is, a j-operator) condition (*) is equivalent to the condition that the associated j-sheaf functor preserves Omega; see A4.5.8 in the Elephant (specifically, condition (vi)). I don't know whether there are any interesting examples other than local operators. Peter Johnstone On Mon, 15 Aug 2016, 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/ ]