[FOM] Question on Second Order Foundations

[Dmytro Taranovsky]

Ordinary mathematics can be developed in the language of objects and binary
relations.  The intended models have the number of objects sufficiently large
relative to smaller numbers and include all binary relations between the
objects.

What is the most elegant way to axiomatize the system?

The conditions on the intended models uniquely fix the theory.  The theory has
the same Turing degree as second order set theory; and to some extent, the
languages have the same expressive power.

The axiomatization should be at least as strong as ZFC.  One can "transcribe"
NBG or Morse-Kelley set theory into the language, but straightforward attempts
of doing that may not be very elegant.  Note that the language allows
quantification over relations, but does not include any particular relations. 
Although set-theoretic foundations will remained preferred, looking at the
foundations from a different angle can yield new insights.

Sincerely,
Dmytro Taranovsky