"Correctness" of type theory How to "proof"  that type theory is correct? Or at least explain that it's meaningful in some sense. In what extent is this a mathematical question and in what is a philosophical one?

When type theories are introduced for example in Luo's book, the following properties are proved:


Subject reduction
Reduction termination
Church-Rosser property


As far as I understand, what these properties describe is that we have a decidable type checking, and that the language of type theory is meaningful in some sense, but nothing more than this.

I asked a question on violation of strict positivity for inductive types (Example of where violation of strict positivity condition in inductive types leads to inconsistency) and in the answer I was told that non strictly positive types might lead to non existence of set theoretic model. Why we need type theoretic model here? And what it gives to us?
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 +
"hello".


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&ouml;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&ouml;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&ouml;del's second incompleteness theorem, we can prove termination of a type-theory only by using a stronger system.