形式論と意味論

⊨
主に意味論的な帰結関係に使われる。
「Γ ⊨ φ」と書いて「Γの全ての論理式が真であるなら、論理式φが真である」を意味する。
「M ⊨ Γ」と書いて「(事前に定まっている理論の)モデルMにおいて、Γに属する論理式がすべて真である」を意味する。
「⊨ φ」と書いて「(事前に定まっている理論の)任意のモデルにおいて、論理式φが真である」を意味する。

⊢
主に形式的な帰結関係に使われる。「Γ ⊢ φ」と書いて、論理式の集合(または多重集合)Γから、形式的に論理式φが推論できることを表す。
Wikipedia

公理系の話に近いような。
⊨
は
「ある公理系Xとして解釈できるモデルにおいては、その公理系Xから演繹できた定理xは常に真となる」

公理主義と無定義用語へのフワッとした感想

数学を学んでいると、数学は認識世界の話であり現実の話をしているのではないと、深く理解できます。当たり前と言えば当たり前なんですが、人の性質はそれを忘れさせます。僕の興味の範囲が徐々に絞られていくのを感じ、またそれは証明の手続きや概念の創造...

可換群の公理を自然数の加法は満たします。ただ、それだけだと1+1=2の意味は与えられません。

可換群の形式を満たすということと、それに一般的な「増える」という解釈=性質を見出すことを切り離して考える為だと思います。

⊨は公理系から導かれた論理構造に意味が与えられた世界の記号。

可換群の定理を自然数の加法というモデルで解釈するのと、可換群を満たす自然数の乗法というモデルで解釈するのとでは、同じ論理構造であっても与えられる意味が異なります。

結合法則:∗(∗)=(∗)∗
単位元の存在:∃1;∗1=1∗=
逆元の存在:
∀,∃−1;
∗−1=−1∗=1
交換法則:
∗=∗

加法的に記せば

結合法則:
+(+)=(+)+
零元の存在:
∃0;+0=0+=
マイナス元の存在:
∀,∃−;+(−)=(−)+=0
交換法則:
+=+

Wikipedia

同じ公理を満たす自然数の加法と乗法であっても、*には×または+と二通りの解釈（性質）が与えられます。零元にも乗法なら1、加法ならと0いう解釈が与えられます。

⊢
は公理系から演繹された論理式ですよ。ただそれだけですよ。ということだと思います。そこに意味はなく構造的にそうであるだけ。

形式論は構文の意味ではなく、抽象的な文の構造の変化を追いかける目的が与えられているのでしょう。
命題論理は命題の意味ではなく論理的な構造がどう変化するのかのみを追いかけます。

「偶数であり奇数である」という文を抽象化し構造だけを抜き出せば、A∧¬Aという、命題の構造自体の性質を考えられます。
「偶数であり奇数であるとは何か？」という具体的な議論には立ち入らず、「AでありAではない」という構文はそもそも論理的に成立するのか、という風なことを考えることが形式論なのだと思います。
前者の場合は「それはどんな数だろうか」を考えることとなり、論理的には結論は出ません。後者の場合は単純に「矛盾」を導き構文そのものが論理的には成立しないことを結論できます。