Mathematics Stack Exchange
Mathematics Stack Exchange

Questions tagged [sequent-calculus]

For questions concerning sequent calculus, a formal proof system originally introduced by Gerhard Gentzen in 1933/1935 and studied in the framework of proof theory.

This tag is for questions concerning sequent calculus rules and proofs. Sequent calculus is a tool in proof theory explicitly designed for investigations of logical consequence and derivability.

Sequent calculus is strictly linked to the other Gentzen's big discovery: natural deduction. In sequent calculus systems, there are no temporary assumptions that would be discharged, but an explicit listing of the assumptions on which the derived assertion depends.

The derivability relation, to which reference was made in natural deduction, is an explicit part of the formal language, and sequent calculus can be seen as a formal theory of the derivability relation.

178 questions
13
votes
1 answer

Main differences and relations between Sequent Calculus and Natural Deduction

What are the main differences between the Sequent Calculus and the Natural Deduction (independently of if we're working with classical, intuitionistic or another logic) ? As far as I know : Differences : The sequent calculus is more suitable for…
Boris
  • 719
  • 4
  • 16
10
votes
3 answers

Good textbook for learning Sequent Calculus

There are many modern text books teaching logic using Natural Deduction. There are no books teaching logic using the axiomatic method (see Good book for learning and practising axiomatic logic ) Now in another post (Prove by introduction rules (P ⇒…
Willemien
  • 6,434
  • 4
  • 38
  • 91
8
votes
1 answer

Relationship between sequent calculus and Hilbert systems, natural deduction, etc

I am trying to learn the basics of logic and I'm confused on how these proof systems work together. The big ones I see are Hilbert style, and then Gentzen style which includes natural deduction, and sequent calculus. I also see "intuitionistic…
Brandon L
  • 103
  • 4
7
votes
3 answers

Does double negation distribute over implication intuitionistically?

Does the equivalence $$\neg\neg (P \rightarrow Q) \leftrightarrow (\neg\neg P \rightarrow \neg\neg Q)$$ hold in propositional intuitionistic logic? In propositional classical logic the equivalence holds obviously since $P \leftrightarrow \neg\neg…
Z. A. K.
  • 7,858
  • 1
  • 10
  • 30
6
votes
1 answer

Linear logic and linearly distributive categories

1. Context On page two of the introduction to their paper Weakly distributive categories on linearly distributive categories Cockett and Seely write: It turns out that these weak distributivity maps, when present coherently, are precisely the…
M.C.
  • 2,755
  • 1
  • 7
  • 38
6
votes
1 answer

In linear logic sequent calculus, can $\Gamma \vdash \Delta$ and $\Sigma \vdash \Pi$ be combined to get $\Gamma, \Sigma \vdash \Delta, \Pi$?

Linear logic is a certain variant of sequent calculus that does not generally allow contraction and weakening. Sequent calculus does admit the cut rule: given contexts $\Gamma$, $\Sigma$, $\Delta$, and $\Pi$, and a proposition $A$, we can make the…
Tanner Swett
  • 9,377
  • 29
  • 52
6
votes
1 answer

What does conditional tautology mean?

Does conditional tautology mean a tautology which hast the form of $(A)\rightarrow (b)$ and therefore $A \lor \lnot A$ is unconditional tautology? (in regards to the following paragraph from wikipedia about sequent calculus:…
K. Smith
  • 137
  • 7
6
votes
1 answer

Understanding the meaning of $\forall,\exists$ rules in sequent calculus.

I'm stucking in understanding the usage and soundness of the rules for the quantifiers $\forall,\exists$ in sequent calculus. $\forall-L$: $~~~~~\dfrac{\Gamma,\phi[t]\vdash \Delta}{\Gamma,\forall x\phi[x/t]\vdash\Delta}$…
Eric
  • 4,417
  • 1
  • 15
  • 29
5
votes
1 answer

Does an inference rule under natural deduction operate on sequents or formulas?

In natural deduction, is it correct that an inference rule operates on sequents which have only one formula on their right hand sides? Why does an inference rule seem to operate on formulas in Hurley's An Concise Introduction to Logic? For…
Tim
  • 45,716
  • 51
  • 220
  • 492
5
votes
1 answer

Natural deduction vs Sequent calculus

I don't understand some rules of natural deduction and sequent calculus. (red) The rule makes sense to me for ND but not for SC. In SC it says "if $\Gamma,\varphi$ proves $\Delta$ then $\neg\varphi,\Delta$". So I guess the comma on the right of…
H. Walter
  • 969
  • 4
  • 9
5
votes
1 answer

Why is the left-intro rule in Sequent Calculus equivalent to elimination rule in Natural Deduction?

I have been reading Florian Steinberger's PhD thesis on harmony in sequent calculus, when he asserts that the left-intro rule is functionally equivalent to elimination rule. His argument is attached at the bottom, but there are two things I don't…
Constantly confused
  • 1,456
  • 1
  • 13
  • 27
5
votes
1 answer

Distributive property of tensor ($\otimes$) over par (⅋) in linear logic

In the setting of linear logic, does the tensor $\otimes$ distribute over the par $⅋$? That is, is it possible to show that $$ A \otimes (B ⅋ C) \stackrel?\equiv (A \otimes B) ⅋ (A \otimes C) $$ holds? If not, what is a counterexample? The…
Andrea Censi
  • 163
  • 6
5
votes
2 answers

Sequent calculus and first incompletness theorem

Wikipedia says that sequent calculus is sound and complete (http://en.wikipedia.org/wiki/Sequent_calculus#Properties_of_the_system_LK). Godel first incompleteness theorem says that system capable of doing arithmetics may not be complete and…
Trismegistos
  • 2,362
  • 1
  • 18
  • 30
5
votes
2 answers

Basic: Sequent definition, and-introduction, and iff

I am reading through "Mathematical Logic by Ian Chiswell & Wilfred Hodges"(amazon, and publisher) So far have it has covered $\land$-Introduction and $\land$-Elimination Sadly this text only has answers to selected solutions, which annoys me to no…
cjh
  • 197
  • 8
5
votes
1 answer

Classical logic without negation and falsehood

It seems to me that Gerhard Gentzen's sequent calculus could just omit negation and falsehood, and still prove any classical tautology in a suitable form. (For a specific formula, falsehood gets replaced by the conjunction of all relevant…
Thomas Klimpel
  • 7,216
  • 1
  • 26
  • 68
1
2 3
…
11 12