The basic logic course in school gives the impression that logic has both the syntax and the semantics aspects. Recently, I wonder whether the syntax part still plays an essential role in the current studies. Below are some of my observations, I hope the idea from the community can make them more complete.


Model theory: Even though model theory is stated in the language of logic, it can be viewed as the study of local isomorphism (see Poizat's "A course in Model Theory"). The syntax part is therefore a natural (though might be uncomfortable for some) way to view the theory rather than a necessity.


Recursion theory: The object of study is the notion of computability in different context. If we believe in Church-Turing Thesis, then these concept are independent of the formalism chosen. 


Set theory: The intimate relationship between large cardinal and determinacy perhaps can suggest that this is a universal phenomenon. Will this phenomenon disappear if we change the language of mathematics to, for example, category theory?


Proof theory: I know too little to say anything.


If the observation is true, is it justified to demand that Turing degrees, and large cardinals receive the same mathematical status as, for example, prime numbers?



How much of the current logic is about syntax?
I think your observation is a very good one, but this phenomenon is limited to classical logic and does not continue to hold when we move to intuitionistic or substructural logics.


One way of understanding the role of syntax is to take the connectives of logic as explaining what counts as a legitimate proof of that proposition. So a conjunction $A \land B$ can be proven with a proof of $A$ and a proof of $B$, and an implication $A \implies B$ can be can be proven with a proof of $B$, assuming a hypothetical proof of $A$, and so on. Conversely, we also give rules explaining how to use true propositions -- e.g., from $A \land B$, we can re-derive $A$, and we can also rederive $B$. 


If you work this out formally, you get Gentzen's system of natural deduction. The natural deduction systems for good logics admit a normal form theorem for proofs. The normalization procedure also gives us an equivalence relation on proofs (two proofs are equivalent if they have the same normal form), and it so happens that for classical logic, all proofs are equivalent. (This is a small lie: we can give more refined accounts of equivalence of classical proofs which don't equate everything, but the right answer here is still not entirely settled....)


The equivalence of proofs means that we can take the view that the meaning of a classical proposition is its truth value -- i.e., its provability -- and so algebraic models of classical logic contain all the information contained in a classical proposition. We don't need the proofs, and so syntax takes a secondary role. 


But in intuitionistic and substructural logics like linear logic, not all proofs are equated. This means that we can't take the view that all the relevant information about a proposition is contained in its truth value, and so syntax retains a more important role.


