Definition of the Decryption oracle 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.
In the standard definition of security for public key encryption schemes there exists only one public key.
Therefore the decryption oracle will always decrypt with the secret key that corresponds to the public key given to the attacker. It does not matter how the $c_1$ in your question is computed, it can be computed using the real public key, a different public key or might even be random garbage. The decryption oracle doesn't care, it simply runs the decryption algorithm with the secret key produced earlier in the security game and the input provided by the attacker.
Whether this results in a valid decryption or not depends on the encryption scheme and is not part of the security definition.