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
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 ...
- 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 (...
- 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, ...
- 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 ...
- 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}\\...
- 43
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 ...
- 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 ...
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 ...
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\...
- 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 ...
- 123
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) \...
- 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 ...
- 99
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 ...
- 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?
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 ...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 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$) ...
- 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 ...
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 ...
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 ...
- 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 ...
- 35
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 ...
- 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 ...
- 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 ...
- 473
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 ...
- 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, \...
- 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 ...
- 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'...
- 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 ...
- 1,120
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.
...
- 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 ...
- 89.2k
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 ...
- 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\...
- 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$
...
- 638
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.$$
...
- 407
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 ...
- 407
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:
$$\...
- 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-...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 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} \...
- 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'...
- 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 ...
- 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 "...
- 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 {...
- 305