>そもそもsyntaxが或る程度定義されてなければ
>semanticsも考えようがないからね

正にそこだよ。そもそも syntax というのは
何が well formed formula なのかを決める、つまり言語を定めるもの。
言語学でもプログラム言語の理論でもそういう使い方をされる
（以下「狭義の構文論」と呼ぶ）。

公理とか証明可能性とか（便宜上、以下「証明可能性論」と呼ぶ）
までを構文論 syntax に入れてしまうのは論理学界隈だけの変な習慣だと思う。
プログラミング言語の公理的意味論との類似が強い。

意味論に必須なのは狭義の構文論だけであって証明可能性論は必要ない。
坪井先生などモデル理論の人の書いたのを見るとそういう立場で書かれている。

狭義の構文論の上に（それぞれ独立に）構築される
モデル（意味）論と証明可能性論の関係を述べるのが完全性定理。

一方、不完全性定理は証明可能性論の定理なので
広義の構文論（狭義の構文論＋証明可能性論）だけで記述できる。

この意味でも、構文論と意味論の対立で説明するのは不適切だと思う。