Definition talk:Distinct

I'm doubtful ahout the need to replace:

$x \ne y$

with

$x \ne y \dashv \vdash \neg\left({x=y}\right)$

They mean exactly the same thing, except that: to get your head round the longer version you need to get your head round some specialised symbology from propositional logic which, on this level, is probably not necessary.

Maybe there's a case for explaining that $x \ne y$ means the same as $\neg(x=y)$ on the "equals" page, but outside of the rigorous theorems of PropLog I would suggest that $\dashv \vdash$ is out of place and $\iff$ should be used instead (after all, in PropLog it is demonstrated that in the general context of mathematics they "mean the same thing"). But again, this would be appropriate only on the Definition:Equals page.

What does anyone else think? --prime mover 06:37, 26 January 2012 (EST)

I agree with you in most contexts. However, I will need the distinction somewhere on the site for the following reason.

I need to eventually put up a page with the alphabet Tarski's Geomtry uses. In that alphabet are the symbols $\neg$ and $=$, but not $\ne$. In most contexts it is unimportant, but IMHO when you're stating the alphabet of a language at its most primitive level it is important to explain that $\ne$ is just $\neg =$. Oh, and $\iff$ is also not part of the alphabet, but $\land$ and $\implies$ are.

So I need it somewhere on the wiki. Either:

a) on this page

b) on the equals page

c) on Tarski's alphabet page

d) somewhere else

Or another option would be to use $\neg =$ on all the axiom definitions instead of $\ne$. --GFauxPas 07:32, 26 January 2012 (EST)

I vote for the other option. People stubborn enough to try and comprehend the axioms should already be familiar with $\neg$, and if not, they should be.

Be aware that it is common practice to define shorthands like $\ne$ and $\iff$ fairly quickly after the formal introduction. Maybe they just deserve pages in the Symbols namespace. --Lord_Farin 07:40, 26 January 2012 (EST)

Alright, thanks for the enlightenment. Be aware that my knowledge is self-taught so I don't know what the common practice is :) --GFauxPas 07:44, 26 January 2012 (EST)

I'd say Tarski's alphabet page, probably. But not in Definition:Distinct Elements or you'd be setting a precedent for defining potentially any concept in the particular formal language of whatever axiomatic system.

Take a look at Definition:Set Equality where a link is made to the Axiom of Extension in ZFC, and perhaps do something similar. If it is necessary to be precise about the meaning of "distinct" in the context of Tarski's Geometry (and I believe it probably is), then add such a page to Tarski's Axioms (or in this context, are they "definitions" like "betweenness" and "equidistant", each of which needs to be defined in the 'specific context of Tarski Geometry (and linked to, perhaps, from other pages where they might have similar meanings in different mathematical or axiomatic systems).

What does your source work do about such definitions? I see you've left a link for the definition of "between", but not actually written this definition. Does this mean that "between" is actually defined by the Axiom of Betweenness or whatever it calls itself? In which case wny have a link to a separate page if the definition is in the axiom itself? I haven't read it all in detail as I haven't had the time to spend more than a few minutes on this here and there. --prime mover 07:45, 26 January 2012 (EST)

The reason I haven't actually written the definition is just because I haven't got to it yet. Givant says : "We shall write $B(abc)$ to express the relation of betweenness holds among the points $a,b,$ and $c$; intuitively, this means that point $b$ lies on the line segment joining $a$ and $c$." Later on he gives a formal definition if you're willing to except stuff about $\R^2$. --GFauxPas 07:57, 26 January 2012 (EST)

If I understand correctly, betweenness $\mathsf B$ is a ternary relation symbol, and equidistance is a quaternary relation symbol. They are both part of the language of Tarski's Geometry and as such need interpretation in models. This cannot be handled by axioms (in this light, look at Equidistance is Independent of Betweenness‎‎ and associated talk). --Lord_Farin 07:56, 26 January 2012 (EST)

Right, okay then, I'd be tempted to suggest that there's a version of "Distinct" specific to Tarski geometry (perhaps called "Definition:Distinct Points" or "Definition:Distinct (Tarski Geometry)" or whatever, depending on whether "Distinct" applies to anything except points. Presumably, as the only property of a point is its position, then two points are equal if they are at the same position, and therefore this is therefore consistent with Leibniz...?--prime mover 08:12, 26 January 2012 (EST)

I'll try to address our questions when I get to the page of Tarski's terms, as Givant goes into how Tarski uses =. Take at look at Axiom:Identity of Equidistance. I put a link to that axiom on the point page, though perhaps I shouldn't have. --GFauxPas 08:33, 26 January 2012 (EST)

Oh, I was wrong about $\iff$, he does have it as a primitive term. I have to figure out why. --GFauxPas 08:11, 26 January 2012 (EST)