Intuitonism and metamathematics. There are various reasons why one would want to reject the law of the excluded middle when doing "normal" mathematics, which I won't get to here, but accepting those, does the same reasoning hold when thinking about metamathematics? Of course, there are many different "levels" of intuitionism and constructivism, but it seems strange to me that a constructionist would rely on results like the Löwenheim–Skolem theorem, when it uses LEM at the metamathematical level. Isn't assuming LEM, even if at a metamathematical level, begging the question for an intuitionist? Are there philosophical reasons to believe that it may be more or less acceptable to use LEM at the metamathematical level from a constructive standpoint?
Furthermore, is there a computational interpretation of metamathematics in general? Its just a hunch, but it seems to me like metamathematics, and using LEM at the metamathematical level might be related to oracles in some way, but I have no sources for this.
 A: This is more a philosophical question than a mathematical one. If you think that even logic (reasoning about formal systems) is just a symbol game that is played with the inference rules of the meta-system, then the question is meaningless as we simply play and never question the rules.
However, if you believe that PA is either consistent (there is no sentence over PA that it both proves and disproves) or inconsistent (there is some sentence over PA that it both proves and disproves), in the sense that one of the two possibilities actually is a fact in the real world, then you essentially have accepted LEM for a $Σ_1$-sentence about the real world (suitably understood). This is equivalent to accepting that an given program on an input either halts or does not halt. Once you do this the next natural step is to ask about the halting behaviour of programs that have access to the halting oracle. Each step of their execution is well-defined, since it is either computable or it requires asking the halting oracle one question, which we have already agreed has a well-defined answer. And so naturally you get the next Turing jump. And you can continue this reasoning for finitely many jumps. In this sense it seems that the meta-system you would have to accept is not only classical but has the same strength as ACA. (See this post for a more detailed analysis.)
Indeed, intuitionistic logic corresponds directly to programs via the BHK interpretation, and every invocation of LEM corresponds to an oracle query in the program. A proof can also be understood via game semantics where "$\forall$" gets the Refuter's move while "$\exists$" gives the Prover's move, and LEM asks the Refuter to choose between two cases. The distinction between "$\forall$" and LEM is that for the quantifier the Refuter must give evidence that the object he provides is of the claimed type, and the Prover can make use of this evidence in her game play, whereas for LEM the Refuter does not have to give any evidence whatsoever of the choice. Notice that "$A \to B$" can only be used in implication elimination when you have also deduced "$A$", which means you have evidence for "$A$" that can be fed to the program that witnesses "$A \to B$". Likewise for universal quantifier elimination. Not so for LEM, which means that a proof that uses LEM corresponds to a program execution that will get stuck at the invocations of LEM until someone feeds it the evidence needed (for one of the cases) to continue along.
A: There is a metamathematical/philosophical use of the law of excluded middle in authors like Errett Bishop that has been spotted by Sam Sanders.  Namely, such authors believe that mathematics is either classical (using LEM) or constructive (eschewing LEM).  No middle ground!  That's a metamathematical reliance on the excluded third.
