[Iris-Club] Frame-preserving update and double-negation
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