% problem-set/algebra/henkin.models/hp3.ver2.clauses % created : 07/21/86 % revised : 07/18/89 % description: % % Theorem HP3: For all x, x/x = 0. % representation: % % declare_predicates(2,[LE,=]). % declare_function(2,f). % declare_variables(x,y,z,u,v,w). % declare_constants(0,1,a,b,c,d,e). % % P(x,y,z) : means x/y = z % LE : means less than or equal % f(x,y) : denotes x/y % Equality axiom (x = x). % A0: definition of LE (less than or equal to ) -LE(x,y) | (f(x,y) = 0). (f(x,y) != 0) | LE(x,y). % A1: x/y <= x LE(f(x,y),x). % A2: (x/z) / (y/z) <= (x/y) / z LE(f(f(x,z),f(y,z)),f(f(x,y),z)). % A3: 0<=x LE(0,x). % A4: x <= y and y <= x implies that x = y -LE(x,y) | -LE(y,x) | (x = y). % A5: x <= 1 (Thus an implicative model with unit ) LE(x,1). % Implicit in equality formulation: '/' is well defined % HP 1: (f(x,1) = 0). % HP 2: (f(0,x) = 0). % denial of the theorem (f(a,a) != 0).