Natural Deduction Proof for Modus Tollens

1. No. You have $P$ come out of nowhere.
2. It's not clear to me what the distinction between "assumption" and "premise" you're making here or how you're defining each. (The impression I get is that you're doing the opposite of what I would do, which is fine, but means you can't assume everyone defines things the same way as you.)
3. Proof systems don't talk about semantics. There is only derivable. A theorem is a formula, $\varphi$, for which $\vdash\varphi$ is derivable. Sometimes the term "conditional theorem" is used for the more general case for $\Gamma\vdash\varphi$ being derivable.
4. Yes, they'd lead to very different proofs and are very different statements.

As you seem to recognize, there's a distinction between statements in the meta-logic and formulas in the logic. However, you seem to think this is some kind of special bookkeeping we do to avoid contradictions that we could just ignore if we wanted to throw caution to the wind. This is not the case. Not distinguishing between the object language and the meta-language is to not even know what you're saying. Most of the time it just leads to completely nonsensical statements, other times ambiguity of what is actually intended. Here are some simple natural language examples of similar kinds of confusions:

1. "The dog" consists of seven characters.
2. The dog consists of seven characters.
3. "The text" consists of eight characters.
4. The text consists of eight characters.

1 makes sense. 2 makes no sense at all. 3 and 4 both make sense but mean quite different things. These examples illustrate the use-mention distinction. You can easily see how being sloppy about it can lead to incorrect arguments, e.g. "A: I only like short books." "B: You'll like this book. 'This book' only has nine characters." This distinction is quite similar to what's happening in formal logic. A formula is like a quoted piece of text. It's a piece of data. We can ask questions like "how many symbols are in it" and analyze its structure. It has no more of a truth value than $3$ does (indeed, when working in very weak foundations, the formulas may literally be encoded as numbers). A connective like $\to$ is a way of sticking to formulas together to make a bigger formula. It's an operation on formulas just like addition is an operation on numbers. $\vdash$ is a meta-logical predicate, $\vdash\varphi$ is the claim that the formula $\varphi$ is derivable. $\vdash\varphi$ is not a piece of data but a statement being made that may be true or false.

More generally, $\vdash$ is a binary (meta-logical) predicate written infix whose first argument is a list of formulas and whose second argument is a formula. The comma in $\varphi,\psi\vdash\chi$ is not some weird alternative to $\land$ and $\varphi,\psi$ is not a formula. Instead the comma indicates prepending to a list. Sometimes we explicitly write the empty list as, say, $\cdot$, and being more systematic we should write $\cdot,\varphi,\psi\vdash\chi$ which would be parsed as $((\cdot,\varphi),\psi)\vdash\chi$. Often, the notation is overloaded so that it also stands for list concatenation. Again, formulas are just pieces of data and a list of formulas is just a more elaborate piece of data. $\varphi,\psi\vdash\chi$ is the claim that the predicate $\vdash$ holds of the two element list containing the formulas $\varphi$ and $\psi$, and the formula $\chi$. $\varphi\land\psi\vdash\chi$ is the claim that the predicate $\vdash$ holds of the one element list containing the formula $\varphi\land\psi$, and the formula $\chi$. There is no a priori reason for these claims to be equivalent. For typical proof systems, we can prove (meta-logically) that they are equivalent, but in other proof systems it may well not be true and regardless it does take a proof to show this.

To make the analogy to numbers again, consider the binary predicate that takes a list of numbers and a number call it $R$. Define $R$ to be true when the length of the first argument equals the second argument, e.g. $R(\langle 2,3\rangle,2)$ holds but $R(\langle 2,3\rangle,3)$ does not. It's obviously not the case that $R(\langle x,y\rangle,z)$ is equivalent to $R(\langle x+y\rangle, z)$. If $R$ was, on the other hand, the relation that states that the sum of the first argument equals the second argument, then $R(\langle x,y\rangle,z)$ would be equivalent to $R(\langle x+y\rangle, z)$ though you'd still have to prove it.

It's probably worth stating what (meta-logical) predicate $\vdash$ actually is. For a natural deduction system like the one you're using, $\Gamma\vdash\varphi$ means that there exists a complete (or closed) derivation of $\varphi$ assuming we have derivations for each of the formulas in $\Gamma$. As your derivation indicates, a derivation is a tree-like structure. It is itself another piece of data hence being able to do things like induction over derivations or calculating the height of a derivation. To show that $\Gamma\vdash\varphi$ holds, you produce a derivation, i.e. one of these tree-like structures.

There's a somewhat different way of arranging things (which I prefer) so that $\Gamma\vdash\varphi$ is itself another piece of data, called a sequent, rather than a meta-logical claim, and we'd write the claim as $\dfrac{}{\Gamma\vdash\varphi}$. We now talk of deriving sequents rather than formulas. This does not mean a sequent is a formula. A sequent is a different type of data that contains formulas. This is like how a vector might be represented as a tuple of numbers but is not itself a number. The benefit of this latter approach is that it makes the management of assumptions something that is explicitly modeled allowing us to explain it more precisely or consider alternatives such as substructural logics. The drawback is that now we have to do that modeling rather than effectively getting it for free from the meta-logic.

1. Is my NK proof above correct?

Somewhat.

• First, you have unnecessarily conjoined your two premises: $P\to Q$ is one premise, and $\lnot Q$ is another.
• Second, you have not distinguished between the premises and the assumption of $P$, nor indicated when that assumption was discharged.   One way is to use brackets and indices, as below, to track which rule discharges which assumption.
• Third, the rule to discharge the assumption is negation introduction, and not contradiction elimination (more usually known as ex falso quodlibet, or "explosion").   The latter is not a rule of discharge; it is a derivation within the context.

$$\begin{split}&\dfrac{\dfrac{\dfrac{[P]^1\quad P\to Q}{Q}{\to\!\mathsf E}\quad\lower{1.5ex}{\lnot Q}}{\bot}{\lnot\mathsf E}}{\lnot P}{\lnot\mathsf I^1}\\[2ex]\hdashline\blacksquare &\quad P\to Q, \lnot Q\vdash \lnot P\end{split}$$

2. As I understand it, in this proof the only assumption I make is $P$...

Technically $P$, $P\to Q$, and $\lnot Q$ are all assumptions.   Premises are undischarged assumptions.   But yes, $P$ is the only assumption you need to raise and discharge.

3. How to differentiate between theorem and true proposition in NK proof system?

A theorem is a tautology: an unconditionally true statement.   Since the classical logic natural deduction system (NK) is a complete, therefore every theorem can be derived unconditionally: that is, if $\phi$ is a theorem, then $\vdash \phi$.   Conversely, since NK is sound, therefore if $\phi$ is unconditionally derivable, then $\phi$ is a theorem.

4. Lastly, is NK proof for $P →Q, ¬Q ⊢¬P$ is the same as NK proof for $⊢(P →Q)∧¬Q →¬P$.

No, they are considered different claims, and they have distinct proof structures, although one may be inferred from the other.