2 deleted 691 characters in body
source | link

After some researches I think I have a quite satisfying answer based on Linear Logic.

Suppose we're in the Sequent Calculus (whichwe don't care whether it is said to be "anti-realist". That's why Girard says that it's unacessible to realism. For more information check "Which Logic for the Radical Anti-Realist" from Bonnayclassical or intuitionistic). I won't explain here what Linear Logic isWe know that the cut rule act on ⊢ while the implications rules act on ⇒.

In Linear Logic, the implication is ⊸ (called linear implication of lollipop) soThe turtle tells us that we can translate the problem tohave the distinction between ⊸premises ⊢ A and A ⊢ B and asks us to get B. We have two possible things we can do:

  • The "par" connective ⅋ is actually an "imbrication". The formula A ⅋ B means that we have both A and B but can't use the simultaneously. They are overlapped, superposed, parallel (it's actually easier to see that in Linear Logic's proof nets). See : the "resource interpretation" part on Wikipedia and Resource interpretation for ⅋

    Use the cut rule to infer ⊢ B (that's one should answer to the turtle)
  • Use the left-implication rule to infer A ⇒ A ⊢ B (that's what Achille does)
    • In that case, with another cut (that's what the turtle want) with ⊢ A ⇒ A which is indeed provable we can have have ⊢ B
    • Or you can also use the left-implication rule again (that's what Achille does) to get (A ⇒ A) ⇒ (A ⇒ A) ⊢ B. That rule can be repeated as much as we want.

Conclusion

  • In Linear Logic,The usual model-theoretic interpretation of sequents are described as A1, ..., An ⊢ B1, ..., Bm. Similarly to the Classical Sequent Calculus, the left comma stands for ⊗ and the right one for ⅋. Since duality (linear negation) is involutive it's okay to transform any hypothesisassociated to a conclusion : A1, ..., An ⊢ B1, ..., Bm becomes ⊢ ~A1, ..., ~An, B1, ..., Bmrealism. The [A] formulas were linked by ⊗ but are now linked by ⅋. It means that ⊢ behave like an "imbricator".sequent has a dynamic power : it is non-terminated, it contains a process we can activate.

  • In the other hand, unlike intuitionistic logic but similarly to classical logic, A B = ~A⅋B. It is an imbrication of ~A and A ⊢ B buthave the same interpretation in a more static wayterm of truth values. It hasSo no power and is just passed through ⊢ as any other formula. It is terminateddistinction can be seen.  

  • The rules for cut elimination based on a kind of modus ponens for ⊢ appears to be a kind of "resolution", it moves the proof forward, it is destructive while we can use the rules for implication as many times as we want in some cases (see the example provideddistinction lies in the Blind Spot, Part 3.A.2, is it incremental.computation behaviour of ⊢ and ⇒:

    • ⊢ moves the reasoning forward, that's why it is destructive. It is a real computation. We reach an information we didn't have, that's why it is implicit (close to the synthetic).
    • ⇒ is static because A ⇒ B is a mere frozen object we can manipulate without performing any activation of computation. The implication rules can be seen as a way to "freeze" computation (or unfreeze when reading from bottom to top). That also explains why it is explicit, terminated.
  • By "Logic lies on the dialectic between ⇒ and ⊢", I think we mean that proofs (inThrough the sequent calculus for instance) are about imbricating then deriving sequents (⊢) then finally connecting every atom A to its dual ~ACurry-Howard isomorphism we can also have a simple interpretation with programs. The axiom rule ⊢~A,A is actually ⊢A⊸A so linear implicationcut-rule is actually hidden inrelated to the outcomeprocess of ant proof computation while the implication rules simply manipulates application of functions f(when looking them in a "proof search mode" from bottom to topx) as a frozen object.

EDIT : I edited my answer to a new one without mentioning Linear Logic.

After some researches I think I have a quite satisfying answer based on Linear Logic (which is said to be "anti-realist". That's why Girard says that it's unacessible to realism. For more information check "Which Logic for the Radical Anti-Realist" from Bonnay). I won't explain here what Linear Logic is.

In Linear Logic, the implication is ⊸ (called linear implication of lollipop) so we can translate the problem to the distinction between ⊸ and ⊢.

  • The "par" connective ⅋ is actually an "imbrication". The formula A ⅋ B means that we have both A and B but can't use the simultaneously. They are overlapped, superposed, parallel (it's actually easier to see that in Linear Logic's proof nets). See : the "resource interpretation" part on Wikipedia and Resource interpretation for ⅋

  • In Linear Logic, sequents are described as A1, ..., An ⊢ B1, ..., Bm. Similarly to the Classical Sequent Calculus, the left comma stands for ⊗ and the right one for ⅋. Since duality (linear negation) is involutive it's okay to transform any hypothesis to a conclusion : A1, ..., An ⊢ B1, ..., Bm becomes ⊢ ~A1, ..., ~An, B1, ..., Bm. The [A] formulas were linked by ⊗ but are now linked by ⅋. It means that ⊢ behave like an "imbricator". has a dynamic power : it is non-terminated, it contains a process we can activate.

  • In the other hand, unlike intuitionistic logic but similarly to classical logic, A B = ~A⅋B. It is an imbrication of ~A and B but in a more static way. It has no power and is just passed through ⊢ as any other formula. It is terminated.  

  • The rules for cut elimination based on a kind of modus ponens for ⊢ appears to be a kind of "resolution", it moves the proof forward, it is destructive while we can use the rules for implication as many times as we want in some cases (see the example provided in the Blind Spot, Part 3.A.2, is it incremental.

  • By "Logic lies on the dialectic between ⇒ and ⊢", I think we mean that proofs (in the sequent calculus for instance) are about imbricating then deriving sequents (⊢) then finally connecting every atom A to its dual ~A. The axiom rule ⊢~A,A is actually ⊢A⊸A so linear implication is actually hidden in the outcome of ant proof (when looking them in a "proof search mode" from bottom to top).

After some researches I think I have a quite satisfying answer.

Suppose we're in the Sequent Calculus (we don't care whether it is classical or intuitionistic). We know that the cut rule act on ⊢ while the implications rules act on ⇒.

The turtle tells us that we have the premises ⊢ A and A ⊢ B and asks us to get B. We have two possible things we can do:

  • Use the cut rule to infer ⊢ B (that's one should answer to the turtle)
  • Use the left-implication rule to infer A ⇒ A ⊢ B (that's what Achille does)
    • In that case, with another cut (that's what the turtle want) with ⊢ A ⇒ A which is indeed provable we can have have ⊢ B
    • Or you can also use the left-implication rule again (that's what Achille does) to get (A ⇒ A) ⇒ (A ⇒ A) ⊢ B. That rule can be repeated as much as we want.

Conclusion

  • The usual model-theoretic interpretation of sequents is associated to realism. The sequent ⊢ A B and A ⊢ B have the same interpretation in term of truth values. So no distinction can be seen.

  • The distinction lies in the computation behaviour of ⊢ and ⇒:

    • ⊢ moves the reasoning forward, that's why it is destructive. It is a real computation. We reach an information we didn't have, that's why it is implicit (close to the synthetic).
    • ⇒ is static because A ⇒ B is a mere frozen object we can manipulate without performing any activation of computation. The implication rules can be seen as a way to "freeze" computation (or unfreeze when reading from bottom to top). That also explains why it is explicit, terminated.
  • Through the Curry-Howard isomorphism we can also have a simple interpretation with programs. The cut-rule is related to the process of computation while the implication rules simply manipulates application of functions f(x) as a frozen object.

EDIT : I edited my answer to a new one without mentioning Linear Logic.

1
source | link

After some researches I think I have a quite satisfying answer based on Linear Logic (which is said to be "anti-realist". That's why Girard says that it's unacessible to realism. For more information check "Which Logic for the Radical Anti-Realist" from Bonnay). I won't explain here what Linear Logic is.

In Linear Logic, the implication is ⊸ (called linear implication of lollipop) so we can translate the problem to the distinction between ⊸ and ⊢.

  • The "par" connective ⅋ is actually an "imbrication". The formula A ⅋ B means that we have both A and B but can't use the simultaneously. They are overlapped, superposed, parallel (it's actually easier to see that in Linear Logic's proof nets). See : the "resource interpretation" part on Wikipedia and Resource interpretation for ⅋

  • In Linear Logic, sequents are described as A1, ..., An ⊢ B1, ..., Bm. Similarly to the Classical Sequent Calculus, the left comma stands for ⊗ and the right one for ⅋. Since duality (linear negation) is involutive it's okay to transform any hypothesis to a conclusion : A1, ..., An ⊢ B1, ..., Bm becomes ⊢ ~A1, ..., ~An, B1, ..., Bm. The [A] formulas were linked by ⊗ but are now linked by ⅋. It means that ⊢ behave like an "imbricator". ⊢ has a dynamic power : it is non-terminated, it contains a process we can activate.

  • In the other hand, unlike intuitionistic logic but similarly to classical logic, A ⊸ B = ~A⅋B. It is an imbrication of ~A and B but in a more static way. It has no power and is just passed through ⊢ as any other formula. It is terminated.

  • The rules for cut elimination based on a kind of modus ponens for ⊢ appears to be a kind of "resolution", it moves the proof forward, it is destructive while we can use the rules for implication as many times as we want in some cases (see the example provided in the Blind Spot, Part 3.A.2, is it incremental.

  • By "Logic lies on the dialectic between ⇒ and ⊢", I think we mean that proofs (in the sequent calculus for instance) are about imbricating then deriving sequents (⊢) then finally connecting every atom A to its dual ~A. The axiom rule ⊢~A,A is actually ⊢A⊸A so linear implication is actually hidden in the outcome of ant proof (when looking them in a "proof search mode" from bottom to top).