Python & the Law of Identity

[Speakpigeon]

Anyone talks Python?

Python (programming language)
Python is an interpreted, high-level, general-purpose programming language. Created by Guido van Rossum and first released in 1991, Python has a design philosophy that emphasizes code readability, notably using significant whitespace. It provides constructs that enable clear programming on both small and large scales. Van Rossum led the language community until stepping down as leader in July 2018.
Python features a dynamic type system and automatic memory management. It supports multiple programming paradigms, including object-oriented, imperative, functional and procedural, and has a large and comprehensive standard library.
Python interpreters are available for many operating systems. CPython, the reference implementation of Python, is open source software and has a community-based development model, as do nearly all of Python's other implementations. Python and CPython are managed by the non-profit Python Software Foundation.
https://en.wikipedia.org/wiki/Python_(programming_language)

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 Logic & Epistemology forum.

Instead, can anyone explain the principle of the algorithm?

So, here is the code:

class Aristotelian(object):
def __init__(self):
pass
A = Aristotelian()
print("Law of Identity: A = A => {}".format(A == A))
class Human(object):
def __init__(self):
pass
def __eq__(self, other):
return False
A = Human()
print("Law of Humanity: A = A => {}".format(A == A))

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...

# The law of identity is the cornerstone of Arostotelian/Classical logic.
# A = A is True.
# In the 2nd half of the 20th century the American mathematician Haskell Curry and logician William Alvin Howard discovered an analogy between logical proofs and working computer programs.
# This is known as the Curry-Howard correspondence.
# Mathematical proofs are working computer programs.
# https://en.wikipedia.org/wiki/Curry–Howard_correspondence
# Therefore, if we can write a working computer program which asserts that A = A is false we have living proof that founding axiom of Aristotelian logic is a mistake.
# I hereby reject the Aristotelian religion and I embrace Lambda calculus.

Thanks,
EB

 

[Jokodo]

The crucial line is

def __eq__(self, other):
    return False

What this does is just overriding the comparison method with unconditionally returning `false`. It shows that when you don't actually do an identity check but only pretend you did one, you're free to report whatever you choose as the alleged result.

That's about it.

 

[Speakpigeon]

The crucial line is

def __eq__(self, other):
    return False

What this does is just overriding the comparison method with unconditionally returning `false`. It shows that when you don't actually do an identity check but only pretend you did one, you're free to report whatever you choose as the alleged result.

That's about it.

Whoa.This is seriously fucked.

No wonder the guy doesn't want to provide a formal proof equivalent.

Thanks.
EB

 

[Jokodo]

The crucial line is

def __eq__(self, other):
    return False

What this does is just overriding the comparison method with unconditionally returning `false`. It shows that when you don't actually do an identity check but only pretend you did one, you're free to report whatever you choose as the alleged result.

That's about it.

Whoa.This is seriously fucked.

No wonder the guy doesn't want to provide a formal proof equivalent.

Thanks.
EB

To be more precise, '==' and '__eq__' which it is shorthand for isn't actually an identity check but an equality check. It is a very useful feature to be allowed to overwrite it, e. g. if you have your custom data container that contains a lot of information about an entity in the world, and also a timestamp when you last updated the information, it would be very counter-productive if the comparison were to return False because the timestamp differs if your goal is to determine how much info has changed. So you overwrite the equality testing method with something along the lines of "ignore timestamp, check if all other attributes are identical".

Identity in Python is checked with the keyword is (like the English word) and cannot be overwritten. So if you actually do an identity rather than equality check with the class defined in your code, as below, you get True:

A = Human()
print("Law of Humanity: A = A => {}".format(A is A))

 

[Speakpigeon]

To be more precise, '==' and '__eq__' which it is shorthand for isn't actually an identity check but an equality check. It is a very useful feature to be allowed to overwrite it, e. g. if you have your custom data container that contains a lot of information about an entity in the world, and also a timestamp when you last updated the information, it would be very counter-productive if the comparison were to return False because the timestamp differs if your goal is to determine how much info has changed. So you overwrite the equality testing method with something along the lines of "ignore timestamp, check if all other attributes are identical".

Identity in Python is checked with the keyword is (like the English word) and cannot be overwritten. So if you actually do an identity rather than equality check with the class defined in your code, as below, you get True:

A = Human()
print("Law of Humanity: A = A => {}".format(A is A))

That explains another argument this guy has where he produced a kind of "syllogism" where "=" and "is" are mixed up as if meaning the same: Socrates is human v. Socrates = human. He probably got inspired by writing Python code.

Also, I see how "return False" would be crucial here, but what is the role of "self" and "other" in the line "def __eq__(self, other)"? How does that affects the instruction print("Law of Humanity: A = A => {}".format(A == A))?
EB

 

[Jokodo]

To be more precise, '==' and '__eq__' which it is shorthand for isn't actually an identity check but an equality check. It is a very useful feature to be allowed to overwrite it, e. g. if you have your custom data container that contains a lot of information about an entity in the world, and also a timestamp when you last updated the information, it would be very counter-productive if the comparison were to return False because the timestamp differs if your goal is to determine how much info has changed. So you overwrite the equality testing method with something along the lines of "ignore timestamp, check if all other attributes are identical".

Identity in Python is checked with the keyword is (like the English word) and cannot be overwritten. So if you actually do an identity rather than equality check with the class defined in your code, as below, you get True:

A = Human()
print("Law of Humanity: A = A => {}".format(A is A))

That explains another argument this guy has where he produced a kind of "syllogism" where "=" and "is" are mixed up as if meaning the same: Socrates is human v. Socrates = human. He probably got inspired by writing Python code.

Actually, no. Confusing them will lead to non-compiling code in Python as "=" is assignment only, and "==" and "is" have different effects.

Also, I see how "return False" would be crucial here, but what is the role of "self" and "other" in the line "def __eq__(self, other)"? How does that affects the instruction print("Law of Humanity: A = A => {}".format(A == A))?
EB

equality is a two-place predicate, but behind the scenes, everything is an object so operations are really methods on objects. If you write "A == B", what's really happening isn't that some global equality operation grabs both A and B and compares them, but rather (roughly, there's probably some resorting to __cmp__ in between):
* the interpreter tries if the object A has an `__eq__` method and does whatever that method says;
* if that fails it checks if B has an `__eq__` method, and
* if that also fails it does identity checking.

`self` is the reference to the method's owning object (`this` if you're more familiar with Java), `other` is the reference to whatever it's going to be compared with.

Here's some silly-but-not-quite-as-silly-as-what-you-quoted code where you might actually overwrite __eq__ in real life, and illustrating what this does:

class Location(object):
    def __init__(self):
        pass


earth = Location()


class PhysicalObject(object):
    """A physical object with some parameters"""

    def __init__(self, mass=0.0, market_value=0.0, composition=None,
                 provenance=None):
        if not provenance or not isinstance(provenance, Location):
            provenance = earth
        self.provenance = provenance
        self.mass = mass  # mass in kg
        self.market_value = market_value  # market value in euros
        self.composition = composition

    @classmethod
    def from_object(cls, other):
        return cls(**vars(other))


class Commodity(PhysicalObject):
    """A physical object in its role as market commodity"""

    def __eq__(self, other):
        try:
            return self.market_value == other.market_value
        except:
            raise ValueError


class BalanceWeight(PhysicalObject):
    """A physical object used as a weight for a balance"""

    def __eq__(self, other):
        try:
            return self.mass == other.mass
        except Exception as e:
            raise e


apple = PhysicalObject(mass=0.2, market_value=0.3)
nugget = PhysicalObject(mass=0.2, market_value=300)
nugget2 = PhysicalObject.from_object(
    nugget)  # second object with same specifications
apple_as_weight = BalanceWeight.from_object(apple)
nugget_as_valuable = Commodity.from_object(nugget)

print(apple_as_weight == nugget_as_valuable)  # True because
# BalanceWeight compares only mass
print(nugget_as_valuable == apple_as_weight)  # False because
# Commodity compares market value, as it comes first, the nugget's
# __eq__ method isused
print(nugget == apple_as_weight)  # True because the plain
# nugget-as-physical-object doesn't have an __eq__ method, so
# the apple's is used
print(nugget == nugget2)  # False because the run-of-the-mill PhysicalObject
# doesn't have an __eq__ method defined: despite all the same
# specifications, the two instances are independent objects and the Identity check fails

 

