# Finding a language that is $NP^L$-complete

I'm trying to prove a theorem and as a lemma I would like to identify an $$NP^L$$-complete language. I was thinking something like a machine that can decide $$SAT$$ equipped with an oracle for $$L$$ can decide every language in $$NP^L$$, but I'm not sure how to formalize this. Here's my attempt at doing so

$$SAT^L = \{\text{satisfiable boolean formulas with some clauses as }L(x_1, \dots, x_k)\}$$

The clauses that are of the form $$L(x_1, \dots, x_k)$$ are queries that are true if and only if $$(x_1 \cdots x_k) \in L$$.

I think $$SAT^L$$ is $$NP^L$$-complete, for any language $$L$$, but I don't know how to prove this. It's of course in $$NP^L$$ since we can take a witness assignment and check it, and we can check the $$L(\cdot)$$ predicates with a query to our oracle to $$L$$. I'm not sure how to prove $$NP$$-hardness though.

I was thinking of just modifying Cook-Levin's construction so that I could add additional clauses to the formula of the form $$L(x_1, \dots, x_k)$$ when encoding the computation graph of an NTM $$M^L$$ but I'm not sure if this works in general, and is honestly more of a rough idea than anything else. This construction seems to be pretty sensitive to the "implementation" of the oracle queries, so I'm not sure how to make this rigorous.

Is there a more standard example of a $$NP^L$$-complete language?

What you are looking for is a relativization of the Cook-Levin theorem in the sense that you consider SAT and NP relative to an oracle for $$L$$. You can find the answer to that in this answer, point number 2. There you get (an extension of) Circuit-SAT as a complete language; reducing this to your version of SAT should not be too hard.
Note that, as mentioned in the linked answer, this is a bit different than a relativization in the sense that it is the reduction which possesses an oracle for $$L$$.