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

Jacques-Henri Jourdan jacques-henri.jourdan at normalesup.org
Wed Aug 24 17:20:40 CEST 2016


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


More information about the Iris-Club mailing list