Python & the Law of Identity

Anyone talks Python?

So, someone posted a link to a bit of code in Python purporting that it falsified the Law of Identity.
That's here if you're interested: https://repl.it/repls/SuperficialShimmeringAnimatronics.
The Law of Identity is one of the three laws considered as the foundation of Aristotelian logic. As such, it is crucial to the conventional view of logic whereby illogical is regarded as synonymous with meaningless and nonsensical.
I'm not here to discuss the Law of Identity, so if someone is interested, please start a thread in the philosophy forum.
Instead, can anyone explain the principle of the algorithm?
So, here is the code:

It doesn't seem too complicated, but I'm a complete ignoramus about Python and the guy seems incapable of explaining himself...

Here is also the blurb to explain the motivation behind the code...

Thanks,
EB

 

Log in or Sign up to hide all adverts.

I don't consider myself an expert at Python, but I'll take a stab at it.

First of all: the == is Python for "compare the two objects for equality, and evaluate to/return True or False". The "print" and "format" are just functions manipulating the display; they don't affect the result of the comparison.

We define a new class (object type), called Aristotelian.
We then create a new object of the type Aristotelian, and store it (or rather, a reference to it) in the variable A.
We then compare A to A. Since no special functions to compare objects are mentioned or defined, Python uses the default built-in comparison function, which returns "True" if you compare an object to itself.

Similar structure, but now we do create a special function: __eq__. This is used to evaluate comparisons using the ==-operator. In this case, we define the __eq__ to return False, no matter what. This definition overrides the build-in operator, so now comparisons involving the class Human will use this comparison function, not the built-in one. So when we do the A == A comparison this time, we get False.

So yes: when you literally override/rewrite the rules of logic, your answers may not follow from the conventional rules of logic anymore. I don't see how a conclusion on the validity of the Law of Identity follows, because the second example doesn't use it in the first place?

 

Log in or Sign up to hide all adverts.

Thanks, that's very helpful!
I don't understand what are "self" and "other" in def __eq__(self, other). Can you explain that as well?
EB

 

Log in or Sign up to hide all adverts.

No problem!

