>>487
もちろんそれらは区別しなければならない。
通常は記号⇒と→を使い分けることにより区別する。すなわち、
p→qはただの論理式であり、p,qの内容によって真にも偽にもなる。
それが恒真である場合は、p⇒qと表す。
これで>>487を書き換えると、次のようになる。
--------
p,qを命題としたとき，含意→と論理積∧を使って
　(p→q)∧(q→p)
と定義される論理演算p←→qを同等（equivalence）という。
このp←→qが恒真命題である場合にはそれを同値（equivalent）といい、
p⇔q と表記する。
--------
「p⇒q」は、シンタクティカルには「pからqが証明可能」あるいは「論理式p→qが証明可能」
のことであり、セマンティカルには「論理式p→qが恒真」ということになる。

ちなみに本によっては、記号→の代わりに⊃が、←→の代わりに≡が、
⇒の代わりに├や→が使われているものもあるので、十分に注意されたし。