[Iris-Club] Frame-preserving update and double-negation

[Jacques-Henri Jourdan]

Hi,

I've been fighting against an apparent paradox: Joe says that (P -* 
False) -* False implies |=r=> P and Robbert said the former is always 
True when used on a later. So, that would mean that |=r=> >P is always 
true, which is rather annoying.


The problem is in the following:

 > It is not hard to show that (P -* False) -* False implies |=r=> P.

In reality, the easy way is the other one, from |=r=> P to (P -* False) 
-* False. Proving |=r=> P requires many hypotheses

-- 
JH