FollowLast Sets in Dependent Lambek Calculus

Definition. FollowLast Sets in Dependent Lambek Calculus

The followlast set of a grammar $𝐴$ may be captured in Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ via the following proposition:

𝑐 \notin 𝖥𝖫𝖺𝗌𝗍 (𝐴) ≔ 𝐴 & (𝐴 \otimes' 𝑐' \otimes ⊤) ⊢ ⊥

Or perhaps with ones of the grammars

𝐴 \Rightarrow \neg (𝐴 \otimes' 𝑐' \otimes ⊤), 𝐴 \otimes' 𝑐' \otimes ⊤ \Rightarrow \neg 𝐴