「ならば」記号の読み方

• ⊃ implies
• |- provable（probableじゃない、注意）
• ⇒（シーケント） entailsかな
• |= valid, satisfies

A |- B に対して、B is provable from A のようになる。|= A も A is valid。A |- B を A proves B と読むとおかしいのかな？ proveする主語はAじゃなくて証明者だから変かもしれない。

意味論的に、「Aが成立するモデルではBも成立する」を A |⇒ B と僕は書くが、|⇒ は「意味論的に帰結する」とか言うようだ、semantic consequence。

- と シーケントの ⇒ は同じ読み方でもいい気がするが、

- は構文論に対するメタな言明で、シーケントは構文論（形式的体系）のなかで使われる記号だから性格は異なる。

演繹定理は、A, B |- C ⇒ A |- B⊃C とかけるが、ここでは ⊃、|-、⇒ が一度に出てくる。ただし、⇒はシーケントじゃなくて「地の文」の「ならば」。

証明図の横棒も「ならば」だと思うが、アレはなんと呼ぶのだろう。

[追記]

• http://math.stackexchange.com/questions/286077/implies-vs-entails-vs-provable
• 伴意は「ばんい」じゃなくて「はんい」と読む - 檜山正幸のキマイラ飼育記
• 論理とはなにか？ - 檜山正幸のキマイラ飼育記
• さまざまな「ならば」達 - 檜山正幸のキマイラ飼育記
• 論理：証明可能性と普遍妥当性 - 檜山正幸のキマイラ飼育記
• 当方記事には過ぎた続編、よみがえる妄想*1 - 檜山正幸のキマイラ飼育記

[/追記]