>>12354625In second-order semantics, where x denotes an element and F a set of elements, interprets as the proposition .
In set theory, the axiom of extensionality states that sets are determined up to equality by their elements. It can be tricky to formalize this axiom (especially in first-order logic), but given that the second-order semantics you have at hand is already informal, there's not much point in doing so.
So I'll just limit to saying that extensionality licenses us to think of each set F as a way to label each element x by one of "Yes" or "No", depending on whether or not. In which case, if , then they are the same element, so every F must label the same way, i.e. .
The converse of Leibniz's Law can also be deduced, provided you are willing to assume that there are "sufficiently" many F's to disambiguate all elements in the domain of discourse. But making this any more precise would run into delicate problems on the formalization of second-order semantics, which cannot be resolved at this crude level of specification.
