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?
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, especially section 4, Semantics, for a whirl-wind tour, or section 3.2 of the handouts by Voronkov, for a longer explanation.
It's not a logical truth that an apple is not an orange, but it's nevertheless analytic with respect to the meaning postulate: if predicate P holds uniformly of object a, then for all predicates Q contrary to P, ¬Q(a). For example, if something is uniformly black, then it's not of any color that is contrary to black (say red). Recall that predicates A, B are contraries iff they cannot simultaneously be true of an object:
Definition. Predicates P and Q are contraries =def for all x, either ¬P(x) or ¬Q(x).
Here's how a proof could proceed. We have a meaning postulate, a convention that states that:
P1. For all P, x: if P(x), then for all Q: if P and Q are contraries, then ¬Q(x).
Now we begin with the hypothesis that some object a is an A, and that A and O are contraries:
P2. A(a)
P3. Predicates A and O are contraries
Then we instantiate (P1) with a for x, obtaining:
P4. For all P: if P(a), then for all Q: if P and Q are contraries, then ¬Q(a)
We then instantiate (P4) with A for P and O for Q, obtaining:
P5. if A(a), then if A and O are contraries, then ¬O(a)
The rest is two applications of modus ponens starting with (P5) and using (P2) and then (P3):
P6. if A and O are contraries, then ¬O(a)
P7. ¬O(a)
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 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, 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.
In mathematics, an equals sign connects subject and predicate.
The statement, apple=orange, is the same as the statement, an apple is an orange.
In order to determine an apple is an apple, you used the principle of identity. That which is the same is the same.
In order to determine an apple is not an orange, we use the principle of difference. That which is the same is not different, or two different things are not the same.
General reasoning from sense infers that apples are not oranges. However, if we use the power of abstraction, we can take the concept of an apple, its "appleness", and a concept of an orange, its "orangeness". These conceptions are known though general reasoning from sense and are often informed from the rest of society, e.g. academia.
An apple's "appleness" can only belong to apples. An orange's "orangeness" can only belong to oranges. "appleness" contains no "orangeness". Therefore, something containing "orangeness", namely an orange, is never something containing "appleness", namely an apple, i.e. apples are never oranges.
the logic used here is mathematical logic . but a mathematical logic is only accepted if there is no way to disprove the given logic i.e to say 2+3 =5 and 3+2 also=5 assures the logic that counting 5 pieces from left or right will always remain same because we cant find any two no's which dont obey this logic . so if we assume apple as x and orange as y such that we know always x=x and y=y is true(because any experiment cant disprove this .an apple remains an apple forever) now if somehow apple could change into orange after a few years then x=x would have been wrong and then x=y would hold good also falsness of only x=x directly assures the validity x=y.
but validity of x=x doesnt directly assures the falsness of x=y note:apple=apple means apple will never change to anything else (including orange) and orange=orange means orange will never change to anything else (including apple) so both the chances are finished and there is no other way by which we can say that apple = orange.if one of the two statements x=x and y=y becomes false then x=y can be true means both x=x and y=y should be true
As has been pointed out already, if you are using logic to talk about apples and oranges you have already provided some model (say, a is an apple and o is an orange - formally speaking you've set up a function from constants in your logical language to objects or types or fruit or whatever). So I'm reasonably comfortable that the following proof is no less rigorous than what you've got already: let P (a one-place predicate) be assigned the meaning 'needs to be peeled to be eaten'*. Then Po is true and Pa is false, so then clearly ¬(x = y) holds.
*obviously if you don't peel your oranges feel free to substitute some other predicate that fits
To generalise a little, in case the moral of the above isn't clear, we 'prove' that two objects are distinct by providing some property that holds of one but not the other. It's an open question in metaphysics whether distinct objects can share every property (contenders might be the object of 52 cards and the object of the deck, I guess). Within logic, though, if two elements of your domain are distinct but the same predicates hold of them there isn't a way to prove that they are distinct - you could show that rigorously in a quite straightforward way; proof systems for first-order logic use (roughly) the above method for proving inequality.
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.
