Date: Mon, 15 Aug 2016 17:05:50 -0300 From: Andrej Bauer <andrej.bauer@andrej.com> To: categories list <categories@mta.ca> Subject: categories: Examples of certain monotone operators
Here is (I hope) a proof that such map is a (sub-open) nucleus. (1) q -> fp = f(q -> p) ; in particular, f is inflationary. This has been pointed out by Ingo Blechschmidt (2) (fp -> p) -> p = fp: reasoning "inside Omega" this is almost trivial - if fp -> p is p, then f(fp -> p) is fp (3) (fp -> p) -> fp = (fp -> p) -> p: (fp -> p) -> fp = [(fp -> p) -> fp] & [(fp -> p) -> (fp -> p)] = (fp -> p) -> [fp & (fp -> p)] = (fp -> p) -> [fp & p] = (fp -> p) -> p (this only required inflationarity of f, at the last step) (4) (fp -> p) -> fp = f((fp -> p) -> p): this is a particular case of (1) (with fp -> p in place of q) (5) (fp -> p) -> p = f((fp -> p) -> p): this follows from (3) and (4) (6) fp = ffp: this follows from (2) and (5) (7) q -> fp = q -> f(q & p): by (1) both are equal to f(q -> p) = f(q -> (q & p)) (8) fq & fp -> f(q & p): in (7), take fq & fp in place of q, then the lhs of (7) becomes true (9) f(q & p) -> fq & fp: monotonicity So f is inflationary, idempotent (6) and multiplicative (8-9). Note that (9) is the only place where monotonicity is used. I wonder whether it could be actually deduced from the rest. I think I have seen in a paper by Anders Kock that any idempotent prenucleus on Omega is a nucleus; and it follows easily (without monotonicity) that q & fp = fq & fp - just apply q & _ to both sides of (7). Glad I'm back, Mamuka
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/ ]