Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

1
vote
0answers
17 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
42 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 ...
0
votes
0answers
15 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 (...
0
votes
1answer
24 views

Is the following derivation of $\{(\phi\to\psi),(\phi\to\chi)\}\vdash (\phi\to(\psi\wedge\chi))$ correct?

It is required to write a derivation to prove $\{(\phi\to\psi),(\phi\to\chi)\}\vdash (\phi\to(\psi\wedge\chi))$. The following is my attempt. Here, $\to E$ is Implication Elimination, $\wedge I$ is ...
2
votes
1answer
51 views

Why is the right implication rule of multi-succedent intuitionistic sequent calculus (LJm) not invertible?

On page 57 of A Short Introduction to Intuitionistic Logic (Mints), the author provides an exercise: prove that the right implication rule is not invertible. By an invertible rule he means: if the ...
3
votes
0answers
35 views

Why can't the sequent calculus for First-Order Classical Logic be used for proving decidability via Proof-search?

I understand that Turing reduced the halting problem to the satisfiability problem of first-order logic thus proving first-order logic undecidable. However, when thinking about the sequent calculus ...
2
votes
1answer
69 views

Calculation of cut height/depth of a cut in Sequent Calculus

I am having trouble understanding the calculation of an idea, which is called 'cut height' in Negri and von Plato's Structural Proof Theory (SPT), and 'depth of a cut' in Troelstra and Schwichtenberg'...
1
vote
2answers
50 views

Prove distribution of or over implies knowing the implication is always true

I was given a task to construct a Hilbert-style proof for the following: $A → B ⊢ C ∨ A → C ∨ B$ I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use ...
1
vote
1answer
83 views

Inversion lemma proof

I am following Structural Proof Theory by Negri and others, and I don't understand the Inversion Lemma proof (i) (the system is G3$_{ip}$, which is the same as G3$_i$ only that it excludes quantifier ...
2
votes
1answer
45 views

Provide sequent calculus proofs of the axioms of the $\{→,∀,⊥\}$-fragment of the Hilbert system $H_c$

Could anyone please help me to understand what the question is asking? Theorem: G1$_i$ + Cut $\vdash \Gamma \Rightarrow A$ iff H$_i$ $\vdash \Gamma \Rightarrow A$ 1) Prove equivalence of G1$...
1
vote
1answer
31 views

Regarding L$\to$ rule in sequent calculus and difference between G1$_c$ and G1$_i$ system

I am going through Troelstra and Schwictenberg's Basic Proof Theory, and I can understand most of the sequent calculus rules by finding some sort of parallel between the rule and a corresponding ...
2
votes
1answer
47 views

Why is “If ψ ∈ Γ then the sequent (Γ ⊢ ψ) is correct” true?

In Chiswell and Hodges Mathematical Logic the authors define a sequent as such "A sequent is an expression (Γ ⊢ ψ) (or Γ ⊢ ψ when there is no ambiguity) where ψ is a statement (the conclusion ...
2
votes
1answer
118 views

Relationship between sequent calculus and Hilbert systems, natural deduction, etc

I am trying to learn the basics of logic and I'm confused on how these proof systems work together. The big ones I see are Hilbert style, and then Gentzen style which includes natural deduction, and ...
2
votes
0answers
46 views

Terminology for free variables

Suppose you have a proof along the lines of $$\begin{array} {rc} \text{Assume:} & x > 2 \\ & \vdots \\ & \text{Some logic stuff} \\ & \vdots \\ \text{Conclude:} & x > 1 \\ \...
2
votes
1answer
79 views

Intuitionistic logic and derivation

It is my first approach to intuitionistic logic (IL) and, even if I understand the principle behind it, I struggle understanding when a sequent is derivable in IL and when is not. I know that IL ...
0
votes
1answer
51 views

Need help for a proof ( sequent calculus )

I have to prove the following: $$\vdash((A \to B) \land (B \to A)) \to (A \leftrightarrow B)$$ But I'm totally stuck here after using introduction of implication and introduction of equivalence: \...
0
votes
0answers
56 views

McNaughton functions and hypersequents for Lukasiewicz logic

For this question, all definitions are borrowed from Proof theory for fuzzy logics (2008) by Metcalfe, Olivetti, and Gabbay. Consider a propositional language over $\{\rightarrow,\bot\}$ for infinite ...
2
votes
1answer
78 views

Hilbert systems and natural deduction systems in terms of “context”

I was reading the Wiki article on Hilbert systems and came across this passage: A characteristic feature of the many variants of Hilbert systems is that the context is not changed in any of their ...
1
vote
2answers
63 views

