 An early proposal to answer this was made in Read (2004), thinking of defining identity by means of indiscernibility: \(\forall F((Fa\leftrightarrow Fb)\leftrightarrow a=b)\). This can be put into the form of an Intuitionistic rule-pair, as in  figure 12.  But of course, for the \(=\)-I rule to correctly mirror the second-order quantification of the indiscernibility principle, the \(F\) needs to be “truly arbitrary” (perhaps: a unary predicate that does not occur in any assumption other than the present one). The \(F\) in the \(=\)-E rule, on the other hand, is any unary predicate of the language. There is a burgeoning literature on this topic, much of it focussing on whether it is legitimate to incorporate features of second-order logic in the ways required.