4
$\begingroup$

I've recently been looking into linear logic, and it seems every source I can find on it uses the sequent calculus proof system. However, I personally find the sequent calculus to have numerous downsides:

  1. All the branching means it takes up a ton more horizontal space compared to the mostly vertical Fitch proofs. This is something I find annoying both on paper and on computer.
  2. Stylistically, I much prefer working from the premises to the conclusion in the object language rather than reducing a metalanguage representation of the proof.
  3. It's a lot harder to wrap my head around all the new operators, especially since many linear logic resources also use duality principles to move everything onto only the right-side, making it even less clear what I'm actually trying to do. (Even in sequent calculus for classical logic, I already struggle with having multiple formulas on the RHS of the turnstile, let alone putting everything there!)

For these reasons and more, I was wondering if it would be possible to work with linear logic using a Fitch-style natural deduction system instead of the sequent calculus. I understand that the notion of resource expenditure might make it more complex, but surely that could be remedied by crossing off statements once they have been used in an inference?

$\endgroup$

1 Answer 1

3
$\begingroup$

I’ll demonstrate a problem that one would run into while developing a Fitch-style ND system for Linear Logic. Observe the following argument:

  1. p            (Assumption)
    
  2.   p       (Assumption)
    
  3.   p⊗p     (1,2 ⊗ Intro)
    
  4. p⊸(p⊗p)     (2-3, ⊸ Intro)
    

It looks like we should be able to use Modus Ponens on lines 1 and 4, and then use $⊸$ Intro to prove $p⊸(p⊗p)$, but this is clearly invalid in Linear Logic. So, it seems that since the instance of $p$ assumed in line 1 was used to get $p⊗p$ on line 3, we can’t use it for Modus Ponens. However,

$p \vdash p⊸(p⊗p)$

$p⊸(p⊸(p⊗p))$ are both valid.

There may be other necessary restrictions, but this is the one that is most obvious to me.

$\endgroup$
5
  • 1
    $\begingroup$ So, it seems the solution would be to allow a “used-up” premise to be used again for -o intro but not any other inference. $\endgroup$
    – Nico
    Apr 17, 2023 at 20:10
  • $\begingroup$ Natural deduction for FOL also has somewhat unintuitive restrictions on the quantifier inferences, but it’s still widely-used. How come nobody has made a natural deduction system for linear logic before? $\endgroup$
    – Nico
    Apr 17, 2023 at 20:12
  • $\begingroup$ Doesn't look like a problem to me, it just means that all statements in a subproof must be used exactly once. $\endgroup$
    – saolof
    Aug 12, 2023 at 9:22
  • $\begingroup$ @saolof I think the restriction is that formulas in a sub proof without an exponential as the main operator can be used at most once. E.g., you could have $p⊕p^{\bot}$ somewhere in a sub-proof without actually using it. $\endgroup$
    – PW_246
    Aug 12, 2023 at 14:34
  • 1
    $\begingroup$ At most once is a restriction that applies, but by itself it sounds more like affine logic? Either way, Haskell with GHC nine and up has linear types. So linear Haskell programs with let statements should translate fairly directly to Fitch-like natural deduction proofs for (intuitionistic?) linear logic $\endgroup$
    – saolof
    Aug 12, 2023 at 19:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .