Mixing
Prove the following theorem in propositional calculus
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
I have the following Hilbert-style propositional calculus, having the logical connectives $neg,rightarrow$ of arity one and two respectively, and the following axioms:
A1: $Arightarrow(Brightarrow A)$
A2: $(Arightarrow(Brightarrow C))rightarrow((Arightarrow B)rightarrow(Arightarrow C))$
A3: $(neg Arightarrow neg B)rightarrow (Brightarrow A).$
$A,B,C$ are any well-formed formulas (wffs). The only inference rule is modus ponens. I want to prove the following theorem:
$vdash (neg Arightarrow A)rightarrow A$ for any wff $A$.
You may use any or all of the following theorems without proof:
$vdash Arightarrow A$ for any wff $A$.
$Arightarrow B, Brightarrow Cvdash Arightarrow C$ for any wffs $A,B,C$.
$Arightarrow (Brightarrow C), Bvdash Arightarrow C$ for any wffs $A,B,C$.
$vdash neg Arightarrow (Arightarrow B)$ for any wffs $A,B$.
Please avoid using the deduction theorem unless absolutely necessary.
logic propositional-calculus
asked Aug 1 at 9:19
baronbrixius
361211
add a comment |Â
up vote
1
down vote
favorite
I have the following Hilbert-style propositional calculus, having the logical connectives $neg,rightarrow$ of arity one and two respectively, and the following axioms:
A1: $Arightarrow(Brightarrow A)$
A2: $(Arightarrow(Brightarrow C))rightarrow((Arightarrow B)rightarrow(Arightarrow C))$
A3: $(neg Arightarrow neg B)rightarrow (Brightarrow A).$
$A,B,C$ are any well-formed formulas (wffs). The only inference rule is modus ponens. I want to prove the following theorem:
$vdash (neg Arightarrow A)rightarrow A$ for any wff $A$.
You may use any or all of the following theorems without proof:
$vdash Arightarrow A$ for any wff $A$.
$Arightarrow B, Brightarrow Cvdash Arightarrow C$ for any wffs $A,B,C$.
$Arightarrow (Brightarrow C), Bvdash Arightarrow C$ for any wffs $A,B,C$.
$vdash neg Arightarrow (Arightarrow B)$ for any wffs $A,B$.
Please avoid using the deduction theorem unless absolutely necessary.
logic propositional-calculus
asked Aug 1 at 9:19
baronbrixius
361211
2
"Avoid using the deduction theorem" for a Hilbert-style calculus is a recipe for absolute misery. Why would you want that?
– Henning Makholm
Aug 1 at 10:03
@HenningMakholm Frege, Lukasiewicz, Russell, Hilbert, and others, as well plenty of theorem-provers avoid using the deduction theorem.
– Doug Spoonwood
Aug 1 at 10:46
add a comment |Â
up vote
1
down vote
favorite
up vote
1
down vote
favorite
I have the following Hilbert-style propositional calculus, having the logical connectives $neg,rightarrow$ of arity one and two respectively, and the following axioms:
A1: $Arightarrow(Brightarrow A)$
A2: $(Arightarrow(Brightarrow C))rightarrow((Arightarrow B)rightarrow(Arightarrow C))$
A3: $(neg Arightarrow neg B)rightarrow (Brightarrow A).$
$A,B,C$ are any well-formed formulas (wffs). The only inference rule is modus ponens. I want to prove the following theorem:
$vdash (neg Arightarrow A)rightarrow A$ for any wff $A$.
You may use any or all of the following theorems without proof:
$vdash Arightarrow A$ for any wff $A$.
$Arightarrow B, Brightarrow Cvdash Arightarrow C$ for any wffs $A,B,C$.
$Arightarrow (Brightarrow C), Bvdash Arightarrow C$ for any wffs $A,B,C$.
$vdash neg Arightarrow (Arightarrow B)$ for any wffs $A,B$.
Please avoid using the deduction theorem unless absolutely necessary.
logic propositional-calculus
asked Aug 1 at 9:19
baronbrixius
361211
I have the following Hilbert-style propositional calculus, having the logical connectives $neg,rightarrow$ of arity one and two respectively, and the following axioms:
A1: $Arightarrow(Brightarrow A)$
A2: $(Arightarrow(Brightarrow C))rightarrow((Arightarrow B)rightarrow(Arightarrow C))$
A3: $(neg Arightarrow neg B)rightarrow (Brightarrow A).$
$A,B,C$ are any well-formed formulas (wffs). The only inference rule is modus ponens. I want to prove the following theorem:
$vdash (neg Arightarrow A)rightarrow A$ for any wff $A$.
You may use any or all of the following theorems without proof:
$vdash Arightarrow A$ for any wff $A$.
$Arightarrow B, Brightarrow Cvdash Arightarrow C$ for any wffs $A,B,C$.
$Arightarrow (Brightarrow C), Bvdash Arightarrow C$ for any wffs $A,B,C$.
$vdash neg Arightarrow (Arightarrow B)$ for any wffs $A,B$.
Please avoid using the deduction theorem unless absolutely necessary.
logic propositional-calculus
asked Aug 1 at 9:19
baronbrixius
361211
asked Aug 1 at 9:19
baronbrixius
361211
asked Aug 1 at 9:19
baronbrixius
361211
asked Aug 1 at 9:19
baronbrixius
361211
361211
2
"Avoid using the deduction theorem" for a Hilbert-style calculus is a recipe for absolute misery. Why would you want that?
– Henning Makholm
Aug 1 at 10:03
@HenningMakholm Frege, Lukasiewicz, Russell, Hilbert, and others, as well plenty of theorem-provers avoid using the deduction theorem.
– Doug Spoonwood
Aug 1 at 10:46
add a comment |Â
2
"Avoid using the deduction theorem" for a Hilbert-style calculus is a recipe for absolute misery. Why would you want that?
– Henning Makholm
Aug 1 at 10:03
@HenningMakholm Frege, Lukasiewicz, Russell, Hilbert, and others, as well plenty of theorem-provers avoid using the deduction theorem.
– Doug Spoonwood
Aug 1 at 10:46
2
2
"Avoid using the deduction theorem" for a Hilbert-style calculus is a recipe for absolute misery. Why would you want that?
– Henning Makholm
Aug 1 at 10:03
"Avoid using the deduction theorem" for a Hilbert-style calculus is a recipe for absolute misery. Why would you want that?
– Henning Makholm
Aug 1 at 10:03
@HenningMakholm Frege, Lukasiewicz, Russell, Hilbert, and others, as well plenty of theorem-provers avoid using the deduction theorem.
– Doug Spoonwood
Aug 1 at 10:46
@HenningMakholm Frege, Lukasiewicz, Russell, Hilbert, and others, as well plenty of theorem-provers avoid using the deduction theorem.
– Doug Spoonwood
Aug 1 at 10:46
add a comment |Â
2 Answers
2
active
oldest
votes
up vote
1
down vote
Lemma
1) $vdash lnot A to (A to B)$ --- Th.4
2) $vdash (lnot A to (A to B)) to ((lnot A to A) to (lnot A to lnot B))$ --- Ax.2
3) $vdash (lnot A to A) to (lnot A to lnot B)$ --- from 1) and 2)
4) $vdash (lnot A to lnot B) to (B to A)$ --- Ax.3
5) $vdash (lnot A to A) to (B to A)$ --- from 3) and 4) by Th.2
Proof
1) $vdash (lnot A to A) to ((lnot A to A) to A)$ --- from Lemma
2) $vdash ((lnot A to A) to ((lnot A to A) to A)) to (((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A))$ --- Ax.2
3) $vdash ((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A)$ --- from 1) and 2)
4) $vdash (lnot A to A) to (lnot A to A)$ --- from Th.1
5) $vdash (lnot A to A) to A$ --- from 3) and 4)
answered Aug 1 at 9:59
Mauro ALLEGRANZA
60.6k346105
add a comment |Â
up vote
-1
down vote
I use Polish notation. Thus, instead I'll translate every wff of the form $lnot$$alpha$ into the form N$alpha$. Also, I'll translate every wff of the form ($alpha$$rightarrow$$beta$) into the form C$alpha$$beta$. Thus, the axioms can get translated to
A1 CxCyx
A2 CCxCyzCCxyCxz
A3 CCNxNyCxy
I'll also use spacing to help to indicate where a substitution of an axiom or previously proved theorem took place.
1 CxCyx
2 CCxCyzCCxyCxz
3 CCNxNyCyx
4 C CxCyx C z CxCyx from 1
5 CzCxCyx from 4, 1
6 CC CxCyz C Cxy Cxz CC CxCyz Cxy C CxCyz Cxz from 2
7 CCCxCyzCxyCCxCyzCxz from 6, 2
8 C CCNxNyCyx C z CCNxNyCyx from 1
9 CzCCNxNyCyx from 8, 3
10 C CxCCyxz C x C y x from 5
11 CCC x C Cyx z C x Cyx CC x C Cyx z C x z from 7
12 CCxCCyxzCxz from 11, 10
13 CC z C CNxNy Cyx CC z CNxNy C z Cyx from 2
14 CCzCNxNyCzCyx from 13, 9
15 CC Nz CC Ny Nz Czy C Nz Czy from 12
16 C Nz CC Ny Nz C z y from 9
17 CNzCzy from 15, 16
18 CC Nz C z y CC Nz z C Nz y from 2
19 CCNzzCNzy from 18, 17
20 CC CNzz CN z N y C CNzz C y z from 14
21 CCN z z CN z Ny from 19
22 CCNzzCyz from 20, 21
23 CC CNxx CC y CNxx x C CNxx x from 12
24 CCN x x C CyCNxx x from 22
25 CCNxxx from 23, 24
answered Aug 2 at 9:44
Doug Spoonwood
7,57012042
add a comment |Â
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
Lemma
1) $vdash lnot A to (A to B)$ --- Th.4
2) $vdash (lnot A to (A to B)) to ((lnot A to A) to (lnot A to lnot B))$ --- Ax.2
3) $vdash (lnot A to A) to (lnot A to lnot B)$ --- from 1) and 2)
4) $vdash (lnot A to lnot B) to (B to A)$ --- Ax.3
5) $vdash (lnot A to A) to (B to A)$ --- from 3) and 4) by Th.2
Proof
1) $vdash (lnot A to A) to ((lnot A to A) to A)$ --- from Lemma
2) $vdash ((lnot A to A) to ((lnot A to A) to A)) to (((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A))$ --- Ax.2
3) $vdash ((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A)$ --- from 1) and 2)
4) $vdash (lnot A to A) to (lnot A to A)$ --- from Th.1
5) $vdash (lnot A to A) to A$ --- from 3) and 4)
answered Aug 1 at 9:59
Mauro ALLEGRANZA
60.6k346105
add a comment |Â
up vote
1
down vote
Lemma
1) $vdash lnot A to (A to B)$ --- Th.4
2) $vdash (lnot A to (A to B)) to ((lnot A to A) to (lnot A to lnot B))$ --- Ax.2
3) $vdash (lnot A to A) to (lnot A to lnot B)$ --- from 1) and 2)
4) $vdash (lnot A to lnot B) to (B to A)$ --- Ax.3
5) $vdash (lnot A to A) to (B to A)$ --- from 3) and 4) by Th.2
Proof
1) $vdash (lnot A to A) to ((lnot A to A) to A)$ --- from Lemma
2) $vdash ((lnot A to A) to ((lnot A to A) to A)) to (((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A))$ --- Ax.2
3) $vdash ((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A)$ --- from 1) and 2)
4) $vdash (lnot A to A) to (lnot A to A)$ --- from Th.1
5) $vdash (lnot A to A) to A$ --- from 3) and 4)
answered Aug 1 at 9:59
Mauro ALLEGRANZA
60.6k346105
add a comment |Â
up vote
1
down vote
up vote
1
down vote
Lemma
1) $vdash lnot A to (A to B)$ --- Th.4
2) $vdash (lnot A to (A to B)) to ((lnot A to A) to (lnot A to lnot B))$ --- Ax.2
3) $vdash (lnot A to A) to (lnot A to lnot B)$ --- from 1) and 2)
4) $vdash (lnot A to lnot B) to (B to A)$ --- Ax.3
5) $vdash (lnot A to A) to (B to A)$ --- from 3) and 4) by Th.2
Proof
1) $vdash (lnot A to A) to ((lnot A to A) to A)$ --- from Lemma
2) $vdash ((lnot A to A) to ((lnot A to A) to A)) to (((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A))$ --- Ax.2
3) $vdash ((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A)$ --- from 1) and 2)
4) $vdash (lnot A to A) to (lnot A to A)$ --- from Th.1
5) $vdash (lnot A to A) to A$ --- from 3) and 4)
answered Aug 1 at 9:59
Mauro ALLEGRANZA
60.6k346105
Lemma
1) $vdash lnot A to (A to B)$ --- Th.4
2) $vdash (lnot A to (A to B)) to ((lnot A to A) to (lnot A to lnot B))$ --- Ax.2
3) $vdash (lnot A to A) to (lnot A to lnot B)$ --- from 1) and 2)
4) $vdash (lnot A to lnot B) to (B to A)$ --- Ax.3
5) $vdash (lnot A to A) to (B to A)$ --- from 3) and 4) by Th.2
Proof
1) $vdash (lnot A to A) to ((lnot A to A) to A)$ --- from Lemma
2) $vdash ((lnot A to A) to ((lnot A to A) to A)) to (((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A))$ --- Ax.2
3) $vdash ((lnot A to A) to (lnot A to A)) to ((lnot A to A) to A)$ --- from 1) and 2)
4) $vdash (lnot A to A) to (lnot A to A)$ --- from Th.1
5) $vdash (lnot A to A) to A$ --- from 3) and 4)
answered Aug 1 at 9:59
Mauro ALLEGRANZA
60.6k346105
answered Aug 1 at 9:59
Mauro ALLEGRANZA
60.6k346105
answered Aug 1 at 9:59
Mauro ALLEGRANZA
60.6k346105
answered Aug 1 at 9:59
Mauro ALLEGRANZA
60.6k346105
60.6k346105
add a comment |Â
add a comment |Â
up vote
-1
down vote
I use Polish notation. Thus, instead I'll translate every wff of the form $lnot$$alpha$ into the form N$alpha$. Also, I'll translate every wff of the form ($alpha$$rightarrow$$beta$) into the form C$alpha$$beta$. Thus, the axioms can get translated to
A1 CxCyx
A2 CCxCyzCCxyCxz
A3 CCNxNyCxy
I'll also use spacing to help to indicate where a substitution of an axiom or previously proved theorem took place.
1 CxCyx
2 CCxCyzCCxyCxz
3 CCNxNyCyx
4 C CxCyx C z CxCyx from 1
5 CzCxCyx from 4, 1
6 CC CxCyz C Cxy Cxz CC CxCyz Cxy C CxCyz Cxz from 2
7 CCCxCyzCxyCCxCyzCxz from 6, 2
8 C CCNxNyCyx C z CCNxNyCyx from 1
9 CzCCNxNyCyx from 8, 3
10 C CxCCyxz C x C y x from 5
11 CCC x C Cyx z C x Cyx CC x C Cyx z C x z from 7
12 CCxCCyxzCxz from 11, 10
13 CC z C CNxNy Cyx CC z CNxNy C z Cyx from 2
14 CCzCNxNyCzCyx from 13, 9
15 CC Nz CC Ny Nz Czy C Nz Czy from 12
16 C Nz CC Ny Nz C z y from 9
17 CNzCzy from 15, 16
18 CC Nz C z y CC Nz z C Nz y from 2
19 CCNzzCNzy from 18, 17
20 CC CNzz CN z N y C CNzz C y z from 14
21 CCN z z CN z Ny from 19
22 CCNzzCyz from 20, 21
23 CC CNxx CC y CNxx x C CNxx x from 12
24 CCN x x C CyCNxx x from 22
25 CCNxxx from 23, 24
answered Aug 2 at 9:44
Doug Spoonwood
7,57012042
add a comment |Â
up vote
-1
down vote
I use Polish notation. Thus, instead I'll translate every wff of the form $lnot$$alpha$ into the form N$alpha$. Also, I'll translate every wff of the form ($alpha$$rightarrow$$beta$) into the form C$alpha$$beta$. Thus, the axioms can get translated to
A1 CxCyx
A2 CCxCyzCCxyCxz
A3 CCNxNyCxy
I'll also use spacing to help to indicate where a substitution of an axiom or previously proved theorem took place.
1 CxCyx
2 CCxCyzCCxyCxz
3 CCNxNyCyx
4 C CxCyx C z CxCyx from 1
5 CzCxCyx from 4, 1
6 CC CxCyz C Cxy Cxz CC CxCyz Cxy C CxCyz Cxz from 2
7 CCCxCyzCxyCCxCyzCxz from 6, 2
8 C CCNxNyCyx C z CCNxNyCyx from 1
9 CzCCNxNyCyx from 8, 3
10 C CxCCyxz C x C y x from 5
11 CCC x C Cyx z C x Cyx CC x C Cyx z C x z from 7
12 CCxCCyxzCxz from 11, 10
13 CC z C CNxNy Cyx CC z CNxNy C z Cyx from 2
14 CCzCNxNyCzCyx from 13, 9
15 CC Nz CC Ny Nz Czy C Nz Czy from 12
16 C Nz CC Ny Nz C z y from 9
17 CNzCzy from 15, 16
18 CC Nz C z y CC Nz z C Nz y from 2
19 CCNzzCNzy from 18, 17
20 CC CNzz CN z N y C CNzz C y z from 14
21 CCN z z CN z Ny from 19
22 CCNzzCyz from 20, 21
23 CC CNxx CC y CNxx x C CNxx x from 12
24 CCN x x C CyCNxx x from 22
25 CCNxxx from 23, 24
answered Aug 2 at 9:44
Doug Spoonwood
7,57012042
add a comment |Â
up vote
-1
down vote
up vote
-1
down vote
I use Polish notation. Thus, instead I'll translate every wff of the form $lnot$$alpha$ into the form N$alpha$. Also, I'll translate every wff of the form ($alpha$$rightarrow$$beta$) into the form C$alpha$$beta$. Thus, the axioms can get translated to
A1 CxCyx
A2 CCxCyzCCxyCxz
A3 CCNxNyCxy
I'll also use spacing to help to indicate where a substitution of an axiom or previously proved theorem took place.
1 CxCyx
2 CCxCyzCCxyCxz
3 CCNxNyCyx
4 C CxCyx C z CxCyx from 1
5 CzCxCyx from 4, 1
6 CC CxCyz C Cxy Cxz CC CxCyz Cxy C CxCyz Cxz from 2
7 CCCxCyzCxyCCxCyzCxz from 6, 2
8 C CCNxNyCyx C z CCNxNyCyx from 1
9 CzCCNxNyCyx from 8, 3
10 C CxCCyxz C x C y x from 5
11 CCC x C Cyx z C x Cyx CC x C Cyx z C x z from 7
12 CCxCCyxzCxz from 11, 10
13 CC z C CNxNy Cyx CC z CNxNy C z Cyx from 2
14 CCzCNxNyCzCyx from 13, 9
15 CC Nz CC Ny Nz Czy C Nz Czy from 12
16 C Nz CC Ny Nz C z y from 9
17 CNzCzy from 15, 16
18 CC Nz C z y CC Nz z C Nz y from 2
19 CCNzzCNzy from 18, 17
20 CC CNzz CN z N y C CNzz C y z from 14
21 CCN z z CN z Ny from 19
22 CCNzzCyz from 20, 21
23 CC CNxx CC y CNxx x C CNxx x from 12
24 CCN x x C CyCNxx x from 22
25 CCNxxx from 23, 24
answered Aug 2 at 9:44
Doug Spoonwood
7,57012042
I use Polish notation. Thus, instead I'll translate every wff of the form $lnot$$alpha$ into the form N$alpha$. Also, I'll translate every wff of the form ($alpha$$rightarrow$$beta$) into the form C$alpha$$beta$. Thus, the axioms can get translated to
A1 CxCyx
A2 CCxCyzCCxyCxz
A3 CCNxNyCxy
I'll also use spacing to help to indicate where a substitution of an axiom or previously proved theorem took place.
1 CxCyx
2 CCxCyzCCxyCxz
3 CCNxNyCyx
4 C CxCyx C z CxCyx from 1
5 CzCxCyx from 4, 1
6 CC CxCyz C Cxy Cxz CC CxCyz Cxy C CxCyz Cxz from 2
7 CCCxCyzCxyCCxCyzCxz from 6, 2
8 C CCNxNyCyx C z CCNxNyCyx from 1
9 CzCCNxNyCyx from 8, 3
10 C CxCCyxz C x C y x from 5
11 CCC x C Cyx z C x Cyx CC x C Cyx z C x z from 7
12 CCxCCyxzCxz from 11, 10
13 CC z C CNxNy Cyx CC z CNxNy C z Cyx from 2
14 CCzCNxNyCzCyx from 13, 9
15 CC Nz CC Ny Nz Czy C Nz Czy from 12
16 C Nz CC Ny Nz C z y from 9
17 CNzCzy from 15, 16
18 CC Nz C z y CC Nz z C Nz y from 2
19 CCNzzCNzy from 18, 17
20 CC CNzz CN z N y C CNzz C y z from 14
21 CCN z z CN z Ny from 19
22 CCNzzCyz from 20, 21
23 CC CNxx CC y CNxx x C CNxx x from 12
24 CCN x x C CyCNxx x from 22
25 CCNxxx from 23, 24
answered Aug 2 at 9:44
Doug Spoonwood
7,57012042
answered Aug 2 at 9:44
Doug Spoonwood
7,57012042
answered Aug 2 at 9:44
Doug Spoonwood
7,57012042
answered Aug 2 at 9:44
Doug Spoonwood
7,57012042
7,57012042
add a comment |Â
add a comment |Â
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%2f2868878%2fprove-the-following-theorem-in-propositional-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
2
"Avoid using the deduction theorem" for a Hilbert-style calculus is a recipe for absolute misery. Why would you want that?
– Henning Makholm
Aug 1 at 10:03
@HenningMakholm Frege, Lukasiewicz, Russell, Hilbert, and others, as well plenty of theorem-provers avoid using the deduction theorem.
– Doug Spoonwood
Aug 1 at 10:46