Note that (9) is the only place where monotonicity is used. I wonder whether it could be actually deduced from the rest.
As I mentioned in a subsequent message, this is actually not the only place where I had to use monotonicity. Now I realized that monotonicity cannot be deduced from f(fp -> p) without additional assumptions. Consider fp = (p or not p); then f(fp -> p) = (not p or not not p), so that f(fp -> p) holds iff the topos is de Morgan, whereas f is monotone iff the topos is Boolean (since f0 = 1).
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/ ]