[TYPES] Encoding of negation

[Rowan Davies]

I agree with Vladimir, although I would also offer the following slightly
more direct counterexample for the conjecture:

If we consider
    A =  (not A1) -> A2        with A1 and A2 not containing 'not'
then
  A* = all Z. (A1 -> Z) -> A2      (since A1*=A1and A2*= A2, in the absence
of not)

In this case, the conjecture (with an empty context)  would assert the
equivalence between the first (in IL) and the second (in CL).

But, the second is logically equivalent to A2, since choosing p=A1 yields
(A1 -> A1) which  forces A2, and p does not appear in A2, hence it must be
true independent of p.

So, the conjecture would relate:
     (not A1) -> A2     with     A2

This seems very unlikely between any two reasonable logics, given that the
second is independent of A1.

Having said that, I see the motivation in making the conjecture, and
considering that it holds for an important case, I wonder:
    How large is the set of formulas/type for which it holds?