０の逆元

　一般に環では|-∀y(0*y=0)なので，|-∃y(0*y=1)となる環は零環（0のみからなる環）に限る．

　これを避けて一般に体では¬(0=1)も公理とし，∀x∃y(x=0∨x*y=1)を公理にする．

　対応する選択関数の一つを1/で表すと，この公理は∀x(x=0∨x*(1/x)=1)と表せる．

　とくに，1/0については|-0=0∨0*(1/0)=1が定義となるが，これは等号の公理に従う．

　ここでsemanticを援用し，∀x(0≦1/x→0＜x)の真偽を考えると，上記のように1/0の解釈は任意なので0とし，他は標準的なものとすれば，0≦1/0は真，0＜0は偽．つまり，∀x(0≦1/x→0＜x)を満たさない構造が得られるので，恒真式ではない．したがって，定理式でもない．

　一方，|-∀x(x=0∨x＜0∨0＜x)，|-∀x(x＜0→1/x＜0)，|-∀x(1/x＜0→¬(0≦1/x))なので，|-∀x(¬(x=0)∧0≦1/x→0＜x)ではある．

　要するに，1/xを含む項を述語の引数とする際は，¬(x=0)との連言をとるのが数学．

という，ありふれたお話でした．