...intuitionist logic is closely tied up with Constructive Mathematics (not to be confused with a similarly named educational fad) which insists that you always construct things you claim exist. This means that it goes hand in hand with computer science where people's programs are usually expected to produce a result - not just say a result exists.Which is funny, because "there exists" statements abound in (theoretical) computer science, especially when dealing with combinatorial constructions. Admittedly, the gap between "there exists" and "here it is" is often an exponential rather than infeasible gap (the probabilistic method, for example).

He goes on to discuss higher-order logics, and mentions an interesting fact:

Quine believed that Second Order Logic isn't even Logic.and goes on to say:

And even though Second Order Logic appears to have greater expressive power mathematicians actually get along fine with First Order Logic. Every time they make a statement about properties there's always a workaround (sometimes quite inelegant) for expressing something that's just as useful in First Order Logic.Aha, but that's not true for NP, for example. After all, NP is equivalent to a restricted form of second order logic, and P is First Order logic augmented with an ordering and fixed point operator.

Yet another nugget that I learned from this article is the existence of "Quantum Logic". Namely,

Quantum Logic really is the quantization of logic - we have replaced truth values with non-commuting Hermitian operators whose eigenvalues are the results we want!Overall, a very illuminating article.