Soundness of cut in Gentzen's System LK

I'm learning the sequent calculus in the classical setting (Gentzen's System LK), and I am a little confused about how to understand the soundness of Cut. As I understand it, for a given sequent, we ...
2
votes
1answer
37 views

sequent calculus for first order logic

I've just started learning sequent calculus. Now I'm trying to prove the formula below: $$ \exists x (P → Q) ⊨ P → \forall x Q $$ My approach to the problem: $$ \underline{_⊢\exists x (P → Q) , _⊣ P ...
0
votes
1answer
119 views

Proof of the deduction theorem in sequent calculus

Can anybody recommend me a text, where the deduction theorem for predicate logic is proved in LK? I mean the following proposition: if $A$ is a closed formula, and $B$ is arbitrary, then the ...
2
votes
0answers
103 views

For every formula of linear logic, is there an equivalent formula in intuitionistic linear logic?

Consider the sequent calculus presentations of propositional linear logic (LL) and propositional intuitionistic linear logic (ILL). Clearly, there are formulas in LL that are not in ILL, such as $\bot$...
3
votes
3answers
121 views

Comma in turnstile (entailment)

In a sequent, on the left and right-hand side of the turnstile operator, does the comma denote disjunction or conjunction? $$\frac{...}{\Delta_1,\Delta_2 \vdash \Gamma_1,\Gamma_2}$$ I think it's one ...
1
vote
2answers
144 views

Use logical deduction to show that the following propositions are unconditionally true

These two questions: 1) $P \to ((Q \lor R) \to P)$ and 2) $(P \to (Q \to R)) \to ( P \land Q \to R)$ It'd be really helpful if you could answer these for. I managed to answer the ones that give ...
1
vote
1answer
69 views

Is cut rule an instance of left implication?

I'm working with a sequent caluculus system where cut-rule is defined as follows: $$\begin{array}{lcr} \Gamma \Rightarrow \varphi, \Delta & & \Gamma, \varphi \Rightarrow \Delta \\ \hline &...
1
vote
2answers
42 views

Why does the inference rule of negation moves a term to the other side of the turnstile

the excellent tutorial http://logitext.mit.edu/tutorial presents the negation inference rule like so: \begin{align} \frac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \lnot_L \end{align}...
1
vote
1answer
104 views

How to understand this mathematical notation?

We were introduced to these rules during class and not sure how to grasp it. And what does this symbol mean ⊢? UPDATE: Added rules 1a and 1b Rule 1a: if the goal list has a proposition that is also ...
2
votes
2answers
75 views

Why is there a limitation on the existential introduction in sequent calculus?

In sequent calculus there is the rule $\exists \vdash$ $~~~~~\dfrac{\Gamma,\phi[y]\vdash \Delta}{\Gamma,\exists x\phi[x/y]\vdash\Delta}$ with the limitation that y is not used in any of the formulas ...
0
votes
1answer
105 views

Prove TRUE is derivable (or provable) from the Empty Set (Ex 3, Sec 1.4 in “A Concise Introduction to Mathematical Logic” by Rautenberg.)

I've being trying to understand more about logic. My reference book is "A Concise Introduction to Mathematical Logic" by Wolfgang Rautenberg. Now I'm having troubles with exercise 3 in section 1.4. In ...
4
votes
1answer
83 views

How can we interpret that $A, B \vdash A, B$ is unprovable with resource interpretation in Linear Logic?

In Linear logic (LL), it is unprovable but when considering the resource interpretation it seems to me that from the resources $A, B$ we can produce the resources $A, B$. By $A, B \vdash A, B$ I mean ...
3
votes
1answer
70 views

Proving Negation Identity in Intuitionistic Linear Logic

In a Gentzen system (i.e. sequent calculus) for Intuitionistic Linear Logic (from now, ILL), given the usual rules for ILL ($\wedge L, \wedge R, \circ L, etc.$), I want to prove that the Identity $A \...
1
vote
1answer
272 views

What does conditional tautology mean?

