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.

0
votes
1answer
40 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
75 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 ...
1
vote
1answer
41 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
28 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
41 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
93 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
75 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
48 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
55 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
64 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
60 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
36 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
105 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
99 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
118 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
134 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
55 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
40 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}...
2
votes
1answer
99 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
74 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
98 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
82 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
68 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
238 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
43 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
97 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
151 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
309 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
86 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
232 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
313 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
126 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
82 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
48 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 ...
1
vote
3answers
90 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
84 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
48 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
235 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
114 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
77 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
37 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
761 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 : ...
1
vote
1answer
88 views

Does every logic have sequent calculus, if not - what are alternatives to them? What prohibits to make general sequent calculus for universal logic?

Does every logic have sequent calculus, if not - what are alternatives to them? What prohibits to make general sequent calculus for universal logic? The question arises in several application domains....
0
votes
1answer
205 views

Rules introducing quantifiers in sequent calculus: a question about notation

I have a (possibly really stupid) question about sequent calculus. My problem is that I am not able to figure out an intuitive explanation of the particular form in which I always find presented the ...
2
votes
1answer
40 views

Restricting left side formulas in sequents

It is well known that if we restrict the right side part of sequents to be single formulas, we obtain intuitionist logic. What happens if we restrict left side part in sequents to have only one ...
2
votes
1answer
59 views

Gentzen's system of sequents provability

$\{p,q\to p,\neg q\}\vdash\{p,q\}$ Is it provable in Gentzen's system ? My trial: $$\frac{p\vdash p,q\ \ \ \ \ \ \ \ \ \ \frac{p\vdash p,q}{p,\neg q\vdash p,q}}{p,q\to p,\neg q\vdash p,q}$$ So, I ...
3
votes
1answer
53 views

Can I derive $ \vdash \Gamma $ from $ \vdash \Gamma, A, A^\bot $?

The Wikipedia article on linear logic mentions the following as an initial sequent: $$ \over \vdash A, A^\bot $$ As far as I can understand from informal descriptions of linear-logic semantics, this ...
2
votes
1answer
106 views

If Γ,A∧B⊢Δ is an axiom, then also Γ,A,B⊢Δ is an axiom

Context I am studying sequent calculus, and I am trying to understand the proof that the rule L∧ introducing "$\land $" on the left: ${\displaystyle \quad {\cfrac {\Gamma ,A,B\vdash \Delta }{\Gamma ,...
1
vote
1answer
69 views

Showing that $(p \lor q) \vdash \lnot (p \land q)$

If $p \lor q$ means that $p$ is true, $q$ is true, or both are true. Then why can $p \lor q \vdash r$ be proved by proving $p \vdash r$ and $q \vdash r$, without proving $p \land q \vdash r$? Wouldn'...