@im assume some F = const true,so Forall x.Fx so you can easily find a pair not x=y but Fx iff Fy

@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)

@im Ok, I can get the later proved in HOL, so I guess it would only problematic in Intuitionistic logic

Sign in to participate in the conversation
Mastodon @ SDF

"I appreciate SDF but it's a general-purpose server and the name doesn't make it obvious that it's about art." - Eugen Rochko