# Is there some variant of sequent calculus that allows for non-trivial axioms?

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?

(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$$.
(c) by cut obtain $$\Gamma \vdash V, \bot$$. Now use $$\Gamma, \bot \vdash V$$ with cut again to conclude.