At high school and in the beginning of my university studies, I used to believe the following "equation":
Foundations of mathematics = Logic + Set Theory
Of course, this "equation" does not hold absolutely, the most notorious example being category theory. However, examples like this usually question the second term of the "right hand side" only. At least to my knowledge, almost nobody seems to challenge the thesis that logic indeed forms one of the foundations of mathematics.
However, my belief in this thesis has been shattered when I encountered the usual "definition" of semantics of first-order predicate logic. This definition is formulated in meta-language – for instance, the semantics of the universal quantifier is defined like that $\forall x P(x)$ is true iff $P(x)$ is true for all $x$. Obviously, this can never be formalized, as any attempt for a formal definition would require already defined semantics of higher order logic, and so on. So the "definition" of first-order semantics is stated utterly on the intuitive level. Nobody usually bothers to explain why this is OK.
I have become slightly more comfortable with this after reading comments to this question addressing the issue. It seems that it simply is not the aim of logic to make these matters formal. On the other hand, logic simply studies formal reasoning "from above", sometimes using slightly informal definitions or arguments (as in any other part of mathematics).
However, there are several important points that I am not comfortable with so far:
- Logic is usually said to be a foundation of mathematics because it makes mathematical reasoning formal. However, as demonstrated above, some parts of logic are highly informal themselves. Is it possible that the real foundation of mathematics is not logic as a whole, but only formal systems that are studied by logic (e.g., predicate logics viewed as collections of axioms and inference rules, etc.)?
- Is it true that in higher level mathematics, it can only be formally established that a given statement is provable, but saying that a statement is true requires a resort to intuition (because of the above reasons)?
- Why does one even speak about the definition of first-order semantics? Would not it be more precise to speak about its description or something similar? In a field such formal and low-level like logic, I find this a bit disturbing and confusing.
Are my views correct, or am I completely wrong?