代入原理と対称律と推移律

代入原理と同値関係

代入原理: 対象 a, b が a = b であるときには、一つの自由変数 x を含むどんな命題関数 P(x) についても P(a) ⇔ P(b) が（両辺ともに一意的な意味を持つ限りにおいて）常に成り立つ。
Wikipedia

負数と正数の演算の間にある関係を考えていた時に必要になったので、代入原理の証明を考えてみました。

Wikipediaの書き方は、反射律と代入原理を満たせば必然的に推移率と対称律が導かれる、という風になっています。

同値関係はこんな感じ。

反射律：a ∼ a.
対称律：a ∼ b ならば b ∼ a.
推移律：a ∼ b かつ b ∼ c ならば a ∼ c.
Wikipedia

混乱するのでいずれかを定義にしてしまえば一方は定理として導かれるのだと一先ずは納得させて次へ進みます。

反射律と推移律と対称律がが成り立つのなら、という前提の元に代入原理を証明します。

(A=P(x))=(A=Q(x))→P(x)=Q(x)

(A=P(x))=(A=Q(x))(仮定)
A=P(x)=A=Q(x)(同値変形)
P(x)=Q(x)(推移律)
(A=P(x))=(A=Q(x))→P(x)=Q(x)(→導入)

反射律と代入原理が成り立つと仮定するなら、そこから推移律と対称律が定理として導かれるし、反射律と推移律と対称律から代入原理を導くこともできる。

必要十分条件
A⇔B
は
A→B∧B→A
Aが真ならBも常に真となる関係。
対称律、推移律、反射律を満たす同値関係なので。
A⇔B
は
A=B
であり
(¬A∨B)∧(¬B∨A)
です。