An example of a classic tautology would be ¬¬A ↔ A. Since double negative elimination is not intuitionistically valid, this classic tautology would not be an intuitionisitic tautology since ¬¬A → A is not intuitionistically valid.
I am particularly interested in De Morgan's rules. The following are classic tautologies:
- (A ∨ B) ↔ ¬(¬A ∧ ¬B)
- (A ∧ B) ↔ ¬(¬A ∨ ¬B)
I wasn't able to prove them without using indirect proof, law of the excluded middle or double negation elimination. However, that does not mean that they can't be shown to be true using only intuitionistic natural deduction rules: (into and elim rules for conjunction, disjunction, conditional and negation).
More generally I wonder if there is a reference list of relatively common classic tautologies that are not intuitionistic tautologies?