(If you are familiar with C++: Python's "self" is C++'s "this".)
Let's say you type "A == B" in Python. Python internally interprets this as "A.__eq__(B)", meaning: from the object A, call its member function __eq__ with as the first (and only) parameter B. Since A is a Human class, the call to A's __eq__ will be 'resolved' to Human.__eq__, and the "A" (the object who's __eq__ is supposed to be called) will be put in the argument list as the first argument. So in the end, it's: Human.__eq__(A, B), so with "self" being A, and "other" being B.

In summary:
A == B
becomes: A.__eq__(B)
becomes: Human.__eq__(A, B)
leading to that __eq__ being run with variable "self" set to object A, and variable "other" set to object B.

 

Good code, but as stated, because the equality operator is overridden, it is meaningless. Good effort though!

 

OK, as I understand it, I would summarise the logic of what he did as essentially substituting an axiom of "non-identity" to the default axiom of identity, and this in-between two evaluations, leading to two contradictory results within the same programme. No big deal. Garbage in, garbage out.

His new claim, however, is that since he could get the same programme to produce a contradiction, and since a programme is equivalent to a logical proof, per Curry-Howard, as he sees it, this is supposed to show that classical logic is wrong about rejecting contradictions. However, again, garbage in, garbage out. In 1st order logic, which I would guess is the assumed logical framework for the computer industry as a whole, if you assume contradictory premises, which is exactly what you do when you use two contradictory axioms as he did, anything whatever follows, including contradictory consequences. This is using a hammer to kill a midget. Gross. And that trick doesn't even prove anything whatever although he could be forgiven for being confused about that.

Your comments welcome.
EB

 

That's my take on it as well.

It's two different programs/classes. But even if he merges them: so what? As you just said, he's using two different logics, one of the one class, and another for the other, and obviously they don't mix very well.

I can easily write a program like this:

def AddTwoNumbersTogether(A, B):

return A + B + 1​

Does this program prove that mathematics as we know it is wrong? Obviously not. He's perhaps got a logical proof equivalent, but it's not a logical proof based on classical logic, so his rejecting of that based on the given argument is incorrect.

I think he got confused by not fully understanding Curry-Howard (not that I do!): the correspondence is between the program and the logic it implements. Implement weird/broken/contradictory logic, and the output of the program can be that as well. He did not implement classical logic correctly, so obviously he can reach conclusions not supported/in contradiction to classical logic. So yes, in that sense: garbage in, garbage out.

 

I agree.

 

Two different logics but within the same programme.
First, I agree that whenever "==" is overwritten by a method specific to A, then "A==A" and "B==B" don't use the same method for comparison and therefore can give different results contrary to A=A and B=B which are effectively equivalent for the ordinary notion of equality since for all x, x=x is true.
However, what this guy does is to replace the axiom of identity that says "for all x, x=x is true" with a freak axiom of non-identity that says "for all x, x=x is true except that for A, A=A is false".
The contradiction then comes from evaluating A==A as true using the default method that implement the axiom of identity, and then, in the same programme, evaluating A==A as false using the method specific to A that implement the freak axiom of non-identity.
The contradiction is in getting the same formalism A==A evaluate first as true, and then as false, in the same programme. Again, I agree it's trivial and doesn't prove anything, but it's nonetheless a contradiction, a purely formal contradiction but code is purely formal anyway, or at least I expect it's meant to be.
What he can't possibly do, however, is get contradictory evaluations for the same formalism A==A each time using the same method of evaluation.

Ah, I think this is the crucial point here: you say the Curry-Howard correspondence is between the program and the logic it implements... I feel good about that idea but are you sure it's true?

Also, I think there is an implementation of the notion of identity in Python, noted Id(x). If so, I would expect you can evaluate Id(x)==Id(y). I would also expect that you can perform the same trick with Id(A)==Id(A) as he did with A==A, unless there is a specific and hardwired "firewall" in Python's syntactic rules against that particular move. It would be interesting to see if the designers of Python have thought about that possibility... If not, maybe it's time you put a word to these guys to think about doing something about it.
EB

 

Well, actually, if you look carefully at what the program does, that's not entirely correct; look back at my explanation of how A == A maps onto the __eq__ function.
A == A is always false in his program, because it uses A.__eq__.
A == B is also always false, because it uses A.__eq__.
B == B is true, because it uses the default built-in __eq__.
B == A is false, because it uses the default built-in __eq__.

The truth-assignment is unambiguous and coherent. A contradiction can only be found if one demands that certain aspects of classical logic hold (B==A is true resulting in A==B is true, while the program says A==B is false), but it is obvious it's the introduction of the assumption that classical logic holds that is causing the contradictions, not the logical system that was used an sich.

Agreed; a formalism that yields incoherent results wouldn't be very useful, IMO.

No, but I don't see how the alternative can be true. How can a program prove something about a logic that it doesn't implement?

I just tried it: the official Python distribution (version 3.6.8) doesn't allow this, because "int" in a built-in type, and cannot be modified that way. But that's (I think) a restriction of this particular implementation of Python, not of the language itself.

Well, I don't see a problem here, so I have no reason to contact anybody about it?

 

Sure, but look again, the programme first evaluates A==A using the default method of comparison and therefore returns True. It's only the second evaluation that relies on the __eq__ method and returns False. And he does this precisely to get a formal contradiction between A == A and A == A, although it's not the same method.

I'd be surprised if you could do that in any version of Python or in any computing language for that matter. But perhaps Python is special in this respect as it seems this language is the computer nerd's wet dream where all restrictions have been removed!
What's "int" exactly?
EB

 

Integer? It doesn't surprise me that you don't know.

 

No, you are introducing the contradiction by demanding that A==A results in the same answer as B==B, which is not true for the given program. The entire point here is that you can no longer exchange A and B, because the __eq__-function (and thus the ==-operator) will react differently depending on which one you provide as input.

It can be done at least in any programming language that is Turing-complete; just not with the built-in variable types. But it looks like Ada supports this out-of-the-box, but I unfortunately have no experience with that language. Also, it's easy enough to write your own interpreted language where this is possible.

(In a similar vein: I remember that the earliest Fortran compilers allowed you to change the value of numerical constants. In other words, a constant "1" in the code could evaluate to the value of 2 when executed.)

Nope, there's still quite a few restrictions present. If you really want the fewest restrictions possible while still running directly on hardware, Assembly is the way to go. If you drop the hardware requirements, the sky's the limit!

It indeed is short for "integer". It is a built-in variable type that can hold integer numbers.

 

First, without __eq__, A==A results in the same answer as B==B, i.e. True.
Second, the programme only evaluates A==A, and it does it twice. It doesn't even try B==B. So, I'm not sure what is your point exactly.
The programme's trick is to get two contradictory evaluations for A==A.

If the language gives you access to the identity of some entity, object or variable, this identity is presumably the address of the content data (possibly just pointers) taken to be the characteristic of this entity. If you can change this identity then it's not really anything like the notion of identity of the Law of Identity in logic.

So, I guess I don't understand what you meant by "because "int" in a built-in type, and cannot be modified that way" in relation to my suggestion of doing the same trick with Id(A)==Id(A) as he did with A==A... An integer will have an "Id" but it's not something specific to the type Integers.
EB

 

Good, so we know you're a triple idiot.
I'm asking about Python because I don't know the language. I did a lot of programmation myself with all sorts of languages so I know what "int" means in that context. However, I couldn't see and still can't see why NE mentioned "int" in relation to Id(A) in Python if "int" stood for integer.
No doubt you know.
EB

 

Technically, it still uses the __eq__; just the default one.

Ah, I see where your confusion is coming from. No, the two "A==A"'s are not the same: the A's differ in type, and because of the way the ==-operator is overloaded (i.e. it runs different code depending on the types of input), this results in two different answers. This situation is not possible in classical logic, and it's your thinking in terms of that classical logic that creates the contradiction. Let go of your demands for classical logic and its behaviours, and the contradiction disappears.

No, it's not. It's how the ==-operator is defined: it's working just fine. The only contradiction is with classical logic; the ==-operator is perfectly well-defined here, even though it doesn't abide by the rules of classical logic. See my truth-table earlier.

In Python it's not documented to be; it's merely some integer number that's unique for the lifetime of the object. It might be the memory address, but it's quite possible it's not. (Also, it's possible for different objects to have the same memory address, although this is very hacky: GCC did this in the earlier 2000's in their C++'s vector<bool> implementation.)

