The following questions may seem very philosophical and I guess that you guys will tell me that this is not the right place for asking them. But for me it is important to get answers from mathematicians and not from philosophers.
Note: The questions are subjective. I am asking for YOUR opinion. So if you tell me your opinion I would be very happy ;-D
Is "5 is not a set" a mathematical statement? I don't want to know, if you think it is a true statement, or a false statement, but I want to know whether you think it is a statement at all. In type theory, one can't express "5 is not a set". However, should a foundation for mathematics be able to express this sentence?
Is "second-order logic" a logic at all? Or is it just "set theory in disguise"?
Do we use the language of higher-order logic in ordinary mathematics? Or are we always working with first-order logic? Comment: Maybe you are going to say that the definition of a topological space is higher-order because we quantify over sets of sets of ... individuals. But that is not what I mean with "using higher-order logic". The example "definition of topological space" can be expressed in set theory which is a first-order theory. Thus with "using higher-order logic" I do not mean quantification over sets, which is a first-order concept, but I mean "quantification over properties".
Is "working in formal systems (like the predicate calculus)" mathematics? That is: Does "proving of logical tautologies" belong to mathematics? Is it a subfield of mathematics? Is there research in this area?
Yes, of course; it is expressible in set theory (like $\mathsf{ZF}$) and set theory, much more than a foundational theory, is a mathematical theory.
The "mathematical part" of mathematical logic is mainly the meta-theory. In terms of mathematical knowledge, a formal derivation in predicate calculus is quite uninteresting (nor more interesting that performing a sum). But Gödel Completeness Theorem for predicate calculus is an outstanding "piece" of mathematics.