Currently, the syntactic poset is just used as a stepping stone to the syntactic category. But of course these structures have a lot of interest on their own. For instance, if the full language + deductive calculus of IPL or CPL is implemented (see #10), then we could formalize the proof that their syntactic posets are Heyting algebras / Boolean algebras, respectively.
Currently, the syntactic poset is just used as a stepping stone to the syntactic category. But of course these structures have a lot of interest on their own. For instance, if the full language + deductive calculus of IPL or CPL is implemented (see #10), then we could formalize the proof that their syntactic posets are Heyting algebras / Boolean algebras, respectively.