Jason (jcreed) wrote,

I think I made a small breakthrough in my understanding of classical logic vis-a-vis intuitionistic logic tonight, staring at the standard quantifier-exchange formula
(~ forall x . A(x)) ==> (exists x . ~A(x))
It is valid classically, invalid intuitionistically, and still invalid intuitionistically if you slap a not-not out front of it. It is an example (unless I made a mistake in pronouncing it unprovable) of the kind of formula I was looking for, one that demonstrates the necessity of the full recursive Goedel-Kolmogorov-Gentzen double-negation translation, but sadly it's first-order. I was hoping a nice little example would exist in the propositional fragment, but I'm finally starting to believe that none exists. I guess that means the type-theoretic consequences of a "classically true" modality are only going to be nontrivial in a system which is already saddled with dependent types. That's kind of a bummer.


Okay, trurl just informed me that the fact that "if classically A, then intuitionistically ~~A" holds for the propositional fragment is known as Glivenko's theorem. I feel comforted to know it has someone's name attached to it after all.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment