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.
130
questions
1
vote
0answers
24 views
How to prove the rule ∀R(universal quantifier induction right) is sound
I am wondering how to prove:
$$ \frac{\Gamma\therefore\Delta,[A]^y_x}{\Gamma\therefore\Delta,\forall x A}\,(\forall\text R)$$
where $y\notin\operatorname{free}(\Gamma\cup\Delta\cup\{\forall x A\})$
...
0
votes
1answer
39 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'...
1
vote
2answers
65 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 ...
0
votes
1answer
42 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.
...
4
votes
1answer
68 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 ...
1
vote
1answer
43 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 ...
2
votes
1answer
58 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\...
0
votes
0answers
27 views
Is the Principle of Explosion valid in $G_0$?
Consider $G_0$, a part of Gentzen's calculus $G$.
Let the alphabet $A$ consist of propositional variables $Q_0, Q_1,\dots;$ logical constant $\mathfrak{F},$ conjunction symbol $\wedge$, negation ...
3
votes
1answer
46 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$
...
2
votes
1answer
76 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.$$
...
0
votes
1answer
63 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 ...
2
votes
1answer
30 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:
$$\...
0
votes
2answers
53 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-...
0
votes
1answer
80 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 ...
2
votes
1answer
127 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
0answers
30 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 ...
3
votes
2answers
90 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 ...
3
votes
1answer
55 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} \...
5
votes
1answer
76 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'...
3
votes
1answer
118 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 ...
3
votes
1answer
84 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 "...
2
votes
1answer
99 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 {...
6
votes
3answers
169 views
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 ...
3
votes
1answer
64 views
Contexts in Natural Deduction
This is my first post. I have a basic question about the use of context in natural deduction. If $A$ is true in an empty context, written as
$\vdash A$
then, by monotonicity, in any context $\Gamma$, $...
1
vote
1answer
31 views
Empty Context in Deduction Theorem
I have a small question about Deduction Theorem. According to Deduction Theorem, we have the following:
$$A\vdash B\ \Leftrightarrow\ \langle\ \rangle\vdash A\rightarrow B.$$
Here I use $\langle\ \...
1
vote
0answers
35 views
Soundness of temporal modal logic rule
I am trying to prove the soundness of a temporal modal logic with this rule:
$$
\dfrac{\Sigma \vdash \Theta}{\bigcirc \Sigma \vdash \bigcirc \Theta}
$$
The semantics given a $\omega$-word $u : \...
2
votes
1answer
111 views
Why use sequents?
In the sequent calculus, the building blocks of a proof are inference rules, which are rules for inferring the validity of certain sequents from other sequents, something like this:
$$\frac{\vec\...
1
vote
1answer
50 views
How to prove (and which deduction systems are necessary/sufficient) the formula $\forall x\exists y f(x)=y$
Let $\mathcal M=\langle M,f\rangle$ be an $\mathcal L$-structure of language $\mathcal L$ that contains $\{=\}$. $f$ is a unary function symbol ($f\subset M\times M$, and $f$ is well defined: $\forall ...
1
vote
0answers
42 views
Prove goal and contradictory assumption satisfiability?
I’m studying for my first logic exam and have some questions regarding proof trees:
In the process of proving the satisfiability of a formula by a proof tree with sequent calculus, I need to close ...
5
votes
1answer
205 views
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,\...
2
votes
1answer
74 views
Discharging Assumptions and Conditional Introduction (Chiswell and Hodges)
I'm currently working through the Chiswell and Hodges Mathematical Logic and found myself a little puzzled by a particular natural deduction issue for ($\to$I). The exercise I'm a little stuck on ...
0
votes
1answer
59 views
Can dummy True/False be in the consequent side of the implication and what it could mean?
It is known that False -> SomeFact is the use of the implication for the representation of the facts in the propositional and first order logic. The Sequent (of ...
0
votes
1answer
24 views
How to avoid elimination of the initial fact when the modus ponens (or the cut rule) is used?
I have FOL knowledge base that describes the actions of some agent:
is_goal(learning)
is_goal(learning)->is_goal(reading)
If both formulas are true then the ...
0
votes
0answers
31 views
Do sequent rules (for first order logic) work in both directions?
Sequent rules allow to create proof obligations from the main formula, that involves some connective, e.g. implication. This is backward chaining strategy for theorem proving. But can I use sequent ...
2
votes
0answers
43 views
Can sequent calculus start with facts and assert facts? I.e. can sequent calculus be used as extended rule engines?
I am reading about sequent calculus https://www.cambridge.org/core/books/structural-proof-theory/487F9F5F1E6174867B458B819043C36B of first order logic and the book states:
Thus sequent calculus ...
0
votes
0answers
37 views
Sequent calculus for classical higher order predicate logic - why not?
I read that there is sequent calculus for second order substructural predicate logic https://link.springer.com/chapter/10.1007/978-3-319-08587-6_5 and sequent calculus for second order (what it means?)...
2
votes
1answer
75 views
Problem with a proof ( sequent calculus)
I have to proof this sequent:
⊢ (p → q) → ((q → r) → ((p v q) → r)))
i ve already done sth like this
...
0
votes
1answer
46 views
How to compute the consequence set of the set of premises for for first order logic?
How to compute the consequence set of the set of premises for for first order logic? I.e. how to compute the right hand side of the judgment given the left hand side. Of course, there are 3 kind of ...
0
votes
1answer
115 views
Confusion about soundness of sequent calculus
I'm currently reading a pdf textbook called Sets, Logic,
Computation An Open Introduction to Metalogic Remixed by Richard Zach, and it covers sequent calculus LK and (partially) proves its soundness. ...
1
vote
1answer
53 views
Difference between free variables and universal quantifiers in predicate logic?
I'm learning about Gentzen's System LK, and the issue with the RHS $\forall$ introduction rule. This rule would allow us to derive the following:
$$\frac{\longrightarrow Pa}{\longrightarrow \forall x ...
2
votes
2answers
229 views
What is the difference between 'true' and 'correct'?
I am reading Chriswell & Hodges which says (p. 7)
A sequent is an expression
$(Γ \vdash ψ)$
where $ψ$ is a statement and $Γ$ is a set of statements. The
sequent $(Γ \vdash ψ)$ means
...
3
votes
1answer
115 views
Relation between classical implication and intuitionistic implication
Recently, I have read an article on combining classical and intuitionistic implications. On page 9, in their Proposition 6, the authors say that
$$A\Rightarrow((A\Rightarrow B)\rightarrow (A\...
2
votes
0answers
140 views
Explaining the eigenvariable condition in sequent calculus
In sequent calculus LK, the right quantifier rule is
$$
\dfrac{\Gamma\vdash[y\backslash x]A, \Delta}{\Gamma\vdash\forall xA, \Delta}\forall\text{R}
$$
where $y$, the eigenvariable, cannot occur free ...
4
votes
1answer
67 views
Index notation in derivation rules
I need some advice on a (fairly rudimentary) notation. Consider the derivation rule
(1) $\qquad\qquad\qquad\qquad \dfrac{k_0, ..., k_n}{A}$.
While it's possible that $k_0 = k_n$, is it possible ...
5
votes
1answer
157 views
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 ...
3
votes
1answer
79 views
Negation Inference with Gentzen Natural Deduction and Sequents?
I'm trying to understand the negation rules of this system.
Wiki's page on Sequent Calculus claims that from:
${\displaystyle \lnot p,p,q\vdash r}$
the following is inferred:
${\displaystyle p,q\...
0
votes
1answer
32 views
Help to prove this formula (Sequent calculus for predicate logic)
I have a formula:
$$¬(\exists x)ϕ(x) ⇒ (∀x)¬ϕ(x) $$
to prove.
If the "$(∃x)ϕ(x)$" was in brackets like this $¬((∃x)ϕ(x))$, I could easily prove this formula, but without it I'm stucked. Can you ...
1
vote
0answers
29 views
Does the order of applying rules in Sequent Calculus matter?
Suppose we want to prove some $\Gamma \models \Delta$ in (first-order logic) sequent calculus LK.
We start with the sequent $\Gamma \vdash \Delta$, and arbitrarily apply rules backward until we reach ...
0
votes
0answers
50 views
classical logic - rules for quantifiers
I have these formulas of CL:
(a) ∀xP(x,x)
(b) ∀x∀y∀z(P(x,y)∧P(y,z) → P(x,z))
(c) ∀x∀y(P(x,y) → ¬P(y,x)
and I have been trying to prove weather (a),(b) ⊨ (c). First I would use ∀l and then my ...
1
vote
0answers
30 views
Is it possible to prove that propositional calculus is consistent using only its syntax?
Let us consider Gentzen's propositional calculus with only one axiom:
$$
\phi \vdash \phi
$$
and 12 rules of inference.
As far as I know this PC is consistent, i.e. not all of their expressions (...