Does conditional tautology mean a tautology which hast the form of $(A)\rightarrow (b)$ and therefore $A \lor \lnot A$ is unconditional tautology? (in regards to the following paragraph from ...
2
votes
0answers
44 views

Isabelle/HOL sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont

I am trying to understand https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html and https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/...
3
votes
1answer
105 views

Completeness of the Gentzen Sequent Calculus

Let $A_1, \dots, A_n ,B_1, \dots, B_m \in \mathcal{F}_{¬,\lor}$ with $\models \lnot A_1 \lor \ldots \lor \lnot A_n \lor B_1 \lor \ldots \lor B_m$ ($\mathcal{F}_{¬,\lor}$ is the set of formulas built ...
4
votes
1answer
173 views

Understanding the meaning of $\forall,\exists$ rules in sequent calculus.

I'm stucking in understanding the usage and soundness of $\forall,\exists$ rules in sequent calculus. $\forall-L$: $~~~~~\dfrac{\Gamma,\phi[t]\vdash \Delta}{\Gamma,\forall x\phi[x/t]\vdash\Delta}...
2
votes
1answer
323 views

A sequent calculus proof

Consider the sequent calculus (with multiplicative contexts) defined by the following rules (without contraction and weakening). The sequent calculus is taken from p.23 here: http://users.ox.ac.uk/~...
1
vote
0answers
94 views

Sequent calculus for propositional logic

I think the propositional calculus must have a translation into the language of Gentzen's sequent calculus. I suppose, to obtain Gentzen's version of this we should just remove from LK the rules with ...
1
vote
0answers
255 views

A method for proving sequents in natural deduction sequent style using solely elimination rules and structural rules

In a previous question, Proving a sequent in natural deduction sequent style with elimination rules only, $${p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \...
2
votes
1answer
332 views

Proving a sequent in natural deduction sequent style with elimination rules only

Can we derive $${p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} \neg \thinspace q \hspace{0.2cm} \vdash \hspace{0.2cm}\bot}$$ using $\textit{...
1
vote
1answer
131 views

Grigori Mints' ADC method of proof search for a natural deduction in “sequent-style” calculus

My question regards a proof search procedure, ADC, for a natural deduction in sequent style calculus: See Grigori Mints, A short introduction to Intuitionistic logic (2000): 2.6. Direct Chaining and ...
0
votes
1answer
87 views

Sequents and Consequences

Recently I posted a question concerning the Deduction Theorem. However, I have seen rules written in sequent notation as well (i.e. φ⊢ψ⊢φ→ψ). I am confused as ...
1
vote
0answers
53 views

intermediate calculus between Natural and Sequent Calculus

So as to formalize arithmetic, Gentzen uses an intermediate calculus between the two basic calculi NK and LK. In such calculus, for example, one can deduce $\supset$-elimination rule: $\Delta,\Gamma ...
2
votes
3answers
95 views

Is this sequent rule unacceptable?

In [Mathematical Logic] by Chiswell and Hodges, within the context of natural deduction and the language of propositions LP (basically like here) it is asked to show, by counter-example that a certain ...
1
vote
2answers
94 views

Implication Introduction in reverse way

In Gentzen system, there is an inference rule such that one can deduce $\Gamma \to \Delta, \mathfrak{A} \supset \mathfrak{B}$ from $\Gamma, \mathfrak{A} \to \Delta, \mathfrak{B}$. Can we, in ...
1
vote
1answer
49 views

How to express Syllogism in Sequent Calculus?

I am playing with Sequent Calculus(Just started studying it) and I want to know how to express the Syllogism: Socrates is a Man. All Men are Mortal. Therefore Socrates is a Mortal. In terms of ...
1
vote
1answer
248 views

Sequent calculus, how to prove double negation introduction and conjunction

I want to prove double negation introduction in sequent calculus using the most basic rule set. That is what I want to prove: from the sequent $$\Gamma \rightarrow\Phi,$$ the sequent $$\Gamma \...
2
votes
0answers
119 views

Substitution in Gentzen sequent calculus

In an answer to this question a substitution lemma is mentioned, namely If the sequent $\Gamma \Rightarrow F$ is derivable and a term $t$ is free for a variable $x$ in $\Gamma,F$, then $\Gamma[x \...
1
vote
1answer
88 views

discharge assumption in another branch

I am self studying from Chiswell & Hodges mathematical logic, and I have a general question about discharging assumptions. To demonstrate, I am using exercise 2.5.1(c), which asks for a proof of: ...
0
votes
1answer
38 views

Why is this sequent generalization valid?

In Takeuti's Proof Theory, he has a sequent rule that from $\Gamma \rightarrow \Delta, F(a)$ where $a$ is a free variable, one can infer $\Gamma\rightarrow \Delta, (\forall x)F(x)$. This seems like ...
6
votes
1answer
833 views

Main differences and relations between Sequent Calculus and Natural Deduction

What are the main differences between the Sequent Calculus and the Natural Deduction (independently of if we're working with classical, intuitionistic or another logic) ? As far as I know : ...