# 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.

158 questions
Filter by
Sorted by
Tagged with
21 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 ...
95 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 (...
122 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, ...
47 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 ...
57 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}\\...
36 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 ...
52 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 ...
18 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 ...
98 views

1 vote
175 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 ...
1 vote
55 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 ...
1 vote
41 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?
95 views

### Trying to understand Sequent Calculus inference rules for quantifiers $\forall$ and $\exists$.

I'm trying to understand any of the LK sequent calculus (logic) inference rules for quantifiers (if I can understand one well enough, perhaps I can use that to inform my understanding of the other ...
75 views

### Substitution in sequent calculus vs substitution in lambda calculus

Wikipedia's Sequent Calculus article defines substitution in LK sequent calculus like this: $A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the ...
65 views

### Clarification regarding substitution in sequent calculus

Wikipedia's Sequent Calculus article states: $A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in formula $A$ with the ...
1 vote
48 views

### Seeking intuition for LK sequent calculus ${\rightarrow}L$ inference rule

This Wikipedia article states the LK (${\rightarrow}L$) rule as: $$\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi \over \Gamma, \Sigma, A \rightarrow B \vdash \Delta, \Pi$$ I'm trying to find ...
1 vote
43 views

### Is there a way to prove the cut rule in LK sequent calculus without converting to implications?

The cut rule is given as follows by these two wikipedia articles 1, 2: $$\Gamma \vdash \Delta, A \qquad \Sigma, A \vdash \Pi \over \Gamma, \Sigma \vdash \Delta, \Pi$$ I have the following proof which ...
77 views

### How does one write a sequent calculus sequent with an empty cedent?

How does one write $P \land Q$ in sequent calculus? This would require an empty succedent/consequent? $$P, Q \vdash$$ or $$P, Q \vdash \bot$$ ? An empty consequent represents the disjunction ($\lor$) ...
79 views

### Sequent Calculus vs Natural Deduction

Can I prove all implication proofs like $A \to A$ or $A \to B \to A$ in both Sequent Calculus and Natural Deduction or just in one of them? So for $A \to A$ can I use the right implication ...
1 vote
76 views

### How does this formula $A\lor (A\to B)$ relate to intuitionistic logic?

It is my first approach to the proof theory of intuitionistic logic and I am considering a single-conclusioned Gentzen-style sequent calculus for it, namely $\bf G3i$ (Negri, Von Plato, Structural ...
1 vote
113 views

### false introduction sequent calculus?

I'm proving the following proposition using sequent calculus. I got stuck at the very top line. My thought is that if the both hypothesis inside the curly bracket are true, then it's false. So I think ...
80 views

### Rules of inference for exclusive disjunction and logical biconditional

Here are the rules of inference in natural calculus of propositions. I'd like to extend this calculus (conservatively) adding exclusive disjunction $\oplus$ and logical biconditional $\sim$ and obtain ...
1 vote
59 views

### Proving Sequent Calculus Statement

I have to prove the sequent $$\vdash (\lnot A \lor \lnot B) \to \lnot (A \land B)$$ using the inference rules for natural deduction listed here (pp. 7-8). I'm super new to natural deduction and ...
55 views

64 views

### Deduction rules involving set $\Gamma$ of premises versus elementary textbook natural deduction rules. How do they differ exactly?

In elementary textbooks, natural deduction rules are presented in the following way, say, for $\&$-Intro from $\phi$ and $\psi$, infer $\phi\&\psi$ or $(n).....\phi$ $(m)....\psi$ $\therefore$ ...
86 views

### Sequent calculus: $0<1$

Considering the axioms of real closed ordered fields, I'm having trouble proving $0<1$ using Gentzen sequent calculus enriched with the cut rule, i.e, $$\text{Ax}_{\text{RCOF}}\vdash 0<1.$$ ...
66 views

121 views

### How to establish the modus ponens inference rule in the LK sequent calculus for first-order logic? [closed]

How can the modus ponens inference rule $$\frac{\Gamma \vdash \varphi\hspace{1cm}\Delta\vdash \varphi\rightarrow\psi}{\Gamma,\Delta \vdash \psi}$$ be established in the LK sequent calculus for first-...
88 views

### Question on topic over "Aboutness theory appendix" by Stephen Yablo.

i would need some help in understanding Yablo's theory of subject matter as expressed in his book "Aboutness". Yablo has uploaded an appendix on his academia.edu profile that serves as a ...
274 views

### Does sequent calculus have axiom?

Are axioms inference rules without assumptions, or not inference rules at all? I heard that sequent calculus doesn't have axioms, is that true? p69 in §6. Summary and Example in IV. A Sequent ...
1 vote
42 views

### Confused about the ground rules of sequent calculus (LK): cut or no cut?

There are many books and internet tutorials about sequent calculus for classical first-order logic (LK – which, if I understood correctly, is the one that allows for any number of formulae on the ...
162 views

### The interpretation of $\nvdash$

I have a question about the use of $\nvdash$. $\nvdash$ is commonly used as a meta-level symbol. Let $A\vdash\perp$, by the deduction theorem, we reach $\vdash A\rightarrow\perp$, which is equivalent ...
72 views

### How to derive ${ A \vdash C }$ from ${A \lor B \vdash C}$ in the sequent calculus LK?
How to derive ${ A \vdash C }$ from ${A \lor B \vdash C}$ in the sequent calculus LK? It seems obvious that if ${A \lor B \vdash C}$ is true, then ${ A \vdash C }$ is true. There are rules \$\cfrac {...