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