[Jokodo]

Maybe more to the point of your question, self and other are needed in the method definition even though they're not used because otherwise you get a TypeError when you try to pass two arguments to a function that takes none in "A==A".

 

[J842P]

This is dumb, for the reason's pointed out by Jokodo. But more succinctly, without all that rigamarole, he could have just written:

print("A = A => False")

And it demonstrates the exact same thing, namely, nothing he is claiming. This doesn't prove anything about the Law of Identity. The crux of Curry-Howard is this (taken from wikipedia):

In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.

If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program. More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.

IOW, the formalisms are equivalent. But because of this, it does not follow that just because I can as easily state an invalid or even unsound proposition using a propositional proof system (no Python required) that I've disproven the Law of Identity.

 

[J842P]

`self` is the reference to the method's owning object (`this` if you're more familiar with Java), `other` is the reference to whatever it's going to be compared with.

Since this is a programming thread, I'm going to be pedantic.

In Python, methods *do not belong to instances*. If anything, instances belong to the method.


Consider this:

>>> class Foo:
...    def bar(self):
...       return 42
...
>>> foo = Foo()
>>> foo.bar
<bound method Foo.bar of <__main__.Foo object at 0x101f0f4e0>>
>>> foo.bar is foo.bar
False

`self` is merely the name we conventionally give to the first argument to a function that will be a method. Methods are simply normal function objects *that belong to a class namespace*, that get *bound* to the instance *when called on the instance*. This is done through the descriptor protocol, because *function objects are descriptors!*, they have a `__get__` method.


So what is happening on *each method invocation on an instance* is essentially:

>>> Foo.bar
<function Foo.bar at 0x101ed8950>
>>> Foo.bar.__get__(foo) # bind the instance to the first argument, this is pretty much what happens underneath the hood
<bound method Foo.bar of <__main__.Foo object at 0x101f0f4e0>>
>>> Foo.bar.__get__(foo)()
42
>>> foo.bar()
42

In the Descriptor HOWTO, we see an example of how this could be implemented in pure Python (of course, in CPython, this is implemented in C):

class Function(object):
    . . .
    def __get__(self, obj, objtype=None):
        "Simulate func_descr_get() in Objects/funcobject.c"
        if obj is None:
            return self
        return types.MethodType(self, obj)

 

[Speakpigeon]

Maybe more to the point of your question, self and other are needed in the method definition even though they're not used because otherwise you get a TypeError when you try to pass two arguments to a function that takes none in "A==A".

But I would think "A==A" has two arguments, namely "A" and "A"?

I thought I had understood that "self" and "other" were the necessary placeholders for whatever will eventually be compared, so that in this particular case, we get both self:= A and other:= A so that the "==" operator gets to compare A with itself. If so, the argument "self" and "other" are used, if only implicitly, and their role is crucial. In particular, this is what is effectively forcing the comparison method to evaluate A==A as False, without in fact any kind of comparison other than A being assigned both to "self" and to "other".

Could you clarify?
EB

 

[Speakpigeon]

This is dumb, for the reason's pointed out by Jokodo. But more succinctly, without all that rigamarole, he could have just written:

print("A = A => False")

And it demonstrates the exact same thing, namely, nothing he is claiming. This doesn't prove anything about the Law of Identity. The crux of Curry-Howard is this (taken from wikipedia):

In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.

If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program. More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.

IOW, the formalisms are equivalent. But because of this, it does not follow that just because I can as easily state an invalid or even unsound proposition using a propositional proof system (no Python required) that I've disproven the Law of Identity.

Yes, I would really like to understand what the Curry-Howard's notion of "analogous" really means. If this is a "strong" analogy which is meant, I would expect that any programme whatsoever could be literally and entirely transcribed as a valid logical proof. I'm not sure this was really what these guys had in mind! Your example, print("A = A => False"), would have to be a proof, but what proof exactly? If we don't have the equivalent proof then Curry-Howard doesn't help.