I don't see how that's relevant here? The __eq__-function given in the code snippet doesn't use the Id-function?

What I meant by that is that it's not possible to change the __eq__-function of the int-class. In other words, in the official Python implementation you cannot change the behavior of int.__eq__.

And I don't see how it's possible to implement the same trick using Id... Please provide a code snippet if you manage that, because I'm interested in seeing that!

True, but I still don't see how Id is relevant for the code snippet above? In fact, it's quite possible that the standard __eq__-function doesn't use it, because if you have two different int-objects, both with the same value, it would return the wrong result.

 

Ah OK, now I see what you are getting at. The Id-function returns an "int", so if you want to mess with Id(A)==Id(A), you have to mess with int.__eq__.

 

Independent advice I got...
"The Curry-Howard correspondence is a mathematical correspondence between particular logical systems and particular λ-calculi.
Python doesn't have the kind of formal definitions to be possibly used in the context of the Curry-Howard correspondence."
But they don't like the suggestion that the correspondence would be really between a programme and the logic effectively implemented in this particular programme.
EB

 

Ah well, that settles it then! If the correspondence doesn't apply to Python, the argumentation given in the OP is invalid. Problem solved.

Please Register or Log in to view the hidden image!

 

OK, that sounds more like what I would expect of reasonable people... So he couldn't possibly have done the same trick with Id(A)==Id(A).
EB