Also, the description of the boolean satisfiability problem isn't the boolean satisfiability problem at all, but just what we might call the boolean evaluation problem, or a version of the circuit value problem, which is certainly in P.

I have no idea what's going on in the lambda calculus excerpt further down the page, in particular substituting (λx.x x) with (x x)? There seems to be a fairly big misunderstanding here. And lambda calculus isn't reduced in any particular order -- there are many ways to reduce the same term.