[CST-2] T in C

[M.Y.W.Y. Becker]

--On 04 June 2001 21:20 +0100 Shu Yan Chan <syc22@cam.ac.uk> wrote:

>
> ----- Original Message -----
> From: "M.Y.W.Y. Becker" <mywyb2@cam.ac.uk>
> To: <cst-2@srcf.ucam.org>
> Sent: Monday, June 04, 2001 9:03 PM
> Subject: Re: [CST-2] D CommII and TinC
>
>
>> So the axioms of the logic are T, F and possibly sets of processes.
>>
>> > of state/process. Then, how can we be convince that if an assertion is
>> > true for B, and B is bisimiliar to C, the assertion would also be true
>> > for C as well?  If the assertion is just true for process B, then
>> > it would not hold true for C...  Clearly I have some big miss
>> > understanding somewhere...
>>
>> If B is an element of the assertion (which is a denotation of a set) why
>> shouldn't C also be an element of the assertion?
>
> My question really is, can't I define a set which only has B as its
> element, and use that as an assertion. Then even though B bisimilar to C,
> C would not be an element of that assertion?  What stopping me to make
> such definition?
>

I see. Just take T and F as atoms then, as defined on the page, where HM 
logic was introduced. So this theorem only holds for HM logic, and not for 
the mu-calculus, but only because in mu-calculus we allow process sets to 
be atoms. (?)
However, adding this axiom doesn't make the logic more expressive, as long 
as we only allow finite sets to be atoms.

Mo