Perhaps one way to think of it is that the Law of Identity is not a fundamental logical law but merely the definition of the sign "=", i.e. Def(=): ∀x(x=x). If so, the Python line forcing A==A to False is simply a redefinition of the semantic of the sign "=", which obviously has radical consequences but not that you prove the Law of Identity false. Rather, it just shows that you can adopt a different definition of the sign "=" than the conventional ∀x(x=x). However, once you do that, then "=" no longer means equal as we all think of it. I guess the crux of the issue is whether you could get any Python code to do anything substantial once you've redefined "==" to return False. In particular, I would expect a contradiction to appear somewhere. Do we also have symmetry (A=B → B=A) and transitivity (A=B ∧ B=C → A=C) with the Python comparison as we have with the ordinary "=" comparison?
EB

 

[J842P]

Maybe more to the point of your question, self and other are needed in the method definition even though they're not used because otherwise you get a TypeError when you try to pass two arguments to a function that takes none in "A==A".

But I would think "A==A" has two arguments, namely "A" and "A"?

I thought I had understood that "self" and "other" were the necessary placeholders for whatever will eventually be compared, so that in this particular case, we get both self:= A and other:= A so that the "==" operator gets to compare A with itself. If so, the argument "self" and "other" are used, if only implicitly, and their role is crucial. In particular, this is what is effectively forcing the comparison method to evaluate A==A as False, without in fact any kind of comparison other than A being assigned both to "self" and to "other".

Could you clarify?
EB

Yes, that is what Jokodo is saying. It is helpful to understand that in Python, everything is an object, there are no primitive types, and built-in operators like `==` or `+` are merely syntactic sugar around calls to methods on these objects¹. So, you can think of:

x == y

As syntactic sugar for:

type(x).__eq__(x, y)

The interpreter will always call `__eq__` with two arguments. If you don't define your `__eq__` function on your type to have those parameters, you'll get a type error, because you are calling a function with invalid arguments. In this case, the implementation simply ignores those parameters, and always returns `False`.

Also, note, the actual names of the parameters don't matter. `self` is merely a convention, and `other` is merely a good descriptive name. You could use:

def __eq__(banana, pineapple):
    ...

And it works. But you should follow conventions in programming, that is, if you want other people to be able to easily digest your code.


^{1. If you want to know more, read the documentation on the Python Data Model}

 

[Jokodo]

Maybe more to the point of your question, self and other are needed in the method definition even though they're not used because otherwise you get a TypeError when you try to pass two arguments to a function that takes none in "A==A".

But I would think "A==A" has two arguments, namely "A" and "A"?

"==" is overwritten. If A has an `__eq__` method set, "A==B" will be interpreted as A.__eq__(B). If A.__eq__ doesn't take a second argument, you get a TypeError, and since that's not what he wants to get, you friend has to define a dummy "other" argument in the method's definition.

I thought I had understood that "self" and "other" were the necessary placeholders for whatever will eventually be compared, so that in this particular case, we get both self:= A and other:= A so that the "==" operator gets to compare A with itself. If so, the argument "self" and "other" are used, if only implicitly, and their role is crucial.

That sounds about right.

In particular, this is what is effectively forcing the comparison method to evaluate A==A as False, without in fact any kind of comparison other than A being assigned both to "self" and to "other".

It doesn't force it, it merely allows it. Any well-formed __eq__ method has two arguments, conventially named "self" and "other", though no-one stops you from calling them "ego" and "super_ego" (except your company's code style if you're lucky, and yes, I mean lucky). What makes it evaluate False is the next line, that says just return False without any checking.

 

[J842P]

This is dumb, for the reason's pointed out by Jokodo. But more succinctly, without all that rigamarole, he could have just written:

print("A = A => False")

And it demonstrates the exact same thing, namely, nothing he is claiming. This doesn't prove anything about the Law of Identity. The crux of Curry-Howard is this (taken from wikipedia):

In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.

If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program. More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.

IOW, the formalisms are equivalent. But because of this, it does not follow that just because I can as easily state an invalid or even unsound proposition using a propositional proof system (no Python required) that I've disproven the Law of Identity.

