numbers in TPTP/FOF

[arademaker]

FOF transformation is an inconsistent theory. There is no axiom that formalizes the symbol 0 as the integer zero. A possible solution would be to introduce a step in the FOF transformation to produce terms in Peano notation using the SucessorFn.

% f: (<=> (and (equal (AbsoluteValueFn ?NUMBER1) ?NUMBER2) (instance ?NUMBER1 RealNumber) (instance ?NUMBER2 RealNumber)) (or (and (instance ?NUMBER1 NonnegativeRealNumber) (equal ?NUMBER1 ?NUMBER2)) (and (instance ?NUMBER1 NegativeRealNumber) (equal ?NUMBER2 (SubtractionFn 0 ?NUMBER1)))))
% 0 of 34586 from file /Users/ar/workspace/sumo/Merge.kif at line 4923
% not higher order
fof(kb_SUMO_1,axiom,(( ( ! [V__NUMBER1,V__NUMBER2] : (((s__AbsoluteValueFn(V__NUMBER1) = V__NUMBER2) & s__instance(V__NUMBER1,s__RealNumber) & s__instance(V__NUMBER2,s__RealNumber)) <=> ((s__instance(V__NUMBER1,s__NonnegativeRealNumber) & (V__NUMBER1 = V__NUMBER2)) | (s__instance(V__NUMBER1,s__NegativeRealNumber) & (V__NUMBER2 = s__SubtractionFn(0,V__NUMBER1))))) ) ))).

but the same problem happens to the real numbers. The theory doesn't have axioms to deal with symbols such as 63.54:

% f: (=> (and (instance ?ATOM Copper) (instance ?ATOM Atom)) (measure ?ATOM (MeasureFn 63.54 Amu)))
% 313 of 34586 from file /Users/ar/workspace/sumo/Mid-level-ontology.kif at line 25974
% not higher order
fof(kb_SUMO_239,axiom,(( ( ! [V__ATOM] : ((s__instance(V__ATOM,s__Copper) & s__instance(V__ATOM,s__Atom)) => s__measure(V__ATOM,s__MeasureFn(63.54,s__Amu))) ) ))).

I know that @apease is working on the TFF transformation. Question is if the FOF transformation can be said to be correct/stable/usable without a solution for these issues.

[apease]

I don't think it's accurate to say that these axioms are "invalid". TPTP doesn't support numbers and arithmetic.