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