Equality through Negation

[Taken from SEP; "Intuitionistic Logic"] ...Rejection of Tertium Non Datur

Intuitionistic logic can be succinctly described as classical logic without the Aristotelian law of excluded middle:

A∨¬A(LEM)
or the classical law of double negation elimination:

¬¬A→A(DNE)
but with the law of contradiction:

(A→B)→((A→¬B)→¬A)
and ex falso sequitur quodlibet:

¬A→(A→B).
Brouwer [1908] observed that LEM was abstracted from finite situations, then extended without justification to statements about infinite collections. For example, let x,y range over the natural numbers 0,1,2,… and let B(y) abbreviate (prime(y)&prime(y+2)), where prime(y) expresses “y is a prime number.” Then ∀y(B(y)∨¬B(y)) holds intuitionistically as well as classically, because in order to determine whether or not a natural number is prime we need only check whether or not it has a divisor strictly between itself and 1.

But if A(x) abbreviates ∃y(y>x&B(y)), then in order to assert ∀x(A(x)∨¬A(x)) intuitionistically we would need an effective (cf. the Church-Turing thesis) method to determine whether or not there is a pair of twin primes larger than an arbitrary natural number x, and so far no such method is known. An obvious semi-effective method is to list the prime number pairs using a refinement of Eratosthenes’ sieve (generating the natural numbers one by one and striking out every number y which fails to satisfy B(y)), and if there is a pair of twin primes larger than x this method will eventually find the first one. However, ∀xA(x) expresses the Twin Primes Conjecture, which has not yet been proved or disproved, so in the present state of our knowledge we can assert neither ∀x(A(x)∨¬A(x)) nor ∀xA(x)∨¬∀xA(x).

(...)

The rejection of LEM has far-reaching consequences. On the one hand,

Intuitionistically, reductio ad absurdum only proves negative statements, since ¬¬A→A does not hold in general. (If it did, LEM would follow by modus ponens from the intuitionistically provable ¬¬(A∨¬A).)
Intuitionistic propositional logic does not have a finite truth-table interpretation. There are infinitely many distinct axiomatic systems between intuitionistic and classical logic.
Not every propositional formula has an intuitionistically equivalent disjunctive or conjunctive normal form, built from prime formulas and their negations using only ∨ and &.
Not every predicate formula has an intuitionistically equivalent prenex normal form, with all the quantifiers at the front.
While ∀x¬¬(A(x)∨¬A(x)) is a theorem of intuitionistic predicate logic, ¬¬∀x(A(x)∨¬A(x)) is not; so ¬∀x(A(x)∨¬A(x)) is consistent with intuitionistic predicate logic.