[sv-ac] non-vacuity and derived forms

Hi Doron:

I don't think that using the semantic derivations to 
infer non-vacuity for derived forms gives the desired 
result in all cases.

I know that 1932 does not say explicitly to use the semantic
derivations, but it is sort of implicit, since otherwise 
non-vacuity for the derived forms is not defined.

The one problematic example I have found so far is if-else.
We get

   w |=^{non} if(b) P_1 else P_2
   ???  w |=^{non} ((b |-> P_1) and (weak(b) or P_2))
   iff  w |=^{non} b |-> P_1 or w |=^{non} weak(b) or w |=^{non} P_2
   iff  [w |=^{non} weak(b)]
        true

which is not what we want.  I think that what we want is something
like 

   w |=^{non} if(b) P_1 else P_2
   iff  w |=^{non} b |-> P_1 or (w |/= weak(b) and w |=^{non} 1 |-> P_2)

J.H.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.