[Christopher Upshaw](https://forum.azimuthproject.org/profile/2188/Christopher%20Upshaw) wrote:

> I'm going to try to see if you can make a natural deduction version of partition logic, and then get a programming language from that. The same way you can from say, a sub structural logic, or modal logic.

I understand that partition logic has the following adjunctions:

$$

\, \setminus \, \dashv \, \vee \, \dashv \Delta \dashv \wedge

$$

So if partition logic had exponentiation it would just be Boolean logic. I don't know how you would embed a lambda calculus into without that...

EDIT: Keith E. Peterson mentions below that partitions have implication after all. I am rather curious now how the logic differs from classical logic.

> I'm going to try to see if you can make a natural deduction version of partition logic, and then get a programming language from that. The same way you can from say, a sub structural logic, or modal logic.

I understand that partition logic has the following adjunctions:

$$

\, \setminus \, \dashv \, \vee \, \dashv \Delta \dashv \wedge

$$

So if partition logic had exponentiation it would just be Boolean logic. I don't know how you would embed a lambda calculus into without that...

EDIT: Keith E. Peterson mentions below that partitions have implication after all. I am rather curious now how the logic differs from classical logic.