Re: How we say Same literals

If "the reader" is a user of a tool that needs to explain inconsistencies
and not a person reviewing or reading a journal article, then explaining
things in multiple steps is probably the right approach.

After explaining that the individual has too many values for the property,
what the limit is, and where it came from, you can explain what the values
of the property are, and where they came from.

Finally you can explain that 'the string «"2"»' is not the same as 'the
integer «2»'.

It is probably not helpful to begin the explanation by saying that "leila
is a person and not a person", which would be where the clash happens.
Explanations meant for human consumption need to be tested on humans.

There is a lot of prior work on this topic from the 80s and 90s, which may
serve as a guide.

Simon

P. S.

Using Robinson's style of theorem proving, the terms could be said to be
"irresolute". In tableaux approaches, this could be described as a "Sex
Pistol". 😉[1]

[1] alethic modal could.
I'm also not sure what you want specifically.

We know, by the predefined disjointness of the types that the values must
be distinct and by the functionality that we must have only one successor.
By the distinctness, we have two. Contradiction.

If you are trying to illustrate how values carry identity conditions, I
wouldn't use values from disjoint types, but merely different values from
the same type eg 1 and 2.

If you are trying to show that lexical form is datatype sensitive then yeah
using same lexical form and disjoint datatype will do the trick.

Cheers,
Bijan.