[TYPES] Encoding of Negation

[Eike Ritter]

Dear all,

it is also very interesting to consider not only provability but also
proofs in the question how to encode negation.

Hofmann and Streicher not only give a continuation interpretation of
classical logic which has the desired property that A |- B classically
iff A* |- B* intuitionistically but also extend this translation to
the level of proofs by converting any classical proof of A |- B into
an intuitionistic proof of A* |- B*. Extending this correspondence to
the level of proofs is subtle. Hofmann and Streicher present a
translation of classical proofs for formulae consisting of negation,
implication and conjunction. We show in [1] that addition of
disjunction is problematic, and that only the addition of classical
(multi-conclusioned) disjunction works, not a version of
intuitionistic sums.

[1] D.J. Pym and E. Ritter. On the semantics of classical
disjunction. Journal of Pure and Applied Algebra, vol 159,
pp. 315--338.

David Pym and Eike Ritter