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.

Filter by
Sorted by
Tagged with
1 vote
1 answer
56 views

Examples of sequent derivations that uses cut rule that can be modified to not to use cut rule?

The cut-elimination theorem states that any sequent calculus derivation that uses the cut rule also has a derivation that does not use the cut rule. I cannot find any explicit examples of such ...
John Davies's user avatar
-1 votes
0 answers
75 views

Deriving $\Phi\vdash\Delta$ from $\lnot\lnot\Phi\vdash\Delta$ without cut rule?

I revisited the old post of mine and I am confused with the answer. The cut elimination theorem states that for any sequent that is derived with cut rule, there exists a derivation of the same sequent ...
John Davies's user avatar
2 votes
1 answer
72 views

Use sequent calculus to show if $\Gamma\vdash t_1=t_2$ then $\Gamma\vdash f(t_1)=f(t_2)$

Suppose the sequent $\Gamma\vdash t_1=t_2$ where $t_1,t_2$ are closed terms. Let $f$ be a one-place function symbol. I am trying to find a sequent calculus derivation of $\Gamma\vdash f(t_1)=f(t_2)$ ...
John Davies's user avatar
1 vote
1 answer
31 views

Showing $\Gamma\vdash A$ and $\Gamma\vdash \lnot B$ from $\Gamma\vdash\lnot (A\to B)$ using sequent calculus

Suppose $\Gamma\vdash\lnot (A\to B)$. How do I show that both $\Gamma\vdash A$ and $\Gamma\vdash \lnot B$ using sequent calculus inference rules? Here is my attempt to obtain $\Gamma\vdash A$: From $\...
John Davies's user avatar
1 vote
1 answer
79 views

Double negation in sequent calculus

Kind of related to this post. I wonder if it is possible to derive $\Phi\vdash\Delta$ from $\lnot\lnot\Phi\vdash\Delta$ using standard sequent calculus elimination rules. I am not sure where to start. ...
John Davies's user avatar
1 vote
1 answer
78 views

Why is there no conditional inference rule in Sequent Calculus of these forms?

