Consider a statement like, "If London is in France, then London is in Asia."
AIUI, in classical/proportional logic, this is "true" because the antecedent is false. This (tenously) makes sense to me, along with the fact that $ P \rightarrow Q \Leftrightarrow ¬P \vee Q $. I'm not asking why vacuous truths are considered true, since there's endless discussion of that already.
However, the statement I opened with is clearly unsound, even if it is true. It would be incorrect, even in the context of a hypothetical/"possible world"/etc, to infer London actually being in Asia from it being in France. You cannot apply modus tollens and actually get $\{ P, (P \rightarrow Q) \} \rightarrow Q$ despite the conditional being true.
My problem with this is that my understanding of the "formal" part of formal theory is that we can do logical manipulations regardless of the specific content of the statement, as long as they have the correct forms. $\{P, (P \rightarrow Q)\} \rightarrow Q$ should always work, regardless of the specific content of the statements $P$ and $Q$. However, clearly, this doesn't work in this case.
I (think I) understand the distinction between syntatic inferences and semantic consequence, so I understand that just because $P \rightarrow Q$ doesn't mean that $P \Rightarrow Q$, but in that (this) case, why do we treat syntatic manipulations as "inferring" anything at all? Or is my understanding of formalism somehow incorrect?
IOW, what is the meaning of $\rightarrow$ as an "implication" - even in a syntatic, formalist, single-model sense - if we cannot always apply modus tollens to the result?