Farkas' lemma for variables in the natural numbers A lot of questions regarding the Farkas' lemma has already been done here. Most of them seems to be related to consequences of the Farkas' lemma, for example, see [1, 2, 3]. This means that the problem of deciding whether a linear programming is feasible or not is well established. On the other hand, there is a class of similar problems called unbounded knapsack problems, but, at least up to my knowledge $-$ which is modest $-$, it does not seem to have a similar characterization for the feasibility as in linear programming. So... since these problems are still quite interesting by themselves, I wonder,

what is a necessary and sufficient condition for an unbounded knapsack problem to be feasible?

Precisely,

given a matrix $A \in \mathbb{R}^{m \times n}$ and a vector $b \in \mathbb{R}^{m}$, there is a result similar to the theorems of the alternative so that it gives a necessary and sufficient condition to the system
$$\begin{align*}
A x \leq &\  b \\
x \geq &\  0 \\
\end{align*}$$ to have a solution with $x \in \mathbb{Z}^n$?

 A: Your question asks for a certificate for both satisfiability and unsatisfiability. However, since the unbounded knapsack problem is $\mathcal{NP}$-complete, it is unlikely there exists a short certificate for this, otherwise the problem would be in $\mathcal{NP} \cap co\mathcal{NP}$, which is very unlikely.
In fact, if any $\mathcal{NP}$-complete problem belongs to $\mathcal{NP} \cap \text{co}\mathcal{NP}$, then $\mathcal{NP} = \text{co}\mathcal{NP}$, which is equivalent to a collapse to the first level of the polynomial hierarchy. It is a widely believed conjecture that any collapse of the polynomial hierarchy is unlikely, especially to the first level.
It would for example imply that $SAT$ is also in co$\mathcal{NP}$, which means that even if we had to do a long computation to show that no solution exists to a given boolean formulation, we would be able to generate a short proof for it.
In a more general manner, this explains why there is no equivalent of the Farkas Lemma for integer programming, since integer programming is $\mathcal{NP}$-hard
