If X reduces to a problem in NP, is X in NP? Let $X$ and $Y$ be problems, and let $X \le_p Y$.  Is it true that 
\begin{equation}
Y \in NP \rightarrow X \in NP\ ?
\end{equation}

I do mean $NP$ here, not $NP$-complete or $NP$-hard.

The solution is simple if the reduction from $X$ to $Y$ transforms an instance of $X$ to an instance of $Y$; to verify that a solution to $X$ is correct, we could transform it to an instance of $Y$ and then verify that the transformed instance is a solution to $Y$.

All we know from $X \le_p Y$, though, is that you can solve $X$ with a polynomial number of solutions to $Y$; we're not guaranteed a simple one-to-one transformation.

I suspect that 
\begin{equation}
Y \in NP \rightarrow X \in NP
\end{equation}
is true for all $X,Y$ such that $X \le_p Y$, but I would like confirmation, and I would like to know how to prove it.
The answer depends on what you mean by the notation $\le_p$.


If $\le_p$ refers to a Karp reduction (i.e., a many-one reduction), then the answer is "Yes".  It follows from the definition of NP.  See What is the definition of P, NP, NP-complete and NP-hard? to learn more.
Assuming that $\le_p$ refers to a Cook reduction (also known as a polynomial-time Turing reduction), then the answer is "We don't know for sure, but we think not".

In particular, let $X$ be the problem TAUTOLOGY, and $Y$ be the problem SAT.  Then $X \le_p Y$ (we can transform an instance of TAUTOLOGY to an instance of SAT; if you then flip the answer from an algorithm to solve SAT, the result will be the answer to TAUTOLOGY).  We know that SAT is in NP.  However $X$ is co-NP-complete, so $X$ is not likely to be in NP: if $X$ is in NP, then it follows that NP = co-NP, which would be a surprise.  While we can't prove NP $\ne$ co-NP, many/most complexity theorists expect that NP $\ne$ co-NP is true, and from that it would follow that the answer to your question is "No" -- assuming you are referring to Cook reductions.


To learn more about the difference between these two types of reductions and why both notions exist, take a look at the following questions:


What is the difference between these terms?
Can one show NP-hardness by Turing reductions?
https://cstheory.stackexchange.com/q/138/5038
https://cstheory.stackexchange.com/q/686/5038