In the context of public-key encryption, what would be a formal definition of the decryption oracle?
I know the informal definition (i.e., a function that is available to the adversary and that provides the decryption of any ciphertext of her choice, except for the challenge ciphertext), but I am looking for a formal definition. I have checked some reference textbooks and papers and it is usually defined informally, just before (formally) defining chosen-ciphertext attacks. I am specially interested in a multi-user setting, since I will later be working on definitions of security for proxy re-encryption, but I want first to fully understand the concepts for the case of PKE.
The motivation behind this question is that I don't know if it is necessary to specify the underlying public-key in the oracle query or if it is something implicit. For instance, let us assume that the adversary creates ciphertext $c_1 = Enc(pk_1, m)$. Is it assumed that the decryption oracle should answer the query $\mathcal D(c_1)$, even if the public key used is not specified? In the case that the decryption oracle permits to specify the associated public key, would it be valid the query $\mathcal D(pk_2,c_1)$? That is, trying to "deceive" the decryption oracle into decrypting with a different key.