Skip to main content
1 of 2
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.

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