a•b≤c ⇔ a≤c←b 这是右剩余
a•b≤c ⇔ b≤a→c 这是左剩余

如果我们用∧替换•，⊢替换≤，可得

a∧b ⊢ c ⇔ a ⊢ c ⊂ b
a∧b ⊢ c ⇔ b ⊢ a ⊃ c

可以看出右剩余←和左剩余→分别就是逆蕴含⊂和蕴含⊃。当然这里我们没有特别强调交换律的问题，如果非交换的话，∧就只能是子结构逻辑中的小野宽晰融合⊗，这时左右蕴含一般写成Lambek的/和\，二者对偶但不直接互逆。

现在来看左剩余的表达式

a∧b ⊢ c ⇔ b ⊢ a ⊃ c

如果我们把其中的b，换成a⊃c，于是

a∧(a⊃c) ⊢ c ⇔ a⊃c ⊢ a⊃c

左侧就是modus ponens。右侧是自反律。

类似的，把右剩余中的a换成c⊂b

a∧b ⊢ c ⇔ a ⊢ c ⊂ b
(c⊂b)∧b ⊢ c ⇔ c⊂b ⊢ c⊂b

不特别强调非交换的话和左剩余的结果是一样的。

++++

所以，modus ponens的代数本质是偏序上的剩余律，这甚至不依赖于格结构。换句话说，它比直觉逻辑的要求要弱得多。