Mixing
![Very General question on the idea of categories [closed]](https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEhZCTB4-bb-s-32SAm6ytjzFOU06cH9o8q-a_wq_UnH6lcd8hvws23CmBWHM6g256LzTX9yK1EiCCzTC1NSgtxlNk_J9hdr9bA3tD0Nqntbl521j4bLAm_uXPANuWLBhcCKTKzns2gaUodx/s72-c/1.jpg)
Proof of the deduction theorem in sequent calculus
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
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 existence of a Gentzen tree
$$
fracfracvdash Adotsvdash B
$$
implies the deducibility of the sequent $Avdash B$ (or, equivalently, the deducibility of the sequent $vdash Ato B$).
More generally, I wonder if there are textbooks on logic where the exposition is presented from the point of view of sequent calculus.
logic first-order-logic predicate-logic sequent-calculus
asked Jul 17 at 4:22
Sergei Akbarov
749413
add a comment |Â
up vote
1
down vote
favorite
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 existence of a Gentzen tree
$$
fracfracvdash Adotsvdash B
$$
implies the deducibility of the sequent $Avdash B$ (or, equivalently, the deducibility of the sequent $vdash Ato B$).
More generally, I wonder if there are textbooks on logic where the exposition is presented from the point of view of sequent calculus.
logic first-order-logic predicate-logic sequent-calculus
asked Jul 17 at 4:22
Sergei Akbarov
749413
Mauro, I mean the system LK as it is explained in Wikipedia. This is the same as in Takeuti's book, but he uses different symbols. I hope, my edit clarifies what I need. Do Negri and von Plato prove the deduction theorem in their book?
– Sergei Akbarov
Jul 17 at 9:15
Ok; in Wiki's entry dedicated to sequent calculus, it is used $vdash$ for sequents and $to$ for the conditional. Having said that, the rules are written "upside-down" to be used in tree-form (the proof start from the formula to be proved and decompose it). Having said that, you can see that the $text R to$ rule is like mine below (written upside-down).
– Mauro ALLEGRANZA
Jul 17 at 9:30
Excuse me I've just understood what is supposed to be done here: we should just add $A$ into each antecedent in this tree, and check that the obtained picture $$ fracfracAvdash AdotsAvdash B $$ can be completed to a deduction for the sequent $Avdash B$. For this we have to check that each rule in LK, after adding $A$, can be completed to a Gentzen tree. The condition that $A$ is closed is necessary for checking $forall R$ and $exists L$.
– Sergei Akbarov
Jul 17 at 12:51
However, the question about a reference is still relevant.
– Sergei Akbarov
Jul 17 at 12:54
add a comment |Â
up vote
1
down vote
favorite
up vote
1
down vote
favorite
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 existence of a Gentzen tree
$$
fracfracvdash Adotsvdash B
$$
implies the deducibility of the sequent $Avdash B$ (or, equivalently, the deducibility of the sequent $vdash Ato B$).
More generally, I wonder if there are textbooks on logic where the exposition is presented from the point of view of sequent calculus.
logic first-order-logic predicate-logic sequent-calculus
asked Jul 17 at 4:22
Sergei Akbarov
749413
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 existence of a Gentzen tree
$$
fracfracvdash Adotsvdash B
$$
implies the deducibility of the sequent $Avdash B$ (or, equivalently, the deducibility of the sequent $vdash Ato B$).
More generally, I wonder if there are textbooks on logic where the exposition is presented from the point of view of sequent calculus.
logic first-order-logic predicate-logic sequent-calculus
asked Jul 17 at 4:22
Sergei Akbarov
749413
edited Jul 17 at 10:46
asked Jul 17 at 4:22
Sergei Akbarov
749413
asked Jul 17 at 4:22
Sergei Akbarov
749413
asked Jul 17 at 4:22
Sergei Akbarov
749413
749413
Mauro, I mean the system LK as it is explained in Wikipedia. This is the same as in Takeuti's book, but he uses different symbols. I hope, my edit clarifies what I need. Do Negri and von Plato prove the deduction theorem in their book?
– Sergei Akbarov
Jul 17 at 9:15
Ok; in Wiki's entry dedicated to sequent calculus, it is used $vdash$ for sequents and $to$ for the conditional. Having said that, the rules are written "upside-down" to be used in tree-form (the proof start from the formula to be proved and decompose it). Having said that, you can see that the $text R to$ rule is like mine below (written upside-down).
– Mauro ALLEGRANZA
Jul 17 at 9:30
Excuse me I've just understood what is supposed to be done here: we should just add $A$ into each antecedent in this tree, and check that the obtained picture $$ fracfracAvdash AdotsAvdash B $$ can be completed to a deduction for the sequent $Avdash B$. For this we have to check that each rule in LK, after adding $A$, can be completed to a Gentzen tree. The condition that $A$ is closed is necessary for checking $forall R$ and $exists L$.
– Sergei Akbarov
Jul 17 at 12:51
However, the question about a reference is still relevant.
– Sergei Akbarov
Jul 17 at 12:54
add a comment |Â
Mauro, I mean the system LK as it is explained in Wikipedia. This is the same as in Takeuti's book, but he uses different symbols. I hope, my edit clarifies what I need. Do Negri and von Plato prove the deduction theorem in their book?
– Sergei Akbarov
Jul 17 at 9:15
Ok; in Wiki's entry dedicated to sequent calculus, it is used $vdash$ for sequents and $to$ for the conditional. Having said that, the rules are written "upside-down" to be used in tree-form (the proof start from the formula to be proved and decompose it). Having said that, you can see that the $text R to$ rule is like mine below (written upside-down).
– Mauro ALLEGRANZA
Jul 17 at 9:30
Excuse me I've just understood what is supposed to be done here: we should just add $A$ into each antecedent in this tree, and check that the obtained picture $$ fracfracAvdash AdotsAvdash B $$ can be completed to a deduction for the sequent $Avdash B$. For this we have to check that each rule in LK, after adding $A$, can be completed to a Gentzen tree. The condition that $A$ is closed is necessary for checking $forall R$ and $exists L$.
– Sergei Akbarov
Jul 17 at 12:51
However, the question about a reference is still relevant.
– Sergei Akbarov
Jul 17 at 12:54
Mauro, I mean the system LK as it is explained in Wikipedia. This is the same as in Takeuti's book, but he uses different symbols. I hope, my edit clarifies what I need. Do Negri and von Plato prove the deduction theorem in their book?
– Sergei Akbarov
Jul 17 at 9:15
Mauro, I mean the system LK as it is explained in Wikipedia. This is the same as in Takeuti's book, but he uses different symbols. I hope, my edit clarifies what I need. Do Negri and von Plato prove the deduction theorem in their book?
– Sergei Akbarov
Jul 17 at 9:15
Ok; in Wiki's entry dedicated to sequent calculus, it is used $vdash$ for sequents and $to$ for the conditional. Having said that, the rules are written "upside-down" to be used in tree-form (the proof start from the formula to be proved and decompose it). Having said that, you can see that the $text R to$ rule is like mine below (written upside-down).
– Mauro ALLEGRANZA
Jul 17 at 9:30
Ok; in Wiki's entry dedicated to sequent calculus, it is used $vdash$ for sequents and $to$ for the conditional. Having said that, the rules are written "upside-down" to be used in tree-form (the proof start from the formula to be proved and decompose it). Having said that, you can see that the $text R to$ rule is like mine below (written upside-down).
– Mauro ALLEGRANZA
Jul 17 at 9:30
Excuse me I've just understood what is supposed to be done here: we should just add $A$ into each antecedent in this tree, and check that the obtained picture $$ fracfracAvdash AdotsAvdash B $$ can be completed to a deduction for the sequent $Avdash B$. For this we have to check that each rule in LK, after adding $A$, can be completed to a Gentzen tree. The condition that $A$ is closed is necessary for checking $forall R$ and $exists L$.
– Sergei Akbarov
Jul 17 at 12:51
Excuse me I've just understood what is supposed to be done here: we should just add $A$ into each antecedent in this tree, and check that the obtained picture $$ fracfracAvdash AdotsAvdash B $$ can be completed to a deduction for the sequent $Avdash B$. For this we have to check that each rule in LK, after adding $A$, can be completed to a Gentzen tree. The condition that $A$ is closed is necessary for checking $forall R$ and $exists L$.
– Sergei Akbarov
Jul 17 at 12:51
However, the question about a reference is still relevant.
– Sergei Akbarov
Jul 17 at 12:54
However, the question about a reference is still relevant.
– Sergei Akbarov
Jul 17 at 12:54
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
2
down vote
In sequent calculus, the Deduction Theorem is simply the $(supset textRight)$ rule :
beginalign
fracC, Gamma to Delta, DGamma to Delta, C supset D (supset text R)
endalign
See : Gaisi Takeuti, Proof Theory, (2nd ed., 1987), page 10. In general, it is an excellent book dedicated to sequent calculus.
You can see also : Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001).
Note on symbolism : I've followed Takeuti in using $supset$ for the conditional conenctive ("if..., then...") and $to$ for the "auxiliary symbol" used in the sequents : $Gamma to Delta$.
Added (following Henning's comment).
We assume having a proof of $B$, i.e. a derivation in the calculus of the sequent : $to B$.
We apply $(text Weakening Left)$ to get : $A to B$ followed by $(supset textRight)$ to conclude with the sequent : $to (A supset B)$.
Regarding the quantifiers, the $(forall text Right)$ rule is [see page 10] :
beginalign
fracGamma to Delta, F(a)Gamma to Delta, forall x F(x) (forall text R)
endalign
with the restriction : $a$ does not occur in the lower sequent.
This means that we cannot use the derivation :
beginalign
fracF(a) to F(a)to F(a) supset forall x F(x) (forall text R)
endalign
to derive te invalid $F(a) supset forall x F(x)$.
answered Jul 17 at 6:12
Mauro ALLEGRANZA
60.7k346105
Mauro, I think this is a mistake: the meaning of the symbol $vdash$ is different in the deduction theorem and in the structural rules. If the meaning for $vdash$ is as in the structural rules, then the question is why for closed $A$ the existence of a Gentzen tree from $vdash A$ to $vdash B$ implies the deducibility of $vdash Ato B$.
– Sergei Akbarov
Jul 17 at 8:32
Mauro, I edited the question to clarify this.
– Sergei Akbarov
Jul 17 at 8:44
1
@SergeiAkbarov; In that setting the premise of the deduction theorem is that you have partial derivation of $GammatoDelta, D$ where $to C$ comes out of nowhere without a justification in some places. Take that derivation, and append a $C$ on the left-hand side of all sequents. This does not disturb the validity of the rules you're already using in the derivation, and makes the "without a justification" cases into bona fide instances of the identify axiom. You derivation now concludes $C,GammatoDelta,D$, and you can apply the $supset$R rule to get what you want.
– Henning Makholm
Jul 17 at 12:16
(Depending on the exact style of your sequent calculus you may need to inject some instances of left contraction or left weakening in your existing derivation tree in order to make all the $C$s meet up correctly -- but that's just bookkeeping).
– Henning Makholm
Jul 17 at 12:18
@HenningMakholm, yes, I have just understood the idea. I'll edit the question to remove what is clear now, thank you!
– Sergei Akbarov
Jul 17 at 12:41
 |Â
show 2 more comments
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
2
down vote
In sequent calculus, the Deduction Theorem is simply the $(supset textRight)$ rule :
beginalign
fracC, Gamma to Delta, DGamma to Delta, C supset D (supset text R)
endalign
See : Gaisi Takeuti, Proof Theory, (2nd ed., 1987), page 10. In general, it is an excellent book dedicated to sequent calculus.
You can see also : Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001).
Note on symbolism : I've followed Takeuti in using $supset$ for the conditional conenctive ("if..., then...") and $to$ for the "auxiliary symbol" used in the sequents : $Gamma to Delta$.
Added (following Henning's comment).
We assume having a proof of $B$, i.e. a derivation in the calculus of the sequent : $to B$.
We apply $(text Weakening Left)$ to get : $A to B$ followed by $(supset textRight)$ to conclude with the sequent : $to (A supset B)$.
Regarding the quantifiers, the $(forall text Right)$ rule is [see page 10] :
beginalign
fracGamma to Delta, F(a)Gamma to Delta, forall x F(x) (forall text R)
endalign
with the restriction : $a$ does not occur in the lower sequent.
This means that we cannot use the derivation :
beginalign
fracF(a) to F(a)to F(a) supset forall x F(x) (forall text R)
endalign
to derive te invalid $F(a) supset forall x F(x)$.
answered Jul 17 at 6:12
Mauro ALLEGRANZA
60.7k346105
Mauro, I think this is a mistake: the meaning of the symbol $vdash$ is different in the deduction theorem and in the structural rules. If the meaning for $vdash$ is as in the structural rules, then the question is why for closed $A$ the existence of a Gentzen tree from $vdash A$ to $vdash B$ implies the deducibility of $vdash Ato B$.
– Sergei Akbarov
Jul 17 at 8:32
Mauro, I edited the question to clarify this.
– Sergei Akbarov
Jul 17 at 8:44
1
@SergeiAkbarov; In that setting the premise of the deduction theorem is that you have partial derivation of $GammatoDelta, D$ where $to C$ comes out of nowhere without a justification in some places. Take that derivation, and append a $C$ on the left-hand side of all sequents. This does not disturb the validity of the rules you're already using in the derivation, and makes the "without a justification" cases into bona fide instances of the identify axiom. You derivation now concludes $C,GammatoDelta,D$, and you can apply the $supset$R rule to get what you want.
– Henning Makholm
Jul 17 at 12:16
(Depending on the exact style of your sequent calculus you may need to inject some instances of left contraction or left weakening in your existing derivation tree in order to make all the $C$s meet up correctly -- but that's just bookkeeping).
– Henning Makholm
Jul 17 at 12:18
@HenningMakholm, yes, I have just understood the idea. I'll edit the question to remove what is clear now, thank you!
– Sergei Akbarov
Jul 17 at 12:41
 |Â
show 2 more comments
up vote
2
down vote
In sequent calculus, the Deduction Theorem is simply the $(supset textRight)$ rule :
beginalign
fracC, Gamma to Delta, DGamma to Delta, C supset D (supset text R)
endalign
See : Gaisi Takeuti, Proof Theory, (2nd ed., 1987), page 10. In general, it is an excellent book dedicated to sequent calculus.
You can see also : Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001).
Note on symbolism : I've followed Takeuti in using $supset$ for the conditional conenctive ("if..., then...") and $to$ for the "auxiliary symbol" used in the sequents : $Gamma to Delta$.
Added (following Henning's comment).
We assume having a proof of $B$, i.e. a derivation in the calculus of the sequent : $to B$.
We apply $(text Weakening Left)$ to get : $A to B$ followed by $(supset textRight)$ to conclude with the sequent : $to (A supset B)$.
Regarding the quantifiers, the $(forall text Right)$ rule is [see page 10] :
beginalign
fracGamma to Delta, F(a)Gamma to Delta, forall x F(x) (forall text R)
endalign
with the restriction : $a$ does not occur in the lower sequent.
This means that we cannot use the derivation :
beginalign
fracF(a) to F(a)to F(a) supset forall x F(x) (forall text R)
endalign
to derive te invalid $F(a) supset forall x F(x)$.
answered Jul 17 at 6:12
Mauro ALLEGRANZA
60.7k346105
Mauro, I think this is a mistake: the meaning of the symbol $vdash$ is different in the deduction theorem and in the structural rules. If the meaning for $vdash$ is as in the structural rules, then the question is why for closed $A$ the existence of a Gentzen tree from $vdash A$ to $vdash B$ implies the deducibility of $vdash Ato B$.
– Sergei Akbarov
Jul 17 at 8:32
Mauro, I edited the question to clarify this.
– Sergei Akbarov
Jul 17 at 8:44
1
@SergeiAkbarov; In that setting the premise of the deduction theorem is that you have partial derivation of $GammatoDelta, D$ where $to C$ comes out of nowhere without a justification in some places. Take that derivation, and append a $C$ on the left-hand side of all sequents. This does not disturb the validity of the rules you're already using in the derivation, and makes the "without a justification" cases into bona fide instances of the identify axiom. You derivation now concludes $C,GammatoDelta,D$, and you can apply the $supset$R rule to get what you want.
– Henning Makholm
Jul 17 at 12:16
(Depending on the exact style of your sequent calculus you may need to inject some instances of left contraction or left weakening in your existing derivation tree in order to make all the $C$s meet up correctly -- but that's just bookkeeping).
– Henning Makholm
Jul 17 at 12:18
@HenningMakholm, yes, I have just understood the idea. I'll edit the question to remove what is clear now, thank you!
– Sergei Akbarov
Jul 17 at 12:41
 |Â
show 2 more comments
up vote
2
down vote
up vote
2
down vote
In sequent calculus, the Deduction Theorem is simply the $(supset textRight)$ rule :
beginalign
fracC, Gamma to Delta, DGamma to Delta, C supset D (supset text R)
endalign
See : Gaisi Takeuti, Proof Theory, (2nd ed., 1987), page 10. In general, it is an excellent book dedicated to sequent calculus.
You can see also : Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001).
Note on symbolism : I've followed Takeuti in using $supset$ for the conditional conenctive ("if..., then...") and $to$ for the "auxiliary symbol" used in the sequents : $Gamma to Delta$.
Added (following Henning's comment).
We assume having a proof of $B$, i.e. a derivation in the calculus of the sequent : $to B$.
We apply $(text Weakening Left)$ to get : $A to B$ followed by $(supset textRight)$ to conclude with the sequent : $to (A supset B)$.
Regarding the quantifiers, the $(forall text Right)$ rule is [see page 10] :
beginalign
fracGamma to Delta, F(a)Gamma to Delta, forall x F(x) (forall text R)
endalign
with the restriction : $a$ does not occur in the lower sequent.
This means that we cannot use the derivation :
beginalign
fracF(a) to F(a)to F(a) supset forall x F(x) (forall text R)
endalign
to derive te invalid $F(a) supset forall x F(x)$.
answered Jul 17 at 6:12
Mauro ALLEGRANZA
60.7k346105
In sequent calculus, the Deduction Theorem is simply the $(supset textRight)$ rule :
beginalign
fracC, Gamma to Delta, DGamma to Delta, C supset D (supset text R)
endalign
See : Gaisi Takeuti, Proof Theory, (2nd ed., 1987), page 10. In general, it is an excellent book dedicated to sequent calculus.
You can see also : Sara Negri & Jan von Plato, Structural Proof Theory, Cambridge UP (2001).
Note on symbolism : I've followed Takeuti in using $supset$ for the conditional conenctive ("if..., then...") and $to$ for the "auxiliary symbol" used in the sequents : $Gamma to Delta$.
Added (following Henning's comment).
We assume having a proof of $B$, i.e. a derivation in the calculus of the sequent : $to B$.
We apply $(text Weakening Left)$ to get : $A to B$ followed by $(supset textRight)$ to conclude with the sequent : $to (A supset B)$.
Regarding the quantifiers, the $(forall text Right)$ rule is [see page 10] :
beginalign
fracGamma to Delta, F(a)Gamma to Delta, forall x F(x) (forall text R)
endalign
with the restriction : $a$ does not occur in the lower sequent.
This means that we cannot use the derivation :
beginalign
fracF(a) to F(a)to F(a) supset forall x F(x) (forall text R)
endalign
to derive te invalid $F(a) supset forall x F(x)$.
answered Jul 17 at 6:12
Mauro ALLEGRANZA
60.7k346105
edited Jul 17 at 14:47
answered Jul 17 at 6:12
Mauro ALLEGRANZA
60.7k346105
answered Jul 17 at 6:12
Mauro ALLEGRANZA
60.7k346105
answered Jul 17 at 6:12
Mauro ALLEGRANZA
60.7k346105
60.7k346105
Mauro, I think this is a mistake: the meaning of the symbol $vdash$ is different in the deduction theorem and in the structural rules. If the meaning for $vdash$ is as in the structural rules, then the question is why for closed $A$ the existence of a Gentzen tree from $vdash A$ to $vdash B$ implies the deducibility of $vdash Ato B$.
– Sergei Akbarov
Jul 17 at 8:32
Mauro, I edited the question to clarify this.
– Sergei Akbarov
Jul 17 at 8:44
1
@SergeiAkbarov; In that setting the premise of the deduction theorem is that you have partial derivation of $GammatoDelta, D$ where $to C$ comes out of nowhere without a justification in some places. Take that derivation, and append a $C$ on the left-hand side of all sequents. This does not disturb the validity of the rules you're already using in the derivation, and makes the "without a justification" cases into bona fide instances of the identify axiom. You derivation now concludes $C,GammatoDelta,D$, and you can apply the $supset$R rule to get what you want.
– Henning Makholm
Jul 17 at 12:16
(Depending on the exact style of your sequent calculus you may need to inject some instances of left contraction or left weakening in your existing derivation tree in order to make all the $C$s meet up correctly -- but that's just bookkeeping).
– Henning Makholm
Jul 17 at 12:18
@HenningMakholm, yes, I have just understood the idea. I'll edit the question to remove what is clear now, thank you!
– Sergei Akbarov
Jul 17 at 12:41
 |Â
show 2 more comments
Mauro, I think this is a mistake: the meaning of the symbol $vdash$ is different in the deduction theorem and in the structural rules. If the meaning for $vdash$ is as in the structural rules, then the question is why for closed $A$ the existence of a Gentzen tree from $vdash A$ to $vdash B$ implies the deducibility of $vdash Ato B$.
– Sergei Akbarov
Jul 17 at 8:32
Mauro, I edited the question to clarify this.
– Sergei Akbarov
Jul 17 at 8:44
1
@SergeiAkbarov; In that setting the premise of the deduction theorem is that you have partial derivation of $GammatoDelta, D$ where $to C$ comes out of nowhere without a justification in some places. Take that derivation, and append a $C$ on the left-hand side of all sequents. This does not disturb the validity of the rules you're already using in the derivation, and makes the "without a justification" cases into bona fide instances of the identify axiom. You derivation now concludes $C,GammatoDelta,D$, and you can apply the $supset$R rule to get what you want.
– Henning Makholm
Jul 17 at 12:16
(Depending on the exact style of your sequent calculus you may need to inject some instances of left contraction or left weakening in your existing derivation tree in order to make all the $C$s meet up correctly -- but that's just bookkeeping).
– Henning Makholm
Jul 17 at 12:18
@HenningMakholm, yes, I have just understood the idea. I'll edit the question to remove what is clear now, thank you!
– Sergei Akbarov
Jul 17 at 12:41
Mauro, I think this is a mistake: the meaning of the symbol $vdash$ is different in the deduction theorem and in the structural rules. If the meaning for $vdash$ is as in the structural rules, then the question is why for closed $A$ the existence of a Gentzen tree from $vdash A$ to $vdash B$ implies the deducibility of $vdash Ato B$.
– Sergei Akbarov
Jul 17 at 8:32
Mauro, I think this is a mistake: the meaning of the symbol $vdash$ is different in the deduction theorem and in the structural rules. If the meaning for $vdash$ is as in the structural rules, then the question is why for closed $A$ the existence of a Gentzen tree from $vdash A$ to $vdash B$ implies the deducibility of $vdash Ato B$.
– Sergei Akbarov
Jul 17 at 8:32
Mauro, I edited the question to clarify this.
– Sergei Akbarov
Jul 17 at 8:44
Mauro, I edited the question to clarify this.
– Sergei Akbarov
Jul 17 at 8:44
1
1
@SergeiAkbarov; In that setting the premise of the deduction theorem is that you have partial derivation of $GammatoDelta, D$ where $to C$ comes out of nowhere without a justification in some places. Take that derivation, and append a $C$ on the left-hand side of all sequents. This does not disturb the validity of the rules you're already using in the derivation, and makes the "without a justification" cases into bona fide instances of the identify axiom. You derivation now concludes $C,GammatoDelta,D$, and you can apply the $supset$R rule to get what you want.
– Henning Makholm
Jul 17 at 12:16
@SergeiAkbarov; In that setting the premise of the deduction theorem is that you have partial derivation of $GammatoDelta, D$ where $to C$ comes out of nowhere without a justification in some places. Take that derivation, and append a $C$ on the left-hand side of all sequents. This does not disturb the validity of the rules you're already using in the derivation, and makes the "without a justification" cases into bona fide instances of the identify axiom. You derivation now concludes $C,GammatoDelta,D$, and you can apply the $supset$R rule to get what you want.
– Henning Makholm
Jul 17 at 12:16
(Depending on the exact style of your sequent calculus you may need to inject some instances of left contraction or left weakening in your existing derivation tree in order to make all the $C$s meet up correctly -- but that's just bookkeeping).
– Henning Makholm
Jul 17 at 12:18
(Depending on the exact style of your sequent calculus you may need to inject some instances of left contraction or left weakening in your existing derivation tree in order to make all the $C$s meet up correctly -- but that's just bookkeeping).
– Henning Makholm
Jul 17 at 12:18
@HenningMakholm, yes, I have just understood the idea. I'll edit the question to remove what is clear now, thank you!
– Sergei Akbarov
Jul 17 at 12:41
@HenningMakholm, yes, I have just understood the idea. I'll edit the question to remove what is clear now, thank you!
– Sergei Akbarov
Jul 17 at 12:41
 |Â
show 2 more comments
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2854128%2fproof-of-the-deduction-theorem-in-sequent-calculus%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Mauro, I mean the system LK as it is explained in Wikipedia. This is the same as in Takeuti's book, but he uses different symbols. I hope, my edit clarifies what I need. Do Negri and von Plato prove the deduction theorem in their book?
– Sergei Akbarov
Jul 17 at 9:15
Ok; in Wiki's entry dedicated to sequent calculus, it is used $vdash$ for sequents and $to$ for the conditional. Having said that, the rules are written "upside-down" to be used in tree-form (the proof start from the formula to be proved and decompose it). Having said that, you can see that the $text R to$ rule is like mine below (written upside-down).
– Mauro ALLEGRANZA
Jul 17 at 9:30
Excuse me I've just understood what is supposed to be done here: we should just add $A$ into each antecedent in this tree, and check that the obtained picture $$ fracfracAvdash AdotsAvdash B $$ can be completed to a deduction for the sequent $Avdash B$. For this we have to check that each rule in LK, after adding $A$, can be completed to a Gentzen tree. The condition that $A$ is closed is necessary for checking $forall R$ and $exists L$.
– Sergei Akbarov
Jul 17 at 12:51
However, the question about a reference is still relevant.
– Sergei Akbarov
Jul 17 at 12:54