Re: Examples of certain monotone operators

Re: Examples of certain monotone operators

[Mamuka Jibladze]

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

Re: Examples of certain monotone operators: errata

[Mamuka Jibladze]

There are some problems with my previous post, sorry

> (1) q -> fp = f(q -> p) ; in particular, f is inflationary.
> This has been pointed out by Ingo Blechschmidt

Actually inflationarity does not follow from this directly,
(1) only gives q -> fq = f1

To show f1 = 1 use f(fp -> p) with p = 1

> (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

lhs indeed becomes true but the rhs is not yet what we want,
it is (fq & fp) -> f(fq & fp & p) = f(fq & p).
To finalize, f(fq & p) -> f(q & p) has to be proved,
and here it seems I cannot get away without another use
of monotonicity: from fq & p -> f(q & p) it gives
f(fq & p) -> ff(q & p) and then one can use (6).

As for fq & p -> f(q & p), it is obtained from (7) as explained
in the last remark of my previous post.

Mamuka


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Examples of certain monotone operators

[Mamuka Jibladze]

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