What is the exact role of logic in the foundations of mathematics?

Question

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?

Answer 1

Many students, myself, some years ago, included, are often confused about the aim of logic. It is certainly not the aim of logic to somehow provide a rigorous framework to do all of mathematics in a somehow pure manner, without invoking any form of intuition or axiomatisation. In particular, it is not the aim of logic to define the meaning of such phrases as for all or there exists at any level other than the intuitive obvious one. It is simply of little interest to do so (that is actually a big fat lie, as there are various flavours of logic in which the meaning of, e.g., there exists is defined differently to the classical one, and some mathematicians object to the classical definition, for many plausible reasons - such issues obivously fall under the umberla of foundations, since it is a study of different variants at a very low level, the very basic building blocks of all arguments).

So, what is logic about then? Well, logic comprises of several fields, so let's just look at one: model theory. Model theory can be described, somewhat, as the study of the expressive power of formal languages. For a long time, mathematicians debated the correctness of certain objects subjectively. Axioms were treated as evident truths, indicating they are indisputably true. Famously, Euclid's fifth postulate in geometry was debated, and argued by many to be an evident axiom of geometry, while literally walking on a counter example. Development in analysis and other realms dictated a much more intricate understanding of the role of axioms, definitions, and the structure of proof. The old axiomatic, platonistic, approach was replaced by a formalism approach: the axioms are just sentences chosen to hold, rather than somehow being externally obvious, and the practice of mathematics is the study of that which flows from the axioms. Of course, when Hilbert said that mathematics is just a formal game, he (I presume) did not mean that when we actually do mathematics, we just randomly choose some axioms, and see what happens. That would be futile. Instead, the formality is there, practiced informally by human beings. However, it cannot be disputed that it is a formal game, and that formal aspect can be studied. So, along comes model theory: a formal definition of language, predicates, statements, etc., together with its semantics. This sets the ground to study the relationship between the language we use in order to study something, and the actual properties of that something. Few things are more foundations than the understanding of the strengths and limitations of the language we use in our quest to understand mathematical objects.

Goedel's completeness and incompleteness theorems are remarkable examples of amazing answers to such foundational questions as the following. If I found a proof of a property from some axioms, does it mean that the property holds in any model of the axioms? (Answer: yes, by a simple proof by induction following the definitions of the semantics). If a property is true (semantics!) in every model of some axioms, does it follow that there exists a proof (a syntactic thing!) of the property from the axioms? (Answer: Yes, this is the completeness theorem). Given a model of interest, is it possible to capture its semantics (i.e., to capture precisely all of the statements that hold for it) as precisely those theorems provable from a regonisable set of axioms? (Answer: depending on the language, but if the model is interesting enough, and the language is rich enough, then the answer is no (the incompleteness theorem)).

I will stop here, though there is much more to say. Perhaps the discussion can continue in the comments, if you have further questions.

Answer 2

I think that the problem lies in the multiple meaning the word logic assume in mathematics and more generally in deductive sciences.

If I understood correctly, I believe that you are right on the first point.

If by logic you mean a formal system of inference rules (for instance first order logic) then mathematics, as any other deductive science, is founded on such logic because it needs these inference rules to prove mathematical statements (i.e. theorems).

To be fairy specific one needs the syntactic part of logic: a description of what are formulas and what are the operations/inference rules for deriving theorems. The semantics is not foundamental for the purpose of foundations (at least in my opinion), except for a psychological reason: as an intuitive motivation for justifying the validity of the inference rules.

On the second point, if by true you mean the intuitive concept then I think you are right again. Mathematics cannot tell what it means for a statement to be true in the intuitive way, that kind of problems belong to the philosophy ... I think.

On the other hand (and this address point three in your question) mathematics allows to provide a formal concept of truth, which basically is a neat trick that allows to reduce proof of properties of some kind of objects (structures like groups, topological spaces, etc) to theorems in some meta-theory. This is what model theory basically is all about and the usefulness of its results are the reason why we need also a formal definition of the semantics of first order logic (inside set-theory).

Hope this helps, if not feel free to ask for any details or specifications.