Of course in Mathematics we have always been quite formalism-free, quite glad to jump from “First Order” to “Second Order” logic without missing a heartbeat, quite glad to dwell in Semantics as our home-base, quite glad to regard the insistence of some logicians on first order formalizations with a little of the same puzzled horror we normally reserve for items like a 19th century corset. Some logicians have actually dug hard into the mathematical (and logical, and philosophical) root of this phenomenon: there are solid intrinsic reasons why we can do away with syntax most of the time. Mathematical logic (especially in the neighborhood of second order model theory, its sister set theory and the formalism-freeness aware abstract elementary classes) has long been able to account for those phenomena.
Excessive insistence on syntax normally seems to be the hallmark of pedantic philosophers, or of computer scientists. Mathematical logicians (especially Model Theorists) usually try to stress the “mathematical” and deemphasize the “logician” in them – often for good reasons, sometimes with a bit of envy of the rest of mathematicians too evident perhaps.
In Gödel’s 1946 paper (for the Bicentennial at Princeton), as Juliette Kennedy has remarked, a framework for breaking syntax is set up, a framework that can be seen to oddly combine the insight obtained from Turing (that helped unify the many previously logic-dependent or syntax-dependent notions of computability due to Gödel, Church and others) with the quest for new axioms for mathematics. Lately (cf. Kennedy’s Dublin lecture) these breaks of syntax have been realized in several domains: (1) the development of “transdefinability hierarchies” (Kennedy, Magidor, Väänänen) where the idea of iterating the construction of L by Gödel is transferred to other logics [and apparently for logics with the cofinality quantifier a robust definition is obtained] – the structures obtained are now called C*(L) where L is a logic and some of them exhibit interesting behavior, (2) the development of “symbiotic” notions between set theory and second-order logic (symbioses can be seen as extremely rich adjoint pairs) capturing compactness, amalgamation, Löwenheim-Skolem phenomena and much more (Väänänen), (3) the development of Model Theory in a very syntax-free manner through abstract elementary classes (Shelah opened that door, several people went in [not en masse] and have done hard work in extending Classification and Stability Theory in a way that reveal structural features not depending on first order syntax), extracting structure way beyond the pale of first order logic yet with a robust classification theory, allowing other kind of symbioses with both set theory (large cardinals, forcing) and geometry (sheaves, accessible categories) – albeit with a firm connection to syntax and even first order through the Presentation Theorem – aecs are really versions of projective classes, and this fact underlies much of the strength of this generalization, in spite of its strong freedom from syntax; and (4) a blend of some of the previous with sheaves (this builds on earlier work of Macintyre and of Grothendieck himself, and through several stages has distilled several semantic/syntactic “blends” and limits – Caicedo’s “sheaf-generic models” (a version of ultraproducts, aware of topology, encompassing usual set-theoretic generic models) an important step in this distilling process – more recently, metric versions and awareness of group actions on the sheaves (joint work with colleagues and students in Bogotá: Padilla, Ochoa) and Zilber’s very recent “Weyl sheaf” – lifting classical semantics/syntax through five stages of generalization of the classical “algebra/geometry” duality (quotients of polynomial rings by ideals/algebraic varieties with Zariski topology all the way through C*-algebras/Zariski geometries) onto the Weyl sheaves.