The short answer to your question 1 is no, but for perhaps subtle reasons.
First of all, System $F$ and $F_\omega$ cannot express the first-order theory of arithmetic, and even less the consistency of $\mathrm{PA}$.
Secondly, and this is really surprising, $\mathrm{PA}$ can actually prove consistency of both those systems! This is done using the so-called proof-irrelevant model, which interprets types as sets $\in\{\varnothing,\{\bullet\}\}$, where $\bullet$ is some dummy element representing an inhabitant of a non-empty type. Then one can write down simple rules for the operation of $\rightarrow$ and $\forall$ on such types rather easily to get a model for system $F$, in which the type $\forall X.X$ is interpreted by $\varnothing$. One can do a similar thing for $F_\omega$, using a bit more care to interpret higher kinds as finite functions spaces.
There's an apparent paradox here, where $\mathrm{PA}$ can prove consistency of these seemingly powerful systems, but not (as I'll show in a moment) normalization.
The missing ingredient here is realizability. Realizability is a way to make certain programs correspond to certain propositions, typically in arithmetic. I won't go into the details here, but if a program $p$ realizes a proposition $\phi$, written $p\Vdash \phi$, then we have a certain piece of evidence for $\phi$, in particular if $p$ is normalizing, then $p\not\Vdash\bot$. We have:
Theorem: If $\phi$ is a theorem of 2nd order arithmetic $\mathrm{PA}_2$, then there is some closed term $t$ of system $F$ such that $$ t\Vdash\phi$$
This theorem can be proven in $\mathrm{PA}$, and so we have
$$\mathrm{PA}\vdash F\mbox{ is normalizing}\Rightarrow\mbox{$\mathrm{PA}_2$ is consistent} $$
and Gödel's argument applies (and $\mathrm{PA}$ cannot prove normalization of system $F$). It's useful to note that the reverse implication holds as well, so we have an exact characterization of the proof-theoretic power needed to prove normalization of system $F$.
There is a similar story for system $F_\omega$, which, I believe, corresponds to higher arithmetic $\mathrm{PA}_\omega$.
Finally, we have the tricky case of MLTT with inductive types. Here again a somewhat subtle issue arises. Certainly here we can express the consistency of $\mathrm{PA}$, so that isn't an issue, and there is no proof-irrelevant model, as we can prove that the type $\mathrm{Nat}$ has at least 2 elements (an infinite amount of distinct elements, in fact).
However we run into a surprising fact of higher-order intuitionistic theories: $\mathrm{HA}_\omega$, the higher-order version of Heyting Arithmetic is conservative over $\mathrm{HA}$! In particular, we cannot prove consistency of $\mathrm{PA}$, (which is equivalent to that of $\mathrm{HA}$). An intuitive reason for this is that intuitionistic function spaces do not allow you to quantify over arbitrary subset of $\mathbb{N}$, since all definable functions $\mathbb{N}\rightarrow \mathbb{N}$ must be computable.
In particular, I don't think you can prove consistency of $\mathrm{PA}$ if you add only natural numbers to MLTT without universes. I do believe adding either universes or "stronger" inductive types (like ordinal types) will give you enough power though, but I'm afraid I have no reference for this. With universes, the argument seems quite simple though, since you have enough set theory to build a model of $\mathrm{HA}$.
Finally, references for the proof theory of type systems: there's really a gap in the literature here I think, and I would relish a clean treatment of all these subjects (in fact, I dream of writing it myself some day!). In the meantime:
The proof-irrelevant model is explained here by Miquel and Werner, though they do it for the Calculus of Constructions, which complicates matters somewhat.
The realizability argument is sketched in the classic Proofs and Types of Girard, Taylor and Lafont. I think they also sketch the proof-irrelevant model, and a great deal of useful things besides. It's probably the first reference to read.
The conservativity argument of higher-order Heyting arithmetic can be found in the elusive second volume of Constructivism in Mathematics by Troelstra & van Dalen (see here). Both volumes are extremely informative, but quite difficult to read for a novice, IMHO. It also somewhat avoids "modern" type theory subjects, which is unsurprising given the books' age.
An additional question in the comments was about the exact consistency strength/normalization strength of MLTT+Inductives. I don't have a precise answer here, but certainly the answer depends on the number of universes and the nature of the inductive families allowed. Rathjen explores this question in the excellent paper The Strength of some Martin-Lof Type theories.
Wrt normalization, the basic idea is that if, for 2 theories $\cal{T}$ and $\cal{U}$, we have
$$\mathrm{PA}\vdash\mathrm{Con}(\cal{T})\Rightarrow\mathrm{Con}(\cal{U}) $$
then, generally
$$\mathrm{PA}\vdash \mbox{1-$\mathrm{Con}$}(\cal{T})\Rightarrow\mathrm{Norm}(\cal{U}) $$
where 1-$\mathrm{Con}$ is 1-consistency and $\mathrm{Norm}$ is (weak) normalization.
MLTT + the type of natural numbers (and recursion) is a conservative extension of $\mathrm{HA}_\omega$, which is proven in Besson Recursive Models for Constructive Set Theories.
As far as MLTT with induction-recursion or induction-induction, I don't know what the situation is, and AFAIK, the problem of exact consistency strength is still open.
