I What Does the Mysterious Symbol in a Formal Proof Represent?

[sa1988]

The below image shows the end part of a formal proof of the inertia tensor. There's a weird symbol in there that I've never seen before, and google isn't bringing much in the way of explanation.

Anybody know what it is? At a guess I'd say it has quite a strong connection to the Kronecker delta in the step above, but a definitive answer would be great. Thanks

 

[Alex163]

http://anorien.csc.warwick.ac.uk/mirrors/CTAN/info/symbols/comprehensive/symbols-letter.pdf

Page 52 gives the LaTex (AMS) description "binary negative entail", naively I'd say that does sound like it'd fit with being a more formal definition of whatever category contains the Kronecker delta. Further attempts at squeezing meaningful links out this symbol lead to vague hints about it being to do with model theory. Which immediately filled me with existential dread. Sorry I can't be of any more help to you, I'd like to know the answer to this as well.

 

[sa1988]

That PDF is gigantic! How did you manage to find it specifically in there?!

Either way, yeah it's an odd one. I can fathom out what it means, based on the step above, but it would be interested to see it properly defined.

 

[jedishrfu]

You could compare the latex mnemonic for that symbol with the kronecker delta you expect to see if a simple typo caused it.

 

[sa1988]

There are over 300 with the string "dash" in them, haha

 

[TeethWhitener]

It almost looks like the rendering of \mathbb{1} (for the identity matrix) went horribly wrong.
Edit: \mathbb{1} doesn't render properly (irony!), but \mathbb{I} gets pretty close: $\mathbb{I}$
2nd edit: Better yet, with the double underline: $\underline{\underline{\mathbb{I}}}$

 

[sa1988]

It almost looks like the rendering of \mathbb{1} (for the identity matrix) went horribly wrong.
Edit: \mathbb{1} doesn't render properly (irony!), but \mathbb{I} gets pretty close: $\mathbb{I}$
2nd edit: Better yet, with the double underline: $\underline{\underline{\mathbb{I}}}$

Sorry for the late reply. I don't come on here much.

I just came back to this thread to say that I've figured it out, but it looks like I was beaten to it!

It certainly must be the identity matrix.

I came across it again in the same lecture notes, at a part covering oscillations using a Lagrangian formulation and finding normal modes using eigenvalues of the resulting matrix construction.

After a bit of careful checking, it now seems obvious that the weird symbol is supposed to be the identity matrix. The image below demonstrates it pretty well (from the original tensor matrix notes I was dealing with before).

That would obviously only work if the symbol there is actually the identity matrix.