I think trying to overformalize this by bringing in LSP might make it harder to understand and easier to nitpick. Another way to look at the same thing is that subclassing/implementation inheritance is an extremely stringent but poorly enforced contract (yeah, also a kind of formalism) that's, in your typical OO language, far too easy break without noticing.
Ironically, the fact that LSP is complicated and to a first approximation nobody understands it is a major part of my point.
(Or, if you prefer, LSP itself isn't that complicated conceptually, but if you try to manifest it in reality it turns out to be very complicated in practice. Code makes a lot more guarantees than we think it does. See also https://hyrumslaw.com/ , which a very different view on the same phenomenon.)
I agree. I think the LSP makes it essentially impossible to subclass a concrete superclass, because the subclass must retain all the observable behaviour of the superclass. If it does so then what's the point? On the other hand, implementing an interface is fine. Different implementations of the interface can just uphold the interface invariants without needing any relationship to each other.
