Why do people separate syntax and semantics in mathematical logic?
This is a rather vague or maybe philosophical question. Basically I want to have a deeper understanding on the motivation of syntax-semantics separation in mathematical logic, since it struck me when I first know people treat mathematical proofs as symbol manipulations purely.
Specifically, there are several aspects that I would like to know about:
Why does viewing proofs purely syntactically helps with mathematical rigour? Examples?
Why do people want a logic language independent of the models it represents?
Why does axiomatic method get more and more emphasised in the history of mathematical development?
I have some vague impressions for the answers of these questions, but I don't know how to elaborate them precisely. Therefore I would like to learn your knowledge and opinions on this topic.
Mikhail Katz and Mauro ALLEGRANZA already gave answers for the historical context but I will try to give an answer focusing on intuition.
Why does viewing proofs purely syntactically helps with mathematical rigour? Examples?
To be rigourous we need to follow a set of rules without objection (in order to create a consensus between people) and syntactical objects provide an adequate form of objectivity (as pure syntax is impartial, not "engaged").
Without consensus in the choice of a formal language/syntax how can one can convince someone about something ?
Why do people want a logic language independent of the models it represents?
I don't think people wanted that. That choice was mainly influenced by Frege philosophical ideas and the popular conception of Logic. In the early days of modern Logic we wanted to study logic as an object so we just put it in the form of a formal object.
When we study logic as an object we sometimes use logic itself to prove properties about it. Since it doesn't make sense we divided the world in two parts :
- the object language (logic as an object with a formal language)
- the meta language (above the object language, our intuition about logic, what we use to prove things about formal logic, something we don't need to explain).
The syntax lives in the object language and the semantic (giving a meaning to the syntax) lives in the "meta-level". Providing a set of logical rules, one often want to prove Soundness and Completeness to ensure that the syntax follows the semantic representing our intuition (and prejudices) of logic.
That distinction is not something we wanted on purpose. We did that because of our beliefs and (mis)conception of logic.
Why does axiomatic method get more and more emphasised in the history of mathematical development?
I don't know much about the axiomatic method but a lot of problems arised from it because we didn't know if something we couldn't prove should be taken as an axiom and we didn't know which axiom to choose : the status of axioms was not clear.
In the beginning of the 20th century, Poincaré suggested to not see axioms as "obvious facts" but as "definitions", a quite satisfying answer.
A lot of mathematical theory are now founded on the axiomatic method in a satisfying and productive way.
Finally, note that the distinction between syntax and semantics is not necessary.
Intuitionistic logic provide an interpretation of logical proofs in term of constructions/programs through the Curry-Howard isomorphism. For instance the implication $A \rightarrow B$ is not interpreted in a semantical world but seen as a functional program producing a proof of $B$ from a proof of $A$.
Recent works on Linear Logic, Ludics, the Geometry of Interaction give an interpretation of logic through the idea of "interaction" with the cut rule elimination procedure as the core. These works try to free logic from external explainations and try to find the meaning of logical rules in the rules themselves.
The distinction you mentioned between language and models is crucial to understanding model theory. Already in the 1920s and 1930s it was clearly understood that Peano arithmetic does not uniquely characterize the natural numbers. Notably in 1933 Skolem constructed exotic models of the "natural numbers" in ZF (Zermelo-Fraenkel set theory without the axiom of choice). Similarly the distinction is crucial to understanding Lowenheim-Skolem phenomema. To mention another example close to my interests, one can show that the existence of a strictly positive function with zero Lebesgue integral is consistent with ZF. Such a claim is probably incomprehensible if one thinks of sets as being "out there" in a literal realist sense, a viewpoint challenged by the syntactic/semantic distinction.
Some mathematicians find such dualities troubling on philosophical grounds and reject them. Thus, Paul Halmos adhered to the view that mathematics is one splendid architecture and sought to reformulate logic in a way that would not involve the aforementioned duality; for details see this article.