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