Equivalence in Natural deduction in First-order logic 2
Clash Royale CLAN TAG#URR8PPP
up vote
2
down vote
favorite
I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task.
Task
Solve the following with natural deduction.
$vdash exists xneg P(x) iff neg forall xP(x)$
Answer
As earlier posted similar tasks for this to be correct I have to prove $A vdash B$ and $B vdash A$, where $A = exists x , lnot P(x)$ and $B = lnot forall x , P(x)$.
$A vdash B$: https://imgur.com/a/R8wt2YR
$B vdash A$: https://imgur.com/a/g7Rz4x9
Thank you!
logic first-order-logic proof-theory natural-deduction formal-proofs
edited Aug 21 at 9:06
Taroccoesbrocco
3,72651433
asked Aug 21 at 8:25
Fredrik Andersson
515
add a comment |Â
up vote
2
down vote
favorite
I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task.
Task
Solve the following with natural deduction.
$vdash exists xneg P(x) iff neg forall xP(x)$
Answer
As earlier posted similar tasks for this to be correct I have to prove $A vdash B$ and $B vdash A$, where $A = exists x , lnot P(x)$ and $B = lnot forall x , P(x)$.
$A vdash B$: https://imgur.com/a/R8wt2YR
$B vdash A$: https://imgur.com/a/g7Rz4x9
Thank you!
logic first-order-logic proof-theory natural-deduction formal-proofs
edited Aug 21 at 9:06
Taroccoesbrocco
3,72651433
asked Aug 21 at 8:25
Fredrik Andersson
515
add a comment |Â
up vote
2
down vote
favorite
up vote
2
down vote
favorite
I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task.
Task
Solve the following with natural deduction.
$vdash exists xneg P(x) iff neg forall xP(x)$
Answer
As earlier posted similar tasks for this to be correct I have to prove $A vdash B$ and $B vdash A$, where $A = exists x , lnot P(x)$ and $B = lnot forall x , P(x)$.
$A vdash B$: https://imgur.com/a/R8wt2YR
$B vdash A$: https://imgur.com/a/g7Rz4x9
Thank you!
logic first-order-logic proof-theory natural-deduction formal-proofs
edited Aug 21 at 9:06
Taroccoesbrocco
3,72651433
asked Aug 21 at 8:25
Fredrik Andersson
515
I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task.
Task
Solve the following with natural deduction.
$vdash exists xneg P(x) iff neg forall xP(x)$
Answer
As earlier posted similar tasks for this to be correct I have to prove $A vdash B$ and $B vdash A$, where $A = exists x , lnot P(x)$ and $B = lnot forall x , P(x)$.
$A vdash B$: https://imgur.com/a/R8wt2YR
$B vdash A$: https://imgur.com/a/g7Rz4x9
Thank you!
logic first-order-logic proof-theory natural-deduction formal-proofs
edited Aug 21 at 9:06
Taroccoesbrocco
3,72651433
asked Aug 21 at 8:25
Fredrik Andersson
515
edited Aug 21 at 9:06
Taroccoesbrocco
3,72651433
edited Aug 21 at 9:06
Taroccoesbrocco
3,72651433
edited Aug 21 at 9:06
Taroccoesbrocco
3,72651433
3,72651433
asked Aug 21 at 8:25
Fredrik Andersson
515
asked Aug 21 at 8:25
Fredrik Andersson
515
asked Aug 21 at 8:25
Fredrik Andersson
515
515
add a comment |Â
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
1
down vote
accepted
Your proof of $exists x , lnot P(x) vdash lnot forall x , P(x)$ is perfect. However, your attempt for proving $lnot forall x , P(x) vdash exists x , lnot P(x)$ is wrong, the rule $forall_i$ on the top is not correctly instantiated because it does not respect the proviso about free variables: indeed, when you apply the rule $forall_i$, $u$ is a free variable of an undischarged hypothesis, which is not allowed as explained here. (Note that this proviso is crucial to get only correct derivations, otherwise you could prove $exists x , P(x) vdash forall x , P(x)$, which is not correct).
A correct derivation of $lnot forall x , P(x) vdash exists x , lnot P(x)$ in natural deduction is the following:
$$
dfracdfraclnot forall x , P(x) qquad dfracdfracdfrac[lnot exists x , lnot P(x)]^* qquad dfrac[lnot P(x)]^**exists x , lnot P(x)exists_ibotlnot_eP(x)RAA^**forall x , P(x)forall_ibotlnot_e
exists x , lnot P(x)RAA^*
$$
Note that in this derivation the rule $forall_i$ is correctly instantiated, since $x$ is not free in the (undischarged) hypothesis.
There is also a derivation using only one instance of the rule RAA, but it is longer and awkward, not really interesting.
answered Aug 21 at 8:54
Taroccoesbrocco
3,72651433
How come you can do $P(x)$ to $forall xP(x)$ with the same x? I thought the rule was that you had to use a free variable for $forall$ introduction?
– Fredrik Andersson
Aug 23 at 10:38
@FredrikAndersson - The rule $forall_i$ claims that if $varphi(x)$ is derivable then $forall x , varphi(x)$ is derivable, on the proviso that the variable $x$ does not occur free in any undischarged hypothesis (see for instance here, p. 32; or Van Dalen, Logic and Structure, 5th ed., 2012, p. 86). The idea is that if you can prove $varphi(x)$ without any specific assumption on $x$, then $varphi(x)$ holds for every $x$.
– Taroccoesbrocco
Aug 23 at 13:36
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
Your proof of $exists x , lnot P(x) vdash lnot forall x , P(x)$ is perfect. However, your attempt for proving $lnot forall x , P(x) vdash exists x , lnot P(x)$ is wrong, the rule $forall_i$ on the top is not correctly instantiated because it does not respect the proviso about free variables: indeed, when you apply the rule $forall_i$, $u$ is a free variable of an undischarged hypothesis, which is not allowed as explained here. (Note that this proviso is crucial to get only correct derivations, otherwise you could prove $exists x , P(x) vdash forall x , P(x)$, which is not correct).
A correct derivation of $lnot forall x , P(x) vdash exists x , lnot P(x)$ in natural deduction is the following:
$$
dfracdfraclnot forall x , P(x) qquad dfracdfracdfrac[lnot exists x , lnot P(x)]^* qquad dfrac[lnot P(x)]^**exists x , lnot P(x)exists_ibotlnot_eP(x)RAA^**forall x , P(x)forall_ibotlnot_e
exists x , lnot P(x)RAA^*
$$
Note that in this derivation the rule $forall_i$ is correctly instantiated, since $x$ is not free in the (undischarged) hypothesis.
There is also a derivation using only one instance of the rule RAA, but it is longer and awkward, not really interesting.
answered Aug 21 at 8:54
Taroccoesbrocco
3,72651433
How come you can do $P(x)$ to $forall xP(x)$ with the same x? I thought the rule was that you had to use a free variable for $forall$ introduction?
– Fredrik Andersson
Aug 23 at 10:38
@FredrikAndersson - The rule $forall_i$ claims that if $varphi(x)$ is derivable then $forall x , varphi(x)$ is derivable, on the proviso that the variable $x$ does not occur free in any undischarged hypothesis (see for instance here, p. 32; or Van Dalen, Logic and Structure, 5th ed., 2012, p. 86). The idea is that if you can prove $varphi(x)$ without any specific assumption on $x$, then $varphi(x)$ holds for every $x$.
– Taroccoesbrocco
Aug 23 at 13:36
add a comment |Â
up vote
1
down vote
accepted
Your proof of $exists x , lnot P(x) vdash lnot forall x , P(x)$ is perfect. However, your attempt for proving $lnot forall x , P(x) vdash exists x , lnot P(x)$ is wrong, the rule $forall_i$ on the top is not correctly instantiated because it does not respect the proviso about free variables: indeed, when you apply the rule $forall_i$, $u$ is a free variable of an undischarged hypothesis, which is not allowed as explained here. (Note that this proviso is crucial to get only correct derivations, otherwise you could prove $exists x , P(x) vdash forall x , P(x)$, which is not correct).
A correct derivation of $lnot forall x , P(x) vdash exists x , lnot P(x)$ in natural deduction is the following:
$$
dfracdfraclnot forall x , P(x) qquad dfracdfracdfrac[lnot exists x , lnot P(x)]^* qquad dfrac[lnot P(x)]^**exists x , lnot P(x)exists_ibotlnot_eP(x)RAA^**forall x , P(x)forall_ibotlnot_e
exists x , lnot P(x)RAA^*
$$
Note that in this derivation the rule $forall_i$ is correctly instantiated, since $x$ is not free in the (undischarged) hypothesis.
There is also a derivation using only one instance of the rule RAA, but it is longer and awkward, not really interesting.
answered Aug 21 at 8:54
Taroccoesbrocco
3,72651433
How come you can do $P(x)$ to $forall xP(x)$ with the same x? I thought the rule was that you had to use a free variable for $forall$ introduction?
– Fredrik Andersson
Aug 23 at 10:38
@FredrikAndersson - The rule $forall_i$ claims that if $varphi(x)$ is derivable then $forall x , varphi(x)$ is derivable, on the proviso that the variable $x$ does not occur free in any undischarged hypothesis (see for instance here, p. 32; or Van Dalen, Logic and Structure, 5th ed., 2012, p. 86). The idea is that if you can prove $varphi(x)$ without any specific assumption on $x$, then $varphi(x)$ holds for every $x$.
– Taroccoesbrocco
Aug 23 at 13:36
add a comment |Â
up vote
1
down vote
accepted
up vote
1
down vote
accepted
Your proof of $exists x , lnot P(x) vdash lnot forall x , P(x)$ is perfect. However, your attempt for proving $lnot forall x , P(x) vdash exists x , lnot P(x)$ is wrong, the rule $forall_i$ on the top is not correctly instantiated because it does not respect the proviso about free variables: indeed, when you apply the rule $forall_i$, $u$ is a free variable of an undischarged hypothesis, which is not allowed as explained here. (Note that this proviso is crucial to get only correct derivations, otherwise you could prove $exists x , P(x) vdash forall x , P(x)$, which is not correct).
A correct derivation of $lnot forall x , P(x) vdash exists x , lnot P(x)$ in natural deduction is the following:
$$
dfracdfraclnot forall x , P(x) qquad dfracdfracdfrac[lnot exists x , lnot P(x)]^* qquad dfrac[lnot P(x)]^**exists x , lnot P(x)exists_ibotlnot_eP(x)RAA^**forall x , P(x)forall_ibotlnot_e
exists x , lnot P(x)RAA^*
$$
Note that in this derivation the rule $forall_i$ is correctly instantiated, since $x$ is not free in the (undischarged) hypothesis.
There is also a derivation using only one instance of the rule RAA, but it is longer and awkward, not really interesting.
answered Aug 21 at 8:54
Taroccoesbrocco
3,72651433
Your proof of $exists x , lnot P(x) vdash lnot forall x , P(x)$ is perfect. However, your attempt for proving $lnot forall x , P(x) vdash exists x , lnot P(x)$ is wrong, the rule $forall_i$ on the top is not correctly instantiated because it does not respect the proviso about free variables: indeed, when you apply the rule $forall_i$, $u$ is a free variable of an undischarged hypothesis, which is not allowed as explained here. (Note that this proviso is crucial to get only correct derivations, otherwise you could prove $exists x , P(x) vdash forall x , P(x)$, which is not correct).
A correct derivation of $lnot forall x , P(x) vdash exists x , lnot P(x)$ in natural deduction is the following:
$$
dfracdfraclnot forall x , P(x) qquad dfracdfracdfrac[lnot exists x , lnot P(x)]^* qquad dfrac[lnot P(x)]^**exists x , lnot P(x)exists_ibotlnot_eP(x)RAA^**forall x , P(x)forall_ibotlnot_e
exists x , lnot P(x)RAA^*
$$
Note that in this derivation the rule $forall_i$ is correctly instantiated, since $x$ is not free in the (undischarged) hypothesis.
There is also a derivation using only one instance of the rule RAA, but it is longer and awkward, not really interesting.
answered Aug 21 at 8:54
Taroccoesbrocco
3,72651433
edited Aug 21 at 9:01
answered Aug 21 at 8:54
Taroccoesbrocco
3,72651433
answered Aug 21 at 8:54
Taroccoesbrocco
3,72651433
answered Aug 21 at 8:54
Taroccoesbrocco
3,72651433
3,72651433
How come you can do $P(x)$ to $forall xP(x)$ with the same x? I thought the rule was that you had to use a free variable for $forall$ introduction?
– Fredrik Andersson
Aug 23 at 10:38
@FredrikAndersson - The rule $forall_i$ claims that if $varphi(x)$ is derivable then $forall x , varphi(x)$ is derivable, on the proviso that the variable $x$ does not occur free in any undischarged hypothesis (see for instance here, p. 32; or Van Dalen, Logic and Structure, 5th ed., 2012, p. 86). The idea is that if you can prove $varphi(x)$ without any specific assumption on $x$, then $varphi(x)$ holds for every $x$.
– Taroccoesbrocco
Aug 23 at 13:36
add a comment |Â
How come you can do $P(x)$ to $forall xP(x)$ with the same x? I thought the rule was that you had to use a free variable for $forall$ introduction?
– Fredrik Andersson
Aug 23 at 10:38
@FredrikAndersson - The rule $forall_i$ claims that if $varphi(x)$ is derivable then $forall x , varphi(x)$ is derivable, on the proviso that the variable $x$ does not occur free in any undischarged hypothesis (see for instance here, p. 32; or Van Dalen, Logic and Structure, 5th ed., 2012, p. 86). The idea is that if you can prove $varphi(x)$ without any specific assumption on $x$, then $varphi(x)$ holds for every $x$.
– Taroccoesbrocco
Aug 23 at 13:36
How come you can do $P(x)$ to $forall xP(x)$ with the same x? I thought the rule was that you had to use a free variable for $forall$ introduction?
– Fredrik Andersson
Aug 23 at 10:38
How come you can do $P(x)$ to $forall xP(x)$ with the same x? I thought the rule was that you had to use a free variable for $forall$ introduction?
– Fredrik Andersson
Aug 23 at 10:38
@FredrikAndersson - The rule $forall_i$ claims that if $varphi(x)$ is derivable then $forall x , varphi(x)$ is derivable, on the proviso that the variable $x$ does not occur free in any undischarged hypothesis (see for instance here, p. 32; or Van Dalen, Logic and Structure, 5th ed., 2012, p. 86). The idea is that if you can prove $varphi(x)$ without any specific assumption on $x$, then $varphi(x)$ holds for every $x$.
– Taroccoesbrocco
Aug 23 at 13:36
@FredrikAndersson - The rule $forall_i$ claims that if $varphi(x)$ is derivable then $forall x , varphi(x)$ is derivable, on the proviso that the variable $x$ does not occur free in any undischarged hypothesis (see for instance here, p. 32; or Van Dalen, Logic and Structure, 5th ed., 2012, p. 86). The idea is that if you can prove $varphi(x)$ without any specific assumption on $x$, then $varphi(x)$ holds for every $x$.
– Taroccoesbrocco
Aug 23 at 13:36
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%2f2889609%2fequivalence-in-natural-deduction-in-first-order-logic-2%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
