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/']
What are these "apple" and "orange" that you speak of? In fact, none of the **terms** used in predicate logic have any meaning. The terms need to be **interpreted** according to a **model** or a domain of discourse. See [this SEP entry on Classical Logic](http://plato.stanford.edu/entries/logic-classical/), especially section 4, Semantics, for a whirl-wind tour, or [section 3.2 of the handouts by Voronkov](http://www.voronkov.com/lics_doc.cgi?what=chapter&n=3%E2%80%8E), for a longer explanation.
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.