Skip to main content
2 of 2
added 196 characters in body; added 329 characters in body
Joel David Hamkins
  • 236.4k
  • 44
  • 777
  • 1.4k

The translation you refer to is just the double-negative. That is, C is classically derivable if and only if not-not-C is intuitionistically derivable.

What this fact shows is that the use of the law of excluded middle in classical logic can be contained entirely in the proof that C and not-not-C are equivalent.

Edit. Here is a reference to the Gödel–Gentzen negative translation, which explains the translation. The situation is that in propositional logic, one can just use the double negation, but in first order logic, one must perform double negation hereditarily, applying the translation to the subformulas fo the formula. The basic idea is that classical laws of deduction become intuitionistically valid for the double negated forms.

Joel David Hamkins
  • 236.4k
  • 44
  • 777
  • 1.4k