> I am not sure this is true for "all" mathematics. You're still using some metalogical axioms that are always true. In particular, laws of untyped lambda calculus (or any other model of universal computation) are "axioms" that you consider unquestionably true (just like you can consider unquestionable that objective shared mathematical reality exists).
Although, if you informally asked me if the rules of logic were true, then I would say that of course they are, if you asked me formally I think I would say that they are not unquestionably true, only unquestionable if you want to do classical mathematics. If you're willing to grant basic rules of logic, then certain consequences follow. If you're not, then you're not doing classical mathematics, although you might still be doing interesting mathematics—for example, if you decide not to accept the law of the excluded middle.
Yes, the law of the excluded middle is an interesting one to exclude. You could also try and go without certain infinities: eg you could remove induction (and things equivalent to induction) from your toolset, and see how far you can go.
There's quite a bit of ideology / philosophy about excluding the law of the excluded middle. But even if you set these aside, it turns out that 'constructive logic' without the 'excluded middle' has enormous practical applications in eg computer science.