Skip to main content
MathOverflow

Return to Question

edited body; edited title
Source Link
Twey
Twey
  • 131
  • 6

Proof of ¬(¬⊤¬1 ⊗ ¬⊤¬1) in tensorial logic

I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.

Is it possible, in Melliès' tensorial logic, to give a proof of ¬(¬⊤¬1 ⊗ ¬⊤¬1) (a.k.a. ⊤1 ⅋ ⊤1)? Equivalently, is there an arrow in a dialogue category (with monoidal unit ⊤1 and negation functor ¬) from ¬⊤¬1 to ⊤1?

Proof of ¬(¬⊤ ⊗ ¬⊤) in tensorial logic

I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.

Is it possible, in Melliès' tensorial logic, to give a proof of ¬(¬⊤ ⊗ ¬⊤) (a.k.a. ⊤ ⅋ ⊤)? Equivalently, is there an arrow in a dialogue category (with monoidal unit ⊤ and negation functor ¬) from ¬⊤ to ⊤?

Proof of ¬(¬1 ⊗ ¬1) in tensorial logic

I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.

Is it possible, in Melliès' tensorial logic, to give a proof of ¬(¬1 ⊗ ¬1) (a.k.a. 1 ⅋ 1)? Equivalently, is there an arrow in a dialogue category (with monoidal unit 1 and negation functor ¬) from ¬1 to 1?

Notice removed Draw attention by Twey
Bounty Ended with Damiano Mazza's answer chosen by Twey
Notice added Draw attention by Twey
Bounty Started worth 50 reputation by Twey
Source Link
Twey
Twey
  • 131
  • 6

Proof of ¬(¬⊤ ⊗ ¬⊤) in tensorial logic

I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it.

Is it possible, in Melliès' tensorial logic, to give a proof of ¬(¬⊤ ⊗ ¬⊤) (a.k.a. ⊤ ⅋ ⊤)? Equivalently, is there an arrow in a dialogue category (with monoidal unit ⊤ and negation functor ¬) from ¬⊤ to ⊤?