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
0 votes
0 answers
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 ...
user avatar
  • 191
3 votes
1 answer
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 (...
user avatar
  • 1,737
6 votes
0 answers
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, ...
user avatar
  • 1,737
3 votes
1 answer
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 ...
user avatar
  • 191
0 votes
1 answer
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}\\...
user avatar
0 votes
0 answers
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 ...
user avatar
  • 47
0 votes
0 answers
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 ...
user avatar
0 votes
0 answers
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 ...
user avatar
0 votes
1 answer
98 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\...
user avatar
  • 133
2 votes
1 answer
54 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 ...
user avatar
0 votes
1 answer
43 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) \...
user avatar
  • 151
1 vote
1 answer
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 ...
user avatar
1 vote
1 answer
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 ...
user avatar
  • 1,059
1 vote
0 answers
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?
user avatar
3 votes
2 answers
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 ...
user avatar
  • 1,059
0 votes
1 answer
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 ...
user avatar
  • 1,059
3 votes
1 answer
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 ...
user avatar
  • 1,059
1 vote
1 answer
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 ...
user avatar
  • 1,059
1 vote
1 answer
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 ...
user avatar
  • 1,059
0 votes
1 answer
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$) ...
user avatar
  • 1,059
0 votes
1 answer
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 ...
user avatar
1 vote
1 answer
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 ...
user avatar
1 vote
2 answers
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 ...
user avatar
  • 611
2 votes
1 answer
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 ...
user avatar
1 vote
1 answer
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 ...
user avatar
  • 67
2 votes
1 answer
55 views

Undo a weakened statement in sequent calculus later in the inferences

I'm working on an answer to (b) of Mathematical Logic, Ebbinghaus et. al. 1984 p. 64 Consider the following inference: $$ \frac{\begin{align}\Gamma \vdash A\\ \Gamma \vdash B\end{align}}{\Gamma \vdash ...
user avatar
  • 698
1 vote
1 answer
49 views

Sequent type system in which all formulae are closed

In most presentations of the sequent calculus, the formulae that appear in a sequent $\Delta \vdash \Gamma$ may be open; i.e., may have free variables. I am looking for elegant presentations of ...
user avatar
2 votes
1 answer
91 views

Relation between the "signature property", polarities and Sequent calculus in "The Blind Spot" book by J.-Y. Girard.

I'm trying to understand one particular concept from the J.-Y. Girard's book "The Blind Spot" (pages 50-51) where he introduces positive and negative signatures to formulas. So now there are ...
user avatar
  • 180
0 votes
1 answer
38 views

Proving an inference rule in sequent calculus

Is the following rule correct? $\dfrac{\Phi, \varphi \Rightarrow \Delta, \psi}{\Phi, \varphi \rightarrow \psi \Rightarrow \Delta}$ I don't think it is. If I pick $\Phi = \{\top\}, \varphi = \bot, \...
user avatar
  • 575
4 votes
1 answer
84 views

Understanding sequent calculus

Are the following rules correct? $(i)$ $\dfrac{\Phi \Rightarrow \Delta}{\Phi, \psi \Rightarrow \Delta}$ $(ii)$ $\dfrac{\Phi, \psi \Rightarrow \Delta}{\Phi \Rightarrow \Delta}$ Intuitively, I would've ...
user avatar
  • 575
0 votes
1 answer
61 views

First order logic reference request

I need a textbook (or any other material) about first order logic, that includes these precise parts: $LK$ sequent calculus, and substitution. I already searched on Shoenfield and Mendelson and I didn'...
user avatar
  • 2,443
1 vote
2 answers
105 views

Sequent calculus: What does it mean to say “choose the sequents from which we can derive some other sequent via the right conjunction rule”?

My question is probably quite silly really, but I am puzzled what this exercise is asking: Excercise. Choose all sequents from which we can derive some other sequent via the right-side conjunction ...
user avatar
0 votes
1 answer
64 views

Should equality, like any other predicate, involve only bound variables in a valid FOL sentence?

I have found a nice interactive tutorial about sequent calculus. It contains all the inference rules for the first order logic (13 rules in the green box). One can also find these rules on Wikipedia. ...
user avatar
  • 453
3 votes
2 answers
200 views

A question about the (un)derivability of Cut Rule in Sequent Calculus

This question is motivated by a previous discussion regarding How to show that a valid rule is not derivable in Intuitionistic propositional calculus. The reference is to Gentzen (1934-35)'s Sequent ...
user avatar
0 votes
1 answer
81 views

How should sequent calculus be extended if we add equality to the first order logic?

Are sequent calculus needed to be extended if we add equality to the first order logic? Is it not enough to say that we just have one more predicate that has all the properties of equality: $\forall X ...
user avatar
  • 453
2 votes
1 answer
80 views

Generalized Deduction Theorem

In my comment on this question, I mentioned that there was a generalized form of the deduction theorem that looks something like this For any finite set of formulae, $\Gamma$ $$\dfrac{\Gamma\vdash\...
user avatar
  • 3,709
3 votes
1 answer
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$ ...
user avatar
2 votes
1 answer
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.$$ ...
user avatar
0 votes
1 answer
66 views

Gentzen Calculus: Proving $\vdash^G_\Sigma (E3_\cong),(E1),\Gamma\rightarrow \Delta, \forall x_1\forall x_2(x_1\cong x_2\supset x_2\cong x_1)$

I am trying to prove some theorems using Gentzen calculus and have a few questions. For example: Show that $$\vdash^G_\Sigma (E3_\cong),(E1),\Gamma\rightarrow \Delta, \forall x_1\forall x_2(x_1\cong ...
user avatar
2 votes
1 answer
51 views

$\forall xA\Rightarrow A[t/x]$ and rule of left universal quantification in sequent calculus

Consider the rule of left universal quantification in the sequent calculus: $$\dfrac{\Gamma,A[t/x]\vdash \Delta}{\Gamma,\forall xA\vdash\Delta}.$$ This can be used to give the following proof: $$\...
user avatar
  • 243
0 votes
2 answers
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-...
user avatar
  • 10.4k
0 votes
1 answer
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 ...
user avatar
  • 422
3 votes
1 answer
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 ...
user avatar
  • 43.6k
1 vote
0 answers
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 ...
user avatar
  • 784
3 votes
2 answers
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 ...
user avatar
  • 571
3 votes
1 answer
72 views

Proving $\forall x \neg P(x) \implies \neg \exists y P(y)$ in sequent calculus

Having the inference rules $$ \frac{\Gamma, A[x:t] \implies \Delta}{\Gamma, \forall x A \implies \Delta} \forall L $$ $$ \frac{\Gamma, A[x:y] \implies \Delta}{\Gamma, \exists x A \implies \Delta} \...
user avatar
  • 503
5 votes
1 answer
106 views

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'...
user avatar
  • 43.6k
3 votes
1 answer
207 views

Converse of Deduction Theorem

I have a basic question about natural deduction and deduction theorem. I learn from my textbook that the deduction theorem $$\textit{If }\ \Gamma,A\vdash B,\ \textit{ then }\ \Gamma\vdash A\rightarrow ...
user avatar
  • 571
4 votes
1 answer
118 views

What is the definition of "a derivation of a sequent "?

In Chapter IV. A Sequent Calculus in Ebbinghaus' Mathematical Logic, a sequent is defined as: If we call a nonempty list (sequence) of formulas a sequent, then we can use sequents to describe "...
user avatar
  • 43.6k
2 votes
1 answer
127 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 {...
user avatar