An object ?id is the identity element for binary operator ?o over domain ?d iff for every instance ?x of ?d, applying ?o to ?x and ?id results in ?x.
(<=> (Identity-Element-For ?Id ?Op ?Domain) (And (Instance-Of ?Id ?Domain) (Binary-Operator-On ?Op ?Domain) (Forall (?X) (=> (Instance-Of ?X ?Domain) (= (Value ?Op ?Id ?X) ?X)))))