読者です 読者をやめる 読者になる 読者になる

体の公理

乗法逆元の存在の公理における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 ==========================