Type theories have multiple uses, and with each kind of usage comes a different
notion of correctness. They two key uses are
As a foundation of mathematics. In this context correctness means
primarily that we can't deduce falisity.
As a tool in programming. Here correctness means primarily that that
well-typed programs "don't go wrong" in Milner's famous words, i.e. that they do not
exhibit a certain forms of error, such as trying to execute 3 +
Both notions of correctness are related, but not the same.
Gödel's second incompleteness theorem puts serious restrictions in the way of showing the 'correctness' of type theories as a foundation of mathematics. The best you can hope for is to show 'correctness' (understood as consistency) relative to some other foundation, e.g. by giving a set-theoretic model.
The key thing we worry about with type theories is that a given type-theory is inconsistent because we can define a non-terminating term. Modern type-theories are fairly complicated beasts, and it's quite easy to make them too powerful so that a fix-point combinator
becomes definable. Such fixpoint combinators inhabit every type, making the type-theory inconsistent as a foundation of mathematics. Since fixpoint combinators can be subtle, it is quite easy to overlook how one's typing system allows them to be defined. Indeed, famous foundationalists have a habit of
proposing foundations of mathematics that are unsound for this reason. For example Martin-Löf's original proposal for type-theory made the kind of types itself a type (that approach to typing is now referred to as Type:Type). This is
extremely convenient, and gives you the most general form of impredicative polymorphism. Alas, Girard discovered that this was unsound, when he managed to express the Burali-Forti paradox in Type:Type, see this discussion for more details. Every since, Martin-Löf's type theories have been predicative, but with added inductive definitions to recover (much of) the expressive power of impredicativity.
Encoding a type theory in another foundation such as set theory gives us a fuzzy feeling of security: it says there are unlikely to be an obvious unsoundness bugs in our type-theory. The justification behind this intuition is strictly empirical (!): in the century of since Cantor invented and Zermelo formalised it, nobody has found a soundness bug in conventional set theory. (As an aside, this situation is similar to cryptography where we trust RSA, Diffie-Hellman, AES or 3DES for little other reason than that they have withstood sustained attempts at breaking.)
Note that while a system with Type:Type is wrong as a foundation of
mathematics, it is perfectly acceptable as a typing system for
programming languages, because we can still show that no typeable program goes "wrong".
Regarding proof techniques for correctness, the different properties you mention relate to different notions
of correctness. Termination is the key step to showing correctness
of a type-theory as a foundation of mathematics, while subject
reduction is usually the key step to showing that a type-theory
is usable as a tool in programming. Note that since a termination
proof is the high-road to consistency as a foundation, by
Gödel's second incompleteness theorem, we can prove termination of a type-theory only by using a stronger system.