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