The defining property of problems in NP [duplicate]

Question

I'm coming to Computer Science from Mathematics and am familiar with the idea of building classes of objects using Propositional Logic. Namely, start with some universe of objects, define some proposition $P \left( x \right)$, and then iterate over the universe of objects, applying $P \left( x \right)$ to each; keep the objects for which $P \left( x \right)$ is true; exclude each object for which $P \left( x \right)$ is false.

So, when we define a class of objects called $\mathbb{NP}$ (as in P vs NP), I really need to see a formal definition of the proposition used to build that class--as well as a formal definition of the universe of objects we're starting with.

Defining the Universe of Discourse, $\mathbb{U}$

My understanding is that, for the question of $\mathbb{P}$ vs $\mathbb{NP}$, our universe of discourse is all decision problems that are satisfiable. Namely, problems that can be implemented in boolean logic, return a boolean result, and that someone somewhere at some point has found a finite sequence of inputs that cause the implementation to return $TRUE$.

In spite of Russell's Paradox, let us define our universe of discourse as the set $\mathbb{U}$.

Defining $\mathbb{NP}$

$\mathbb{NP}$ is a subset of $\mathbb{U}$. Namely, it is the set of all objects in $\mathbb{U}$ for which the following proposition returns $TRUE$:

This object can be written as a decision problem that returns a boolean value, that decision problem can take any amount of time to resolve, and--as long as the decision problem resolves--given a sequence of inputs that cause the decision problem to resolve to $TRUE$, we can verify the correctness of that resolution in polynomial time.

So, in defining $\mathbb{NP}$, we are really applying our class-defining proposition $P \left( x \right)$ to objects that are compositions of four other objects: namely, a decision problem, a sequence of inputs, an output, and an algorithm for verifying the output is indeed determined by the inputs.

Furthermore, the only object in that composition whose run time we care about is the verifier: the decision problem can run in any amount of time--so long as it resolves. But the verifier needs to return in polynomial time, $O \left( n^{ O \left( 1 \right) } \right)$.

Furthermore, the $\mathbb{N}$ in $\mathbb{NP}$ stands for "nondeterministic". That word is meant to describe the following, further clause in our proposition for defining $\mathbb{NP}$:

If we are given no known solution to the decision problem being examined, we should be able in polynomial time to do the following:

1. Randomly choose values from the decision problem's input space.
2. Plug those values into the verifier.
3. Repeat until we find a sequence of inputs that both satisfy the decision problem and cause the verifier to return $TRUE$.

Is my understanding of the proposition used to define $\mathbb{NP}$ correct?