体の公理
乗法逆元の存在の公理におけるx=0の違和感？をなくした公理系を考えました．そのココロは
(x=0|x*y=1)->(x*(x*y)=x)はOK，整域なら逆もOK
です．
Axioms:
(all x all y all z (x + y) + z = x + (y + z)). (all x all y x + y = y + x). (all x x + 0 = x). (all x exists y x + y = 0). (all x all y all z (x + y) * z = (x * z) + (y * z)). (all x all y all z (x * y) * z = x * (y * z)). (all x all y x * y = y * x). (all x x * 1 = x). (all x exists y x * (x * y) = x). (all x all y (x * y = 0 -> x = 0 | y = 0)). 0 != 1.
Goal:
(all x exists y (x = 0 | x * y = 1)).
Proof:
============================== prooftrans ============================ Prover9 (64) version 2009-02A, February 2009. Process 12008 was started by k on debian, Sat May 17 11:10:43 2014 The command was "/usr/bin/prover9". ============================== end of head =========================== ============================== end of input ========================== ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 1.55 (+ 0.23) seconds. % Length of proof is 76. % Level of proof is 23. % Maximum clause weight is 17. % Given clauses 650. 1 (all x all y all z (x + y) + z = x + (y + z)) # label(non_clause). [assumption]. 2 (all x all y x + y = y + x) # label(non_clause). [assumption]. 3 (all x x + 0 = x) # label(non_clause). [assumption]. 4 (all x exists y x + y = 0) # label(non_clause). [assumption]. 5 (all x all y all z (x + y) * z = (x * z) + (y * z)) # label(non_clause). [assumption]. 6 (all x all y all z (x * y) * z = x * (y * z)) # label(non_clause). [assumption]. 7 (all x all y x * y = y * x) # label(non_clause). [assumption]. 8 (all x x * 1 = x) # label(non_clause). [assumption]. 9 (all x exists y x * (x * y) = x) # label(non_clause). [assumption]. 10 (all x all y (x * y = 0 -> x = 0 | y = 0)) # label(non_clause). [assumption]. 11 (all x exists y (x = 0 | x * y = 1)) # label(non_clause) # label(goal). [goal]. 12 (x + y) + z = x + (y + z). [clausify(1)]. 13 x + y = y + x. [clausify(2)]. 14 x + 0 = x. [clausify(3)]. 15 x + f1(x) = 0. [clausify(4)]. 16 (x + y) * z = (x * z) + (y * z). [clausify(5)]. 17 (x * y) * z = x * (y * z). [clausify(6)]. 18 x * y = y * x. [clausify(7)]. 19 x * 1 = x. [clausify(8)]. 20 x * (x * f2(x)) = x. [clausify(9)]. 21 x * y != 0 | 0 = x | 0 = y. [clausify(10)]. 24 0 != c1. [deny(11)]. 25 c1 != 0. [copy(24),flip(a)]. 26 c1 * x != 1. [deny(11)]. 28 x + (y + z) = y + (x + z). [para(13(a,1),12(a,1,1)),rewrite([12(2)])]. 31 0 + x = x. [para(14(a,1),13(a,1)),flip(a)]. 32 x + (f1(x) + y) = y. [para(15(a,1),12(a,1,1)),rewrite([31(2)]),flip(a)]. 34 (x * y) + (0 * y) = x * y. [para(14(a,1),16(a,1,1)),flip(a)]. 35 (x * y) + (f1(x) * y) = 0 * y. [para(15(a,1),16(a,1,1)),flip(a)]. 36 x * (y + z) = (y * x) + (z * x). [para(18(a,1),16(a,1))]. 37 x * (y * z) = y * (x * z). [para(18(a,1),17(a,1,1)),rewrite([17(2)])]. 41 1 * x = x. [para(19(a,1),18(a,1)),flip(a)]. 45 x * (x * (f2(x) * y)) = x * y. [para(20(a,1),17(a,1,1)),rewrite([17(4)]),flip(a)]. 55 x + (y + f1(x)) = y. [para(15(a,1),28(a,1,2)),rewrite([14(2)]),flip(a)]. 66 f1(f1(x)) = x. [para(15(a,1),32(a,1,2)),rewrite([14(2)]),flip(a)]. 107 x + (0 * x) = x. [para(41(a,1),34(a,1,1)),rewrite([41(5)])]. 122 0 * f1(x) = 0. [para(107(a,1),32(a,1,2)),rewrite([15(2)]),flip(a)]. 127 0 * x = 0. [para(66(a,1),122(a,1,2))]. 129 (x * y) + (f1(x) * y) = 0. [back_rewrite(35),rewrite([127(6)])]. 146 x * (1 + y) = x + (y * x). [para(41(a,1),36(a,2,1))]. 180 x + (f1(1) * x) = 0. [para(41(a,1),129(a,1,1))]. 189 f1(1) * f1(x) = x. [para(180(a,1),32(a,1,2)),rewrite([14(2)]),flip(a)]. 212 f1(x) * f1(1) = x. [para(189(a,1),18(a,1)),flip(a)]. 214 f1(1) * x = f1(x). [para(66(a,1),189(a,1,2))]. 221 x * f1(1) = f1(x). [para(66(a,1),212(a,1,1))]. 222 f1(x) * y = f1(x * y). [para(214(a,1),17(a,1,1)),rewrite([214(6)])]. 223 x * f1(y) = f1(x * y). [para(214(a,1),17(a,2,2)),rewrite([221(3),222(2)]),flip(a)]. 278 x * (x * f2(f1(x))) = f1(x). [para(222(a,1),20(a,1,2)),rewrite([223(6),37(5),222(4),223(5),66(6)])]. 364 x * (x * (f2(f1(x)) * y)) = f1(x * y). [para(278(a,1),17(a,1,1)),rewrite([222(2),17(6)]),flip(a)]. 386 x * (1 + y) = x + (x * y). [para(18(a,1),146(a,2,2))]. 453 x + (x * y) != 0 | 0 = x | 1 + y = 0. [para(386(a,1),21(a,1)),flip(c)]. 474 x * (x * (y * f2(x))) = x * y. [para(18(a,1),45(a,1,2,2))]. 475 x * (f2(x) * f2(f2(x))) = x. [para(20(a,1),45(a,1,2,2)),rewrite([20(3)]),flip(a)]. 499 x * f2(f2(x)) = x * x. [para(475(a,1),45(a,1,2)),flip(a)]. 505 x * (y * f2(f2(x))) = y * (x * x). [para(499(a,1),37(a,1,2)),flip(a)]. 506 f1(x * f2(f2(f1(x)))) = x * x. [para(499(a,1),222(a,1)),rewrite([223(3),18(2),223(2),66(3)]),flip(a)]. 507 x * f2(f2(f2(x))) = x * f2(x). [para(499(a,1),45(a,1,2,2)),rewrite([474(5)]),flip(a)]. 515 x * f2(f2(f1(x))) = f1(x * x). [para(506(a,1),66(a,1,1)),flip(a)]. 565 f1(x * f2(f2(f2(f1(x))))) = f1(x * f2(f1(x))). [para(507(a,1),222(a,1)),rewrite([222(4)]),flip(a)]. 566 x * f2(f2(f2(f2(x)))) = x * x. [para(507(a,1),45(a,1,2,2)),rewrite([505(5),18(3),17(3),20(3)]),flip(a)]. 568 x * (f2(f2(f1(x))) * y) = f1(x * (x * y)). [para(515(a,1),17(a,1,1)),rewrite([222(3),17(2)]),flip(a)]. 573 x * (y * f2(f2(f1(x)))) = f1(y * (x * x)). [para(515(a,1),37(a,1,2)),rewrite([223(3)]),flip(a)]. 634 x * f2(f2(f2(f2(f2(x))))) = x * f2(x). [para(566(a,1),45(a,1,2,2)),rewrite([474(5)]),flip(a)]. 1613 f1(x * f2(f2(f2(f2(f2(f1(x))))))) = f1(x * f2(f1(x))). [para(634(a,1),222(a,1)),rewrite([222(4)]),flip(a)]. 2435 x * f2(f1(x)) = f1(x * f2(x)). [para(364(a,1),474(a,1)),flip(a)]. 2472 f1(x * f2(f2(f2(f2(f2(f1(x))))))) = x * f2(x). [back_rewrite(1613),rewrite([2435(11),66(12)])]. 2482 f1(x * f2(f2(f2(f1(x))))) = x * f2(x). [back_rewrite(565),rewrite([2435(9),66(10)])]. 2513 x * f2(f2(f2(f1(x)))) = f1(x * f2(x)). [para(2482(a,1),66(a,1,1)),flip(a)]. 2521 x * (y * f2(f2(f2(f1(x))))) = f1(y * (x * f2(x))). [para(2513(a,1),37(a,1,2)),rewrite([223(4)]),flip(a)]. 4673 f1(x * (x * f2(f2(f2(f2(f2(f1(x)))))))) = x. [para(507(a,1),568(a,1,2)),rewrite([2521(9),18(6),17(6),573(6),18(3),17(3),20(3),66(2)]),flip(a)]. 4783 x * (x * f2(f2(f2(f2(f2(f1(x))))))) = f1(x). [para(4673(a,1),66(a,1,1)),flip(a)]. 4838 0 = x | 1 + (x * f2(f2(f2(f2(f2(f1(x))))))) = 0. [para(4783(a,1),453(a,1,2)),rewrite([15(2)]),xx(a)]. 9435 x * f2(f2(f2(f2(f2(f1(x)))))) = f1(x * f2(x)). [para(2472(a,1),66(a,1,1)),flip(a)]. 9440 0 = x | 1 + f1(x * f2(x)) = 0. [back_rewrite(4838),rewrite([9435(10)])]. 9453 0 = x | x * f2(x) = 1. [para(9440(b,1),55(a,1,2)),rewrite([13(6),31(6)])]. 9558 $F. [resolve(9453,b,26,a),flip(a),unit_del(a,25)]. ============================== end of proof ==========================