I'm wondering why sequent calculus doesn't have rules like these (at least in the ones I've come across): $$ \Gamma \vdash A \rightarrow B, \Pi \qquad \Delta \vdash A, \Sigma \over \Gamma, \Delta \...
confusedcius's user avatar
3 votes
1 answer
92 views

Question about quantifiers in the proof of the cut eliminiation theorem

Lately I have been reading about the cut elimination theorem, I think I get the idea however I have been struggling with some technical details concerning quantifiers. Consider the following rule: ...
Le Grand Spectacle's user avatar
1 vote
0 answers
47 views

Property Equivalent to Maximally Consistent

This is a question about Gentzen calculus. $X$ is a set of formulas with the symbols $\{\lnot, \land\}$, and $a$ is such a formula. On page 27 of "A Concise Introduction to Mathematical Logic&...
Enrico Borba's user avatar
0 votes
1 answer
53 views

Clarification for a rule in this sequent calculus

I'm reading through Ebbinghaus' Mathematical Logic and more specifically chapter 4 where a sequent calculus is constructed. Below is the rule I need clarification on because, according to my ...
iwjueph94rgytbhr's user avatar
0 votes
1 answer
73 views

Showing if $A[y/x]\models\Delta$ then $\exists x A(x)\models\Delta$

In order to better understand the tricky $\exists L$ rule and its eigenvariable requirement from sequent calculus: $$\Gamma, A[y/x] \vdash \Delta \over \Gamma, \exists xA \vdash \Delta$$ I decided to ...
John Davies's user avatar
1 vote
1 answer
59 views

Making sense of eigenvariable restriction in $\exists L$ rule in sequent calculus

I still cannot understand why the $\exists L$ rule from sequent calculus is sound: $$\Gamma, A[y/x] \vdash \Delta \over \Gamma, \exists xA \vdash \Delta$$ Intuitively I can explain this rule as "...
John Davies's user avatar
5 votes
0 answers
170 views

Proving $\exists x[P(x)] \to \exists y[\exists x[P(x)]\to P(y)]$ in for intuitionistic $\varepsilon$-calculus.

I am researching Mint's paper: Intuitionistic Existential Instantiation and Epsilon Symbol (this is as far as I know unfinished work) In intuitionistic logic, it is not difficult to prove that $$\...
Tungsten's user avatar
  • 130
0 votes
0 answers
38 views

Understanding quantifier rules in sequent calculus [duplicate]

I am trying to learn sequent calculus for a while and for the life of me, I cannot make sense of the below quantifier rules for sequent calculus: $L$ $R$ $\forall$ $$\Gamma, A[t/x] \vdash \Delta \...
John Davies's user avatar
3 votes
1 answer
127 views

What is the metatheory required for proving the cut-elimination theorem for classical logic? Is the proof circular?

I am new to proof theory, and I am curious about the tools required in the proof of cut-elimination for the sequent calculus. I understand how the proof operates informally: a main induction on the ...
MotDave's user avatar
  • 33
1 vote
1 answer
43 views

What is the correct way to interpret the Intuitionistic rules of Kleene's sequent (Gentzen) system G1 (in sec. 77 of Kleene I.M. 1952)

I'm having difficulty understanding the sequent/Gentzen proof system in section 8 of a paper by Gurevich [G1977], and he defines that system by telling the reader to modify the system G1 from Kleene's ...
tuiowalu's user avatar
1 vote
1 answer
96 views

Exchange case in proving interpolation theorem by induction on the length of proof tree

I'm trying to prove Craig's interpolation theorem of propositional logic using Maehara's method by induction on the length of proof tree using sequent calculus. the theorem is as stated below: $$ \...
asha soroushpoor's user avatar
1 vote
1 answer
85 views

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, ...
pglpm's user avatar
  • 831
2 votes
0 answers
39 views

Sequents in which succedents are restricted to one formula

In the original version of Sequent Calculus by Gentzen for classical and intuitionistic propositional logic there is a structural difference: the classical version admits succedents with multiple ...
effezeta's user avatar
  • 445
2 votes
0 answers
33 views

Equivalence of Martin-Löf sequent calculus and standard sequent calculus with material implications

I have a question about the proof system of Per Martin-Löf, developed in his paper "Hauptsatz for the intuitionionistic theory of iterated inductive definitions". In this paper, Martin-Löf ...
RobbeVB's user avatar
  • 21
1 vote
1 answer
67 views

Establishing $\Gamma, A: Type \vdash (A)Type\ \textbf{kind}$ in LF

This is a follow-up to my previous question. Consider the same LF as in that question: LF is a simple type system with terms of the following forms: $$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$ ...
user avatar
1 vote
0 answers
59 views

Reflection principle for finite subsystems of PA.

I would like to clarify the reasoning behind the proof of reflection schema for finite subsystems of PA that I found in "The Blind Spot" book. To be wore precise, we have a finite subsystem $...
A. G's user avatar
  • 328
1 vote
1 answer
93 views

Is there a G4ip equivalent for first-order logic?

G4ip is a sequent calculus for propositional logic (by Dyckhoff) that is contraction-free, thus (if I understand correctly) greatly simplifying the writing of automated theorem provers by avoiding ...
vigoux's user avatar
  • 13
0 votes
0 answers
62 views

Proof in Natural Deduction, Sequent Calculus or Hilbert System

Is there any smart way to check if certain statements are not provable in any of these proof systems? Like for example the following task: Prove or disprove the following statements: $\vDash \exists ...
jjbinks's user avatar
  • 71
0 votes
2 answers
100 views

Adding $\tfrac{}{\Gamma \varphi}$ (for a fixed non-correct $\Gamma \varphi$) to the rules of the sequent calculus, can one now derive every sequent?

One knows that the sequent calculus over the set of sequents $\Gamma \varphi$ is correct and complete, meaning that the derivable sequents are precisely the correct ones. However, adding just one ...
Hypatius's user avatar
1 vote
0 answers
106 views

Prove "proof by contradiction" from $L_0$

Basically, I was reading the comments to Equivalence of Deductive System $L_0$ and the Sequent Calculus and Mauro says that PC is A3 in sequent form. I don't quite understand this. Can someone please ...
You1234's user avatar
  • 301
-3 votes
1 answer
60 views

Doing formulas on sequent calculus

JAre we allowed to equivalence rules on sequential calculus that isn't structural or logical, for example, can I do deMorgans on the red arrow to make it ~p1 ∧ ~p2 |-- ~p2? Formula
Julefikar's user avatar
3 votes
1 answer
232 views

Curry-Howard Isomorphism For Classical Logic

I wonder if there is some direct proof of how $\lambda$-$\mu$-calculus maps to classical logic via the Curry-Howard correspondence. Just like one can verify a valid sentence in propositional logic by ...
fweth's user avatar
  • 3,574
0 votes
0 answers
59 views

Replacing a term in a sequent by a variable

I'm going through 'Proof Theory' by Gaisi Takeuti (second edition 1987). Theorem 6.9 on page 34 talks about when one can replace all occurrences of a term $t$ in a provable sequent $S$ by a free ...
gkb0986's user avatar
  • 131
3 votes
1 answer
157 views

Proof of cut-elimination for a propositional calculus?

Consider the classical propositional calculus over the alphabet $\{\bot,\top,\neg,\land,\lor,\rightarrow\}$ with the following inference rules (together with the initial sequent): Is cut-elimination ...
Max Demirdilek's user avatar
0 votes
1 answer
61 views

Understanding when to use rules in sequent calculus

Would the proof still work if used $[\lor_{R_1}]$ and $[\lor_{R_2}]$ before $[∃_R]$, in both branches. I assumed appluing $[∃_R]$ to $B$ and $A$ in the respective branches would be redundant since ...
user avatar
0 votes
0 answers
44 views

understanding when to use left right rules sequent calculus

I'm trying to understand this classical Sequent Calculus proof. These are the rules Of Sequent Calculus(version 1) in respect to this question How do we know to use ...
user avatar
0 votes
1 answer
297 views

understanding the implication rule in sequent calculus

I'm trying to understand a proof on sequent Calculus Note: This proof is not yet finished. I don't understand how the 3rd statement(counting from bottom up) is converted into the fourth statement ...
user avatar
0 votes
0 answers
110 views

Sequent calculus as multilinear/tensor algebra?

Settings I have been studying sequent calculus for several months and found that there should be a rule that is seemingly typical, even too trivial, but/hence no one officially mentions: $$ \dfrac{ a ...
Rin's user avatar
  • 1
1 vote
1 answer
75 views

Sequent calculus for classical propositional logic without ⊤ and ⊥

Is there a standard multiple-conclusion sequent calculus for classical propositional logic in the language $\{\neg, \wedge, \vee, \to, \leftrightarrow\}$? Usually $\leftrightarrow$ is excluded, and ...
jdonland's user avatar
  • 197
4 votes
3 answers
492 views

The simplication of left implication rule in intuitionistic sequent calculus

The original left implication rule in sequent calculus for intuitionistic logic is $$ \dfrac{\Gamma, A \supset B \vdash A \quad \Gamma,A \supset B, B \vdash C}{\Gamma, A \supset B \vdash C} $$ There ...
maplgebra's user avatar
  • 377
0 votes
0 answers
63 views

Derivable sequent

I’m currently following the book “Mathematical logic” of Ebbinghaus. He says that a sequent $\Gamma\varphi$ is derivable when exists a derivation of this sequent in the sequent calculus $\mathfrak{S}$ ...
Jesus's user avatar
  • 59
1 vote
1 answer
113 views

Provability of sequents in LK

In his answer to my question Andreas Blass writes: "$A\lor(B\land C)$ doesn't classically imply $(A\lor B)\land C$". I read this as: The sequent $A\lor(B\land C) \vdash (A\lor B)\land C$ is ...
Margaret's user avatar
  • 1,777
4 votes
1 answer
147 views

Natural Deduction: An unusual presentation?

1. Context On page 241 of their paper Natural deduction and coherence for weakly distributive categories Blute et al give the right- and left-introduction rules of multiplicative conjunction for (...
Max Demirdilek's user avatar
6 votes
1 answer
284 views

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, ...
Max Demirdilek's user avatar
3 votes
1 answer
100 views

Is $A ⅋ (B \otimes C) \vdash (A⅋B) \otimes C$ provable in MLL?

Consider the multiplicative fragment of linear logic (MLL) which only consists of the multiplicative connectives tensor and par together with the inference rules axiom, cut, $\otimes$ and ⅋. I was ...
Margaret's user avatar
  • 1,777
0 votes
1 answer
64 views

Logical derivations without instantiation rules

I'm trying to, through sequent calculus, prove some derivations without any instantiation rules, but I keep getting stuck. Take, for example, \begin{align} &\text{All basketball players are tall}\\...
FazeZizek's user avatar
  • 332
0 votes
0 answers
99 views

How to convert a Gentzen Calculus Formula to a Natural Deduction One

I have a proof on my textbook, which prooves denials of quantified propositions ∀xφ ⊨ ¬∃x¬φ... However it is written in Gentzen calculus style, while what I need it a Natural Deduction style one. Can ...
Breno's user avatar
  • 47
0 votes
0 answers
61 views

Are logical rules logics?

When I asked whether the empty logic (the one on which no argument is valid) is axiomatizable, the consensus was that it is, and that it is axiomatized by a proof system having no rules whatsoever. Is ...
jdonland's user avatar
  • 197
0 votes
0 answers
30 views

What does it mean for a sequent to be equivalent to a set of sequents?

Adam Přenosil's article "Cut elimination, identity elimination, and interpolation in super-Belnap logics" contains this proposition: Proposition 3.2. Each sequent is equivalent in the ...
jdonland's user avatar
  • 197
0 votes
2 answers
129 views

Prove using minimal logic that $\neg\neg\neg A \rightarrow \neg A$

Prove using natural deduction for minimal logic that $\neg\neg\neg A \rightarrow \neg A$. I'm trying to prove this argument using only the rules of minimal logic. So far I have this. $$1. ⊢ \neg\neg\...
MR_chep's user avatar
  • 141
2 votes
1 answer
142 views

Prove the following argument $\forall x \exists y (Px → Rxy) ⊢ \forall y (Py → \exists x Ryx)$ using the rules of sequent calculus

Prove the following argument $\forall x \exists y (Px \to Rxy) \vdash \forall y (Py \to \exists x Ryx)$ using the rules of sequent calculus. I've been struggling how to prove this argument. I've tried ...
Massimo2015MX's user avatar
0 votes
1 answer
58 views

How understand in which logic a sequent is provable and in which one is not?

Determine if the following sequent is provable in the classic logic, intuitionistic logic or minimal logic. $$ ( \exists x \psi(x) \rightarrow \forall x \theta(x) ) \vdash \forall x ( \psi(x) \...
3m0o's user avatar
  • 783
1 vote
1 answer
378 views

Natural Deduction Proof search algorithm for Classical Propositional logic?

I know of two algorithms for determining classical propositional validity: Convert the problem into a SAT problem, run a SAT solver. These algorithms are efficient, but it seems difficult/infeasible ...
user1636815's user avatar
1 vote
1 answer
161 views

"forward" natural deduction vs "backward" natural deduction

Updated Question I'm following Interactive Tutorial of the Sequent Calculus which states the rules for "backwards" deduction and comparing it to the rules for "forward" natural ...
joseville's user avatar
  • 1,477
1 vote
0 answers
84 views

Natural Deduction and Sequent Calculus

Are there any good natural deduction and sequent calculus solvers online for both predicate and propositional logic? Or perhaps forums that specialise in these proof systems?
structures9818's user avatar