>>505
> A|-B
>
> この記号なんだかわかってませんよね

君自身が分かってないんじゃないの？ それはentailmentだよ

そしてHerbrandの演繹定理の最も簡単な形は　A |- B　⇒　|- A→B だ（普通は複数の前提を並べた形だがね）
君、理解できてる？

それとも “|-” はLKでのderivabilityの記号だとでも言いたかったのかな？
だったら>>479はきちんとそう書くべきだね
この記号 “|-” はもっと一般的なentailmentの記号として定着しているのだから

それにLKならば導出されるのはsequentであってformulaではない
だから |- をderivabilityの記号としてLKで使って |- A→B と書くのは有り得ない（完全な間違い）
LKでderivabilityを主張するのならば |- ―→　A→B と書かねばならない（“―→”はもちろんLKのsequentの左辺と右辺とを分ける記号で通常は長い矢印で書かれるもの）

まさか>>479での |- はLKでの“―→”のつもりで書いてたなんて非常識なことを主張する気じゃないよね

>>505の何も分かってない君、君はもう少し命題論理や述語論理の基本、特にNK, sequent形式によるNK, LKなどやderivability, entailmentの基本をきちんと勉強すべきだね、もちろんHerbrandの演繹定理も含めてね