@ldbeth That's not how it's quantified, though; it says that if _no_ predicate distinguishes x from y then they are equal, not that, given a predicate, if it doesn't distinguish x from y then they are equal. (This is trivially true if "x =" is a predicate but not if you're working in a logic without primitive equality)

Ian@im@mastodon.sdf.org@ldbeth That's not how it's quantified, though; it says that if _no_ predicate distinguishes x from y then they are equal, not that, given a predicate, if it doesn't distinguish x from y then they are equal. (This is trivially true if "x =" is a predicate but not if you're working in a logic without primitive equality)