0
$\begingroup$

In the errata to the third edition of Terry Tao's Analysis I, he suggests that the following remark should be included at the conclusion of Appendix A, the basics of mathematical logic, Section 7, Equality:

For most applications in analysis, one should not need to compare objects of different types: for instance, if $x$ is a set, and $y$ is a number, then one should not need to consider the question of whether $x=y$ is true or false. But for the purposes of doing set theory, it is convenient to adopt the convention that the statement $x=y$ is automatically false if $x,y$ are of different types; for instance, if one is treating natural numbers and vectors as objects of different types, then a natural number would not be equal to a vector. But sometimes we override this convention by identifying objects of one type with some objects of another type, e.g. when we identified natural numbers with their counterparts in the integers, or integers with their counterparts in the rationals, and so forth. This is technically an “abuse of notation”, but can be tolerated as long as one verifies that no violation of the axioms of equality occur by doing so.

Following along these lines, I'm trying to understand how to express, in a many-sorted first-order theory, the convention that objects of different types are unequal. In a metatheory, if I had some function $S$ that would tell me the sort of each object $x$ in a domain of discourse, then I could simply write: $$ \forall x\, \forall y\, (S(x) \neq S(y) \implies x \neq y). $$ But I think a function whose codomain is the set of sorts could only exist in the metatheory, so this wouldn't work as an axiom of the object theory. The approach that comes to my mind is that of instead using an axiom schema. For example, if there are 3 sorts, reserve the letters $x$, $y$, and $z$ for denoting variables of the first, second, and third sorts, respectively, and then include the 3 axioms: \begin{align} \forall x\, \forall y \, & (x\neq y) \\ \forall y\, \forall z \, & (y\neq z) \\ \forall z\, \forall x \, & (z\neq x). \end{align} Is this the right approach to expressing the convention that objects of different types are unequal?

$\endgroup$
3
  • $\begingroup$ You mean x not equal to y but the app won't let me suggest such a small change. Need 6 characters to submit. $\endgroup$ May 19, 2017 at 2:16
  • $\begingroup$ @Jean-FrançoisGagnon Thanks, fixed $\endgroup$
    – justin
    May 19, 2017 at 2:29
  • $\begingroup$ You can see Many-sorted logic. Some more details in Herbert Enderton, "A Mathematical Introduction to Logic" (2nd edition, 2001), pp.295-299. $\endgroup$ May 19, 2017 at 8:57

0

You must log in to answer this question.

Browse other questions tagged .