But how did humans develop formal systems and the notion of syntactic consequence in the first place? Wouldn't they have had to develop such systems based on what semantic consequences they agreed with?
... and you are entirely correct: As has been pointed out in the comments, the study of semantic consequence lead to the notion of syntactic consequence. The opening lines of George Boole's The Laws of Thought (the title is itself suggestive) are telling:
- The design of the following treatise is to investigate the fundamental laws of those operations of the mind by which reasoning is performed; to give expression to them in the symbolical language of a Calculus, and upon this foundation to establish the science of Logic and construct its method; to make that method itself the basis of a general method for the application of the mathematical doctrine of Probabilities; and, finally, to collect from the various elements of truth brought to view in the course of these inquiries some probable intimations concerning the nature and constitution of the human mind.
The introduction then carries on to briefly discuss the historical development of such an investigation, starting with Aristotle.
Once a system of symbolic logic based on semantic reasoning, i.e. truth-preserving argumentation, has been developed, then that system can be studied in isolation, thus beginning the study of syntactic consequence, where the rules of logical inference become purely mechanical. Put very simply – Leibniz, Babbage and Lovelace were ahead of their time, for instance – the progress was as follows:
- People naturally reason with each other.
- It is noticed that some arguments are valid while others are not.
- Various attempts to analyse point 2 are made.
- Symbolic logic based on semantic reasoning is developed.
- People discover that symbolic logic, aka syntactic reasoning, is interesting in its own right. There's a lot to this stage, but a key stepping stone on the way was the discovery of non-Euclidean geometries. Peano and Pieri were important figures in the early study of syntactic reasoning for its own sake.
- The study of symbolic reasoning leads to modern mathematical logic and also to computability theory (Turing machines and all that).
Symbolic logic is of course crucial to modern logic and set theory, but it is interesting to note that Zermelo came up with his eponymous axioms in 1908, a decade before first-order logic was brought into its current form by Hilbert and Bernays in 1917–1918.
A final note: The development of the study of logic and reasoning is quite similar to that of grammar, which isn't so surprising, considering the connections between the two. An oversimplified account:
- People naturally follow unwritten grammatical rules.*
- People start to analyse these rules, leading to grammar as a field of study.**
- People discover that grammar is interesting in the abstract, eventually leading to formal grammars.***
- People realise that formal grammars are rather useful in practical computing.
*Native speakers speak grammatically without having to study grammar.
**It seems so obvious to us now, but coming up with grammatical categories (nouns, verbs, prepositions, etc.) was a tremendous breakthrough.
***This glosses over a lot of the actual historical motivation, e.g. the idea of a universal grammar.