1
$\begingroup$

Apologies if the question doesn't make sense: it's one of those cases where my confusion is so diffuse that I'm not even sure how to ask the question.

In short, I would like to know if it's possible, within some variant of sequent calculus, to prove the sequent $$ \varGamma \,\vdash\, V $$ starting from the two sequents $$ \varGamma \,\vdash\, U \lor V \ ;\qquad \varGamma \land \lnot V \,\vdash\, \lnot U $$ $$ \text{(or equivalently} \qquad \varGamma \,\vdash\, U, V \ ; \qquad \varGamma, \lnot V \,\vdash\, \lnot U \qquad \text{)} $$ taken as "axioms". Intuitively it seems to me a valid inference, but I don't quite see how the first sequent can be obtained from the latter two using the various rules of introduction, elimination, cut, and so on.

(I wrote "axioms" in quotation marks because Takeuti defines axiom as a sentence, not a sequent. The starting points above are sequents, not sentences.)

From the texts which I've tried to follow – Takeuti, Negri & von Plato, Ben-Ari – I'm getting the impression that only tautologies can be proved within the sequent calculus; and obviously the first sequent above is not a tautology. But I also remember having read a comment – I think it was in some book by Girard, but I'm not 100% sure – that if one introduced non-trivial axioms in sequent calculus, then the cut-elimination theorem was not valid anymore. Provided I remember correctly, I wonder now if the inference above is one of this kind.

So I have two questions; an answer to either of them should help with the other:

  • Is it possible to draw the inference I mention above within some kind of sequent calculus?
  • Can you suggest a good book that explains such a kind of "sequent calculus with non-trivial axioms"?

Or maybe I'm not making any sense whatsoever?

My question is possibly related to this one or this one, but I haven't been able to understand if they are asking really the same thing, and their answers didn't help me.


Edit: Maybe I've found a proof, but again I don't know if I could call this a proof within sequent calculus: $$ \dfrac{ \varGamma \,\vdash\, U,V \qquad \begin{gathered}[b] \dfrac{ \dfrac{ \varGamma, \lnot V \,\vdash\, \lnot U }{ \varGamma \,\vdash\, \lnot U,V } }{ \varGamma,U \,\vdash\,V } \end{gathered} }{ \dfrac{ \varGamma, \varGamma \,\vdash\, V,V }{ \varGamma \,\vdash\, V } } $$ the second-last step being a cut?

$\endgroup$
0

1 Answer 1

Reset to default
1
$\begingroup$

Using Negri/Von Plato

(a) obtain that $\Gamma \vdash u, v$.

(b). now obtain via inversion from $\Gamma, \neg V \vdash \neg U$ that $\Gamma, U \vdash V, \bot$.

in detail: apply inversion with Rconditional, then Lconditional

(c) by cut obtain $\Gamma \vdash V, \bot$. Now use $\Gamma, \bot \vdash V$ with cut again to conclude.

$\endgroup$
2
  • $\begingroup$ Thank you for the proof, it's useful but doesn't quite answer my question: is this still sequent calculus? Mabye you can add some explanation on this point? $\endgroup$
    – pglpm
    Commented Jun 9, 2023 at 5:36
  • $\begingroup$ yes, this is sequent calculus. as for axioms- all sequent calcluli have axioms- thats how derivations are started in the first place. perhaps you mean nonlogical axioms, in which case I believe negri/von plato cover this in ch 6 of their intro text $\endgroup$
    – emesupap
    Commented Jun 11, 2023 at 5:26

You must log in to answer this question.

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