Yes, I would really like to understand what the Curry-Howard's notion of "analogous" really means. If this is a "strong" analogy which is meant, I would expect that any programme whatsoever could be literally and entirely transcribed as a valid logical proof. I'm not sure this was really what these guys had in mind! Your example, print("A = A => False"), would have to be a proof, but what proof exactly? If we don't have the equivalent proof then Curry-Howard doesn't help.

Perhaps one way to think of it is that the Law of Identity is not a fundamental logical law but merely the definition of the sign "=", i.e. Def(=): ∀x(x=x). If so, the Python line forcing A==A to False is simply a redefinition of the semantic of the sign "=", which obviously has radical consequences but not that you prove the Law of Identity false. Rather, it just shows that you can adopt a different definition of the sign "=" than the conventional ∀x(x=x). However, once you do that, then "=" no longer means equal as we all think of it. I guess the crux of the issue is whether you could get any Python code to do anything substantial once you've redefined "==" to return False. In particular, I would expect a contradiction to appear somewhere. Do we also have symmetry (A=B → B=A) and transitivity (A=B ∧ B=C → A=C) with the Python comparison as we have with the ordinary "=" comparison?
EB

It's been a long time since I looked at this stuff, and I never took a deep dive, so take my musings with a grain of salt. This is more in Jokodo's wheelhouse, so maybe Jokodo can chime in and we can safely ignore what I'm saying, but ...


I think fundamentally what is going on is a category error . The analogy is between proof systems and models of computation (like the lambda calculus). Models of computation are formalisms used to study computer programs and algorithms in the abstract. Python is not a model of computation, it is a concrete programming language. All a programming language does is give you an easy human readable way to tell a computer what to do. You can tell your computer to do anything. If that is telling your computer to print a bunch of untruths to the screen, it will happily do that.


What Curry-Howard claims, fundamentally, is that theories of computation are isomorphic to structural logic. Here's a link that actually gets into the details:

https://en.wikibooks.org/wiki/Haskell/The_Curry–Howard_isomorphism

Suffice it to say, it doesn't mean "because I can write a Python program that prints something, I've proven that proposition that it is printing". That's not even wrong. It's simply nonsensical as far as I can tell. A Python program doesn't prove anything. A formal description of the Python program, using say, a typed lambda calculus, would be proving a statement about the types of the program.


Finally, since you asked, you are correct that an implementation of `==`, i.e. `__eq__` in Python does not have to obey the rules of an equivalence relation. That's fine. Equality in programming language often doesn't strictly obey the axioms of an equivalence relation. Consider the `==` and the numeric data types. The `float` type include `NaN` (not a number), and `NaN` does not obey reflexivity. So `NaN == NaN` returns `False`. We are simply always just re-defining symbols. These symbols are really only useful as higher-order abstractions to humans. To the computer, it's simply pushing bytes around. Whether the abstractions we've created are sound doesn't matter to the computer. So in summary:

Rather, it just shows that you can adopt a different definition of the sign "=" than the conventional ∀x(x=x).

Is essentially exactly what is happening in that Python code. It is defining what the `==` sign means when applied to objects of type `Human` (and only when objects of type human are on the left hand side of the operator).

 

[Jokodo]

(and only when objects of type human are on the left hand side of the operator).

Since we are already being pedantic: when objects of type human are on the left hand side of the operator or when objects of type human are on the right hand side of the operator and the object on the left hand side doesn't have a defined `__eq__` method.

 

[J842P]

(and only when objects of type human are on the left hand side of the operator).

Since we are already being pedantic: when objects of type human are on the left hand side of the operator or when objects of type human are on the right hand side of the operator and the object on the left hand side doesn't have a defined `__eq__` method.

OR when objects on the left hand side return `NotImplemented` from `__eq__`, and the object on the right is of type Human

That extra set of logic is a good example of why "dunder" methods aren't exactly equivalent to the operators/built-in functions they are meant to correspond to.

 

[Jokodo]

Do we also have symmetry (A=B → B=A) and transitivity (A=B ∧ B=C → A=C) with the Python comparison as we have with the ordinary "=" comparison?
EB

Unless you overwrite it, yes. As soon as you overwrite it, it all depends what you overwrite it with. I gave an example in post #6 where symmetry doesn't hold:

>>> print(apple_as_weight == nugget_as_valuable) 
True
>>> print(nugget_as_valuable == apple_as_weight)
False

It's equally possible to make it so that transitivity doesn't hold: since "==" always first checks the left hand side argument's `__eq__` method (if defined), you only need to make it so that A and B are different classes that use different logic to determine equivalence: If A is a BalanceWeight of post #6, and B is a Commodity as defined there, A==B will be True if A and B have the same mass, while B==C will be True if B and C have the same market value.

It is left as an exercise to the reader to decide whether or not that implies A and C have the same mass.

 

[steve_bank]

a = 2 puts 2 in the variable a, it makes a and 2 equal.

== is one of several logical tests.
<
<=
>
>=

in C if(arg) evaluates arg. If it is positive the if will be executed.

If( a == b) the == will call a function that compares a and b and returns 1 for a match.

a = 2
If(a) ..then do this

in if( b =2) first 2 is transferred to b and b is evaluated.


this prints "match'
b = 2
if( b == 2) then print "it is a match.
else print"no match"

this prints "no match'
b = 3
if( b == 3) then "print match"
else print "no match"

this prints "positive"
if(a = 2) then print"positive"
else print"not positive"

this prints "not positive"
if(a = -2) then print"positive"
else print"not positive"

a = 2 says make a equal to 2

a == 2 says check if a and 2 are the same.

<= less than or equal
>= grater tan or equal

There is no logical conundrum. It is a form of symbolic logic.

Scroll down to logic comparisons.

https://www.programiz.com/python-programming/operators

 

[Speakpigeon]

Do we also have symmetry (A=B → B=A) and transitivity (A=B ∧ B=C → A=C) with the Python comparison as we have with the ordinary "=" comparison?
EB

Unless you overwrite it, yes. As soon as you overwrite it, it all depends what you overwrite it with. I gave an example in post #6 where symmetry doesn't hold:

>>> print(apple_as_weight == nugget_as_valuable) 
True
>>> print(nugget_as_valuable == apple_as_weight)
False

It's equally possible to make it so that transitivity doesn't hold: since "==" always first checks the left hand side argument's `__eq__` method (if defined), you only need to make it so that A and B are different classes that use different logic to determine equivalence: If A is a BalanceWeight of post #6, and B is a Commodity as defined there, A==B will be True if A and B have the same mass, while B==C will be True if B and C have the same market value.

It is left as an exercise to the reader to decide whether or not that implies A and C have the same mass.

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

 

[Jokodo]

Do we also have symmetry (A=B → B=A) and transitivity (A=B ∧ B=C → A=C) with the Python comparison as we have with the ordinary "=" comparison?
EB

Unless you overwrite it, yes. As soon as you overwrite it, it all depends what you overwrite it with. I gave an example in post #6 where symmetry doesn't hold:

>>> print(apple_as_weight == nugget_as_valuable) 
True
>>> print(nugget_as_valuable == apple_as_weight)
False

It's equally possible to make it so that transitivity doesn't hold: since "==" always first checks the left hand side argument's `__eq__` method (if defined), you only need to make it so that A and B are different classes that use different logic to determine equivalence: If A is a BalanceWeight of post #6, and B is a Commodity as defined there, A==B will be True if A and B have the same mass, while B==C will be True if B and C have the same market value.

It is left as an exercise to the reader to decide whether or not that implies A and C have the same mass.

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

I can see no contradiction only sloppy use of variable names (that is, labels). In the line where he writes `A = Human()` he's making the label "A" refer to a different entity than it previously did, overwriting the earlier assignment of `A = Aristotelian()`. That's no more a contradiction than in the two sentences "America extends from the Mexican border to the Canadian border" and "America extends from Tierra del Fuego to the Arctic Ocean". Both are true statements for one common interpretation of the label "America", and arguably, he'd have a better case arguing for a real contradiction here than with his code, since he didn't actively overwrite any assignment, he took what he found (and could be sort of kind of forgiven for missing the fact that the label is ambiguous between to entities, which the statements are about).