Precise relation between complexity classes(focus on P, NP and EXPTIME) I am interested in the precise relation between $P$, $NP$ and $EXPTIME$ classes.

What I know so far: 


$P \subseteq EXP$ (from Time Hierarchy Theorem [1])
We don't know an exact relation between $P$ and $NP$, and between $NP$ and $EXPTIME$. What do we know:

2.1 $\forall problem \in P \Rightarrow problem \in NP$ (Any problem in $P$ is in $NP$.)

2.2 $\forall problem \in P \Rightarrow problem \in EXPTIME$ (Any problem in $P$ is in $EXPTIME$.)
In $P$ vs $NP$:

3.1 We haven't found an $ NP $ $complete$  $problem $ that we can solve in polynomial time (this would imply $P = NP$)

3.2 We haven't found a proof that states that we can't find an polynomial (running time) algorithm for an $NP$ $complete$ $problem$ (this would imply $P \neq NP$)

3.3 From 3.1 and 3.2 we can't state anything about the cardinality of $NP-P$. Most of scientists belive that $P \neq NP$ so there are $NP$ problems that we can't solve in polynomial time.


First, if you find and "hole" in what is stated above, please correct me.

Now for my questions:

A. What can we say about $NP$ vs $EXPTIME$? Are there $EXPTIME$ $complete$ problems not in $NP$? For me it sounds like the $P$ vs $NP$ problem just one "level" (in the hierarchy) higher.

B. How does one go about finding a proof like in 3.2? Obviously we haven't found such a proof but I am looking to understand. The first idea that comes to mind is to go with a proof by contradiction. Not finding such a proof doesn't say much (maybe we are not "smart" enough). What else could we try? The problem reduces, in my opinion, to proving that an algorithm in "elegant" (in running time; that means that it is "the fastests")

Kind of bonus question:

C. How does this relate to Godel's incompleteness theorem? Maybe the better question (quite outside of the scope of the original question) is how much of the math we use on answering these questions can be considered a formal system(so we can apply Godel's result)? What parts are not "formal"?

D. I wasn't able (yet) to look very far into [1]. If possible, can someone give me an informal insight on how it handles defining a strict lower (time) bound for a certain problem? 

[1]https://en.wikipedia.org/wiki/Time_hierarchy_theorem
The Wikipedia page on EXPTIME summarizes all the known relationships:


$\mathsf{P} \subseteq \mathsf{NP} \subseteq \mathsf{EXPTIME}$.
$\mathsf{P} \subsetneq \mathsf{EXPTIME}$ due to the time hierarchy theorem.


You can find more information on the time hierarchy theorem in Wikipedia, in textbooks, and in online lecture notes. It is a very standard topic.

The P vs NP question is about the first two levels of the polynomial hierarchy. It is conjectured that all levels are distinct and different from $\mathsf{PSPACE}$, which is an upper bound on the hierarchy; and that $\mathsf{PSPACE}$ is distinct from $\mathsf{EXPTIME}$ (it is known that $\mathsf{PSPACE} \subseteq \mathsf{EXPTIME}$).

The proof of the time hierarchy theorem uses diagonalization in a straightforward manner (at least conceptually), and in this regard it is part of a line of results that includes Gödel's (first) incompleteness theorem and Turing's undecidability of the halting problem. In fact, it is a time-bounded version of the latter.

Finally, while some people have some ideas on how to prove $\mathsf{P} \neq \mathsf{NP}$, we mostly know a few general methods which cannot prove $\mathsf{P} = \mathsf{NP}$. These are known as barriers, and include diagonalization (used to prove the time hierarchy theorem), natural proofs (used to prove lower bounds in circuit complexity), and arithmetization (used to prove $\mathsf{IP}=\mathsf{PSPACE}$). The Wikipedia article about the P vs NP problem has a nice summary about these barriers.