[TYPES] Encoding of negation

Peter Selinger selinger at mathstat.dal.ca
Thu Aug 30 23:45:49 EDT 2007

Vladimir Komendantsky wrote:
> You couldn't have ever expected Gamma |- B classically iff Gamma* |- B*
> intuitionistically because this is false for your definition of *.

It certainly holds for the Hofmann-Streicher-Reus translation, and
also for Goedel's translation. The right-to-left implication is
trivial in those cases because in each case, A = A** holds

-- Peter

More information about the Types-list mailing list