Re: Still on negative translation for substructural logics

On 01/12/2024 16:17, Julio Di Egidio wrote:

On 01/12/2024 15:32, Mild Shock wrote:

I am afraid I have no time for that. You
could do it by yourself. Or what

 I have already done it, and I have already told you the results!  You have no time for anything apparently, except for posting random shit and fucking with thread titles: I have messages all over the place, and it's just me, you, and Ross once a month...

And you keep doing it, to the point that again I cannot just continue: you have split this thread in two, and managed to get all points discussed exactly on the wrong side. -- I am looking back at the past week: I cannot find a single reason not to just kill-file you, again.
---
Here are lecture notes that prove that DNT embeds classical into intuitionistic (I take it that their "linear" has not to do with substructural, structurally theirs is a "normal" system):
<https://www.cs.cmu.edu/~fp/courses/15816-f16/lectures/27-classical.pdf>
If I am not totally misreading it, it is indeed not using semantics (or, is it? I don't know what those double brackets mean), though it is definitely at the meta-level.  But I still cannot even fully parse it.
 >> Which is a form of contraction.
 >
 > Which is not allowed in a linear or affine logic.
 >
 > Also, with reference to another comment of yours: my rules are
 > "directed", and that is a feature... as I have read somewhere.
Not only consistency but completeness: and canonicity and decidability... with simplicity. Here is a nice intro:
<https://www.typetheoryforall.com/episodes/type-theory-properties>
A propositional logic is easily all of that, but I'd like to keep it (the kernel) that way all the way up.
To be continued...
-Julio