How does (non)deterministic time relate to verifiability? So far, from all the research I've done, I've come across 2 different ways that NP time is explained. One is that a nondeterministic turing machine is able to solve the problem in polynomial time. It seems like this is the exact same as being able to verify that a result is correct in polynomial time, but not necessarily solve the problem in polynomial time. Both these ideas make sense, but these ideas seem very different to me. One is talking about solvability of a problem in a nondeterministic context while the other is talking about solvability vs. verifiability. Can you please intuitively explain why they're related, and if this relationship between solvability, verifiability, determinism, nondeterminism applies to harder complexity classes such as EXP vs NEXP?
Here's some intuition for the equivalence proof

$(\implies)$: Suppose we have a non-deterministic Turing Machine $M$ that solves a problem $P$ in polynomial time. When we run $M$ on some accepted input $x$, we make a bunch of decisions non-deterministically, essentially choosing an execution path. If we record each of those choices, this gives is a string with is polynomial in the size of $x$ (since we know $M$ runs in non-deterministic polynomial time). Then the trace of running $M$ on $x$, with each decision point, is a certificate for $x$. We can follow the steps again and check that any string represents a valid run on $M$, and see whether it ends in a YES or NO state.

$(\impliedby)$: Suppose we have a verifier which takes a string $c$ and input $x$ and checks if $c$ is a valid certificate that $x$ is accepted by problem $P$, where  $|c| \leq |x|^k$ for some fixed $k$. Then we can make an NTM which looks at any $x$ and determines whether it is in $P$ by "guessing" non-deterministically guessing a certifier $c$ of length less than $|x|^k$ and running the verifier on that.

EDIT: to apply this to $EXP$ and $NEXP$, just replace the word polynomial with exponential and change the bound on $c$, and the rest should still work. It doesn't really apply to classes like $PSPACE$, since it's not defined in terms of non-deterministic machines. Not being able to make these kinds of guesses are what makes PSPACE harder (as far as we know) than NP.