Editing Intuitionistic logic (section)

==== Intermediate logics ====
In 1932, [[Kurt Gödel]] defined a system of logics intermediate between classical and intuitionistic logic. Indeed, any finite Heyting algebra that is not equivalent to a Boolean algebra defines (semantically) an [[intermediate logic]]. On the other hand, validity of formulae in pure intuitionistic logic is not tied to any individual Heyting algebra but relates to any and all Heyting algebras at the same time.

So for example, for a [[Axiom schema|schema]] not involving negations, consider the classically valid <math>(A\to B)\lor(B\to A)</math>. Adopting this over intuitionistic logic gives the intermediate logic called [[Gödel-Dummett logic]].