2

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?

|improve this question
  • 1
    There is a note here: proofwiki.org/wiki/… that claims to answer the immediate question, but without proofs (despite the name of the wiki?) – jobermark Aug 14 at 3:09
  • 1
    Despite Heyting, tautologies are basically alien to the notion of intuitionism or constructivism. If you are looking for a proof that preserves trust, or a construction that can be carried out, omitting the instructions is not the best approach. Brouwer hated the idea of Heyting formalizing his logic. And Kleene rejected logic as the right approach to proof in general, which led him to elaborate recursive function theory more deeply. – jobermark Aug 14 at 3:14
  • 1
    A 'truly constructive' proof results in a function. You can then pick that function up and use it to build other functions more easily than you can back off from the function to one of its Boolean implications and use tautologies to extend the implication. The extended implications are also less 'constructive', because you don't end up with a function you can take elsewhere, just a fact. So it would be quite an unusual undertaking to make such a table. – jobermark Aug 14 at 3:22
  • 2
    In this form both are intuitionistically invalid (since taking B=F or T produces the double negation rule). In the usual form (with the outside negation on the left), the first one is valid and the second one only works one way, see Do De Morgan's laws hold in propositional intuitionistic logic? on Math SE. Here is planetmath's list of some common non-intuitionistic tautologies. There are infinitely many so there can be no exhaustive list. – Conifold Aug 14 at 4:13
  • I updated my answer with a more detailed overview of the De Morgan laws and some tautologies that are intuitionistically valid. – lemontree Aug 15 at 22:32
2

I don't know of any external, more comprehensive list, but here are some of what I'd claim the most prominent statements that are valid classically but not intuitionistically:

  • (¬A→⊥)→A (reductio ad absurdum)
  • ¬¬A→A (double negation elimination)
  • A∨¬A (tertium non datur)
  • ¬(¬A∨¬B)→A∧B (DeMorgan 1a←)
  • A∨B↔¬(¬A∧¬B) (DeMorgan 2a→+←)
  • ¬(A∧B)→¬A∨¬B (DeMorgan 2b←)
  • (A→B)∨(B→A)
  • (A→B)→(¬A∨B)
  • (¬B→¬A)→(A→B) (reverse of contraposition)
  • ((A→B)→A)→A (Peirce's law)
  • (¬A→A)→A (consequentia mirabilis)

For the implications, the reverse direction is provable in intuitionistic logic. In addition, the following are intuitionistically valid:

  • ⊥→A (ex falso quodlibet sequitur)
  • ¬⁢¬⁢¬⁢A→¬⁢A (double negation elimination on negative formulas)
  • ¬A∧¬B↔¬(A∨B) (DeMorgan 1b→+←)
  • (A→¬B)→(B→¬A) (contraposition with negated consequent)
  • A→(B→A) (weakening)

The list of intuitionistically invalid formulas boils down to all those formulas whose derivation requires the use of reductio ad absurdum, or equivalently law of excluded middle, or equivalently double negation eliminiation.

It is provable that for all the propositions which are valid clasically but not intuitionistically, their double negation is derivable intuitionistically (so we have e.g. ¬¬(A∨¬A) though not A∨¬A).

|improve this answer

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.