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