Questions tagged [linear-logic]
The linear-logic tag has no usage guidance.
5
questions
12
votes
1
answer
737
views
Is Girard's LU just an embedding of classical and intuitionistic logic into linear logic?
This question is about Girard's system LU, presented in his paper On the unity of logic. Girard starts by giving a "modal" sequent calculus with two zones of both hypotheses and consequents, $\Gamma;\...
11
votes
2
answers
2k
views
Can linear logic be used to resolve unexpected hanging/surprise examination paradox?
In the Unexpected Hanging Paradox, the prisoner tries to narrow down their date of execution using seemingly sound logical reasoning. They instead arrive at a contradiction. When the paradox is ...
6
votes
1
answer
379
views
Conservativity of multiplicative linear logic over intuitionistic multiplicative linear logic
It is well known that multiplicative linear logic (MLL) is conservative over intuitionistic multiplicative linear logic (IMLL). In other words, if an IMLL formula is provable in MLL then it is already ...
5
votes
1
answer
557
views
Embedding of classical into intuitionistic linear logic
Following on from this recent question, there is another construction that is well-known, but I don’t know a good primary source for: the Kolmogorov-style double-negation embedding of classical into ...
1
vote
1
answer
88
views
Injecting premises into two implicational premises connected by a tensor (multiplicative conjunction) in linear logic
I have another question regarding linear logic: I want to get to the proof E, using the premises in (1-4). Is this at all possible?
1: $A$
2: $C$
3: $(A\multimap B)\otimes(C\multimap D)$
4: $B\...