It is easy to prove that an apple is an apple: The equation x=x is a tautology, for all x. So if x=apple, we can substitute it in the equation x=x and get apple=apple, so an apple is an apple.

But how can one prove (using standard deductive logic) that an apple is not an orange, since x!=y is not a tautology for all x,y?
['https://philosophy.stackexchange.com/questions/8459', 'https://philosophy.stackexchange.com', 'https://philosophy.stackexchange.com/users/4639/']
It depends on your definition of "apple" and "orange".

Is a human an ape? Most people would say "no", because their definition of 'ape' implicitly excludes humans. (They mostly involve animals hairier than most humans, and less verbose.) But [humans are apes](http://en.wikipedia.org/wiki/Homo) in the sense understood by modern biologists. So without precise definitions, you are unlikely to be able to prove that humans are not apes.

Analogously, oranges are fruit which were introduced only a few hundred years ago to Europe, and this shows in the names given them by different European languages. In particular, in many slavic languages, nordic languages, and also Dutch, the name for "orange" translates into English literally as "Chinese Apple", after the country which they were first imported from.

Clearly in English we distinguish strongly between apples and oranges, but until the mid 1800s we did not distinguish between lemons and limes; so any attempt to prove that a "lemon" was not a "lime" might have proven confusing. And complicating the matter is that technically, lemons, limes, and oranges are all merely cultivars of the same species of tree (you can cross them and get fertile offspring). This is beside the point for the apple/orange distinction, of course, except that it illustrates that distinctions we take for granted now and for practical purposes are both arbitrary (based on which citrus fruit we wish to distinguish from others) and contingent (our sense of what counts as a lime has changed with time).

Another example: how do you prove that Pluto is not a planet? In the year 2000, you couldn't; it was considered a planet. Now, following [the decision by the IAU in 2006](http://en.wikipedia.org/wiki/IAU_definition_of_planet), one would *start from the agreed-upon definition of a planet*, which includes requirements which Pluto does not fulfil.

In short, in order to prove that any A is not a B — *e.g.* where A is an apple, human, lemon, or the planet Pluto, and B is an orange, an ape, a lime, or a planet — definitions of A and B, or at least *some* extralogical information of what these things are, is necessary.
Use *types*:

So that x:Apple, y:Orange 

This means that x is an apple, y is an orange.

Then we cannot even compare oranges to apples - they're not of the same type; showing that they *must* be different.

If one had an additional type Fruit from which these descend, then the types Orange and Apple would be comparable; but this would be *additional* type information that is unneccessary to implement and demonstrate the question asked by the OP.

It's also worth noting that in an actually existing type system like Haskell, it would not be legal to construct two types of the same nature and name.