Restrict lower case variables to K and upper case variables to P(K).
Assume biduction, also known as symmetric induction: for all nonempty A, if for all x in A, (x in A iff Sx in A) then A = K.
Algelo Margaris, "Successor Axioms for the Integers" uses symmetric induction to axiomatically describe the integers.
(K,S) with biduction is a consistent theory. For example the integers, the positive integers, or the integers modulus n with Sx = x + 1 are models that satisfy the axioms. K could be finite and (K,S) would still be a consistent theory.
Use biduction to define a relation < with not a < a; a <= b iff a < Sb where a <= b is written for a < b or a = b.
Here's my reasoning why 'a <' is defined for all of K. First off a < a is defined as false. Whenever a < b is defined, a < Sb is defined as a <= b Whenever a < Sb is defined, a < b is defined as a < Sb and a = b. This later come from the definition since a <= b iff a < Sb is equivalent to a < b iff a < Sb, a /= b. Thus using biduction conclusion 'a <' is defined for all of K,
However with the establishment of that definition the previous finite models create contradictions. Nothing so simple as < is empty or < equals KxK. No, a raw a < a.