Mixing
Which one of the following equivalence is wrong [closed]
Clash Royale CLAN TAG#URR8PPP
up vote
2
down vote
favorite
$$ 1) forall z C(z,y) → B(t) iff forall z ( C(z,y) → B(t)) $$
$$ 2) forall z forall u (forall x A(x,u) → forall x B(x,z)) iff forall x forall u A(x,u) → forall z forall x B(x,z) $$
$$ 3) ¬ exists x P(x) iff forall x ¬P(x) $$
$$ 4) exists x P(x) & exists y B(y) iff exists y (exists x P(x) & B(y)) $$
Is it right that to check whether an equivalence is wrong or not, I have to prove that both $A→B$ and $B→ A$ holds or not.
According to my attempt of solving this problem the wrong one is $2$, but I'm not sure, as I'm new to first-order logic.
For the second one I've got:
$$ underline ∀x∀u A(x,u)→∀z∀x B(x,z) , ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) $$
$$ underline forall z forall x B(x,z), ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) , ⊢ forall x forall u A(x,u) $$
$$ underline forall z forall x B(x,z), ⊢ forall x A(x,t) → forall x B(x,r), ⊢ forall x forall u A(x,u) $$
$$ underline forall z forall x B(x,z), ⊢ forall x B(x,r), ... $$
$$ underline B(p,q), ⊢ forall x B(x,r) $$
$$ B(p,q), ⊢ B(p,r) $$
logic first-order-logic predicate-logic
asked Jul 27 at 20:37
Pavel Iljiev
754
closed as off-topic by Graham Kemp, amWhy, Adrian Keister, Brian Borchers, user223391 Jul 29 at 22:02
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Graham Kemp, amWhy, Adrian Keister, Brian Borchers, Community
add a comment |Â
up vote
2
down vote
favorite
$$ 1) forall z C(z,y) → B(t) iff forall z ( C(z,y) → B(t)) $$
$$ 2) forall z forall u (forall x A(x,u) → forall x B(x,z)) iff forall x forall u A(x,u) → forall z forall x B(x,z) $$
$$ 3) ¬ exists x P(x) iff forall x ¬P(x) $$
$$ 4) exists x P(x) & exists y B(y) iff exists y (exists x P(x) & B(y)) $$
Is it right that to check whether an equivalence is wrong or not, I have to prove that both $A→B$ and $B→ A$ holds or not.
According to my attempt of solving this problem the wrong one is $2$, but I'm not sure, as I'm new to first-order logic.
For the second one I've got:
$$ underline ∀x∀u A(x,u)→∀z∀x B(x,z) , ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) $$
$$ underline forall z forall x B(x,z), ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) , ⊢ forall x forall u A(x,u) $$
$$ underline forall z forall x B(x,z), ⊢ forall x A(x,t) → forall x B(x,r), ⊢ forall x forall u A(x,u) $$
$$ underline forall z forall x B(x,z), ⊢ forall x B(x,r), ... $$
$$ underline B(p,q), ⊢ forall x B(x,r) $$
$$ B(p,q), ⊢ B(p,r) $$
logic first-order-logic predicate-logic
asked Jul 27 at 20:37
Pavel Iljiev
754
closed as off-topic by Graham Kemp, amWhy, Adrian Keister, Brian Borchers, user223391 Jul 29 at 22:02
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Graham Kemp, amWhy, Adrian Keister, Brian Borchers, Community
2
According to what attempt? It is difficult to check something that isn't shown.
– Graham Kemp
Jul 27 at 22:05
I think you should consider what distributes and what does not.
– smokeypeat
Jul 28 at 12:13
add a comment |Â
up vote
2
down vote
favorite
up vote
2
down vote
favorite
$$ 1) forall z C(z,y) → B(t) iff forall z ( C(z,y) → B(t)) $$
$$ 2) forall z forall u (forall x A(x,u) → forall x B(x,z)) iff forall x forall u A(x,u) → forall z forall x B(x,z) $$
$$ 3) ¬ exists x P(x) iff forall x ¬P(x) $$
$$ 4) exists x P(x) & exists y B(y) iff exists y (exists x P(x) & B(y)) $$
Is it right that to check whether an equivalence is wrong or not, I have to prove that both $A→B$ and $B→ A$ holds or not.
According to my attempt of solving this problem the wrong one is $2$, but I'm not sure, as I'm new to first-order logic.
For the second one I've got:
$$ underline ∀x∀u A(x,u)→∀z∀x B(x,z) , ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) $$
$$ underline forall z forall x B(x,z), ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) , ⊢ forall x forall u A(x,u) $$
$$ underline forall z forall x B(x,z), ⊢ forall x A(x,t) → forall x B(x,r), ⊢ forall x forall u A(x,u) $$
$$ underline forall z forall x B(x,z), ⊢ forall x B(x,r), ... $$
$$ underline B(p,q), ⊢ forall x B(x,r) $$
$$ B(p,q), ⊢ B(p,r) $$
logic first-order-logic predicate-logic
asked Jul 27 at 20:37
Pavel Iljiev
754
$$ 1) forall z C(z,y) → B(t) iff forall z ( C(z,y) → B(t)) $$
$$ 2) forall z forall u (forall x A(x,u) → forall x B(x,z)) iff forall x forall u A(x,u) → forall z forall x B(x,z) $$
$$ 3) ¬ exists x P(x) iff forall x ¬P(x) $$
$$ 4) exists x P(x) & exists y B(y) iff exists y (exists x P(x) & B(y)) $$
Is it right that to check whether an equivalence is wrong or not, I have to prove that both $A→B$ and $B→ A$ holds or not.
According to my attempt of solving this problem the wrong one is $2$, but I'm not sure, as I'm new to first-order logic.
For the second one I've got:
$$ underline ∀x∀u A(x,u)→∀z∀x B(x,z) , ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) $$
$$ underline forall z forall x B(x,z), ⊢ ∀z∀u (∀x A(x,u)→∀x B(x,z)) , ⊢ forall x forall u A(x,u) $$
$$ underline forall z forall x B(x,z), ⊢ forall x A(x,t) → forall x B(x,r), ⊢ forall x forall u A(x,u) $$
$$ underline forall z forall x B(x,z), ⊢ forall x B(x,r), ... $$
$$ underline B(p,q), ⊢ forall x B(x,r) $$
$$ B(p,q), ⊢ B(p,r) $$
logic first-order-logic predicate-logic
asked Jul 27 at 20:37
Pavel Iljiev
754
edited Jul 28 at 9:28
asked Jul 27 at 20:37
Pavel Iljiev
754
asked Jul 27 at 20:37
Pavel Iljiev
754
asked Jul 27 at 20:37
Pavel Iljiev
754
754
closed as off-topic by Graham Kemp, amWhy, Adrian Keister, Brian Borchers, user223391 Jul 29 at 22:02
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Graham Kemp, amWhy, Adrian Keister, Brian Borchers, Community
closed as off-topic by Graham Kemp, amWhy, Adrian Keister, Brian Borchers, user223391 Jul 29 at 22:02
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Graham Kemp, amWhy, Adrian Keister, Brian Borchers, Community
2
According to what attempt? It is difficult to check something that isn't shown.
– Graham Kemp
Jul 27 at 22:05
I think you should consider what distributes and what does not.
– smokeypeat
Jul 28 at 12:13
add a comment |Â
2
According to what attempt? It is difficult to check something that isn't shown.
– Graham Kemp
Jul 27 at 22:05
I think you should consider what distributes and what does not.
– smokeypeat
Jul 28 at 12:13
2
2
According to what attempt? It is difficult to check something that isn't shown.
– Graham Kemp
Jul 27 at 22:05
According to what attempt? It is difficult to check something that isn't shown.
– Graham Kemp
Jul 27 at 22:05
I think you should consider what distributes and what does not.
– smokeypeat
Jul 28 at 12:13
I think you should consider what distributes and what does not.
– smokeypeat
Jul 28 at 12:13
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
0
down vote
accepted
Note, that since FOL is undecidable, there is no general way of answering such questions. In other words, the fact that you couldn't prove some formula does not entail that it is unprovable. Or, in yet other and more technically correct words, there are some unprovable first order formulas for which no counter model can be constructed effectively. Fortunately, this is not the case in your task.
Now, we want to "check" whether some of the following formulas are valid. For this task it is better to use analytic tableaux (there are many kinds of tableau calculi, so you may choose whichever you like the most) which are in fact means for constructing models. Putting a formula "into" a tableau and applying rules to it until no more are applicable yields either of the three following answers:
- formula is invalid (i.e. we failed to construct its model);
- formula is satisfiable (i.e. we constructed its model);
- the tableau does not end (we have come to neither of the previeous two conclusions because there is still and will always be a way to implement a rule, i.e. "until no more are applicable" is not the case).
Indeed, if you run the second formula through your tableaux caclulus of choice, you'll see that your tableau might not end (at least, it does not end in the version I've been taught).
But this alone does not prove that the fomula is falsifiable. What does, then? A countermodel does! So, let us build one.
Assume, our universe consists of five objects: $a$, $b$, $c$, $d$ and $e$ such that $forall x A(x,b)$, $neg A(c,e)$ and $neg B(d,a)$. Under this interpretation LHS is false (think, why) but RHS is true (again, think, why).
All other formulas can be easily proved in either a Hilbert style calculus or again using tableaux method.
answered Jul 29 at 19:31
Daniil Kozhemiachenko
1187
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
0
down vote
accepted
Note, that since FOL is undecidable, there is no general way of answering such questions. In other words, the fact that you couldn't prove some formula does not entail that it is unprovable. Or, in yet other and more technically correct words, there are some unprovable first order formulas for which no counter model can be constructed effectively. Fortunately, this is not the case in your task.
Now, we want to "check" whether some of the following formulas are valid. For this task it is better to use analytic tableaux (there are many kinds of tableau calculi, so you may choose whichever you like the most) which are in fact means for constructing models. Putting a formula "into" a tableau and applying rules to it until no more are applicable yields either of the three following answers:
- formula is invalid (i.e. we failed to construct its model);
- formula is satisfiable (i.e. we constructed its model);
- the tableau does not end (we have come to neither of the previeous two conclusions because there is still and will always be a way to implement a rule, i.e. "until no more are applicable" is not the case).
Indeed, if you run the second formula through your tableaux caclulus of choice, you'll see that your tableau might not end (at least, it does not end in the version I've been taught).
But this alone does not prove that the fomula is falsifiable. What does, then? A countermodel does! So, let us build one.
Assume, our universe consists of five objects: $a$, $b$, $c$, $d$ and $e$ such that $forall x A(x,b)$, $neg A(c,e)$ and $neg B(d,a)$. Under this interpretation LHS is false (think, why) but RHS is true (again, think, why).
All other formulas can be easily proved in either a Hilbert style calculus or again using tableaux method.
answered Jul 29 at 19:31
Daniil Kozhemiachenko
1187
add a comment |Â
up vote
0
down vote
accepted
Note, that since FOL is undecidable, there is no general way of answering such questions. In other words, the fact that you couldn't prove some formula does not entail that it is unprovable. Or, in yet other and more technically correct words, there are some unprovable first order formulas for which no counter model can be constructed effectively. Fortunately, this is not the case in your task.
Now, we want to "check" whether some of the following formulas are valid. For this task it is better to use analytic tableaux (there are many kinds of tableau calculi, so you may choose whichever you like the most) which are in fact means for constructing models. Putting a formula "into" a tableau and applying rules to it until no more are applicable yields either of the three following answers:
- formula is invalid (i.e. we failed to construct its model);
- formula is satisfiable (i.e. we constructed its model);
- the tableau does not end (we have come to neither of the previeous two conclusions because there is still and will always be a way to implement a rule, i.e. "until no more are applicable" is not the case).
Indeed, if you run the second formula through your tableaux caclulus of choice, you'll see that your tableau might not end (at least, it does not end in the version I've been taught).
But this alone does not prove that the fomula is falsifiable. What does, then? A countermodel does! So, let us build one.
Assume, our universe consists of five objects: $a$, $b$, $c$, $d$ and $e$ such that $forall x A(x,b)$, $neg A(c,e)$ and $neg B(d,a)$. Under this interpretation LHS is false (think, why) but RHS is true (again, think, why).
All other formulas can be easily proved in either a Hilbert style calculus or again using tableaux method.
answered Jul 29 at 19:31
Daniil Kozhemiachenko
1187
add a comment |Â
up vote
0
down vote
accepted
up vote
0
down vote
accepted
Note, that since FOL is undecidable, there is no general way of answering such questions. In other words, the fact that you couldn't prove some formula does not entail that it is unprovable. Or, in yet other and more technically correct words, there are some unprovable first order formulas for which no counter model can be constructed effectively. Fortunately, this is not the case in your task.
Now, we want to "check" whether some of the following formulas are valid. For this task it is better to use analytic tableaux (there are many kinds of tableau calculi, so you may choose whichever you like the most) which are in fact means for constructing models. Putting a formula "into" a tableau and applying rules to it until no more are applicable yields either of the three following answers:
- formula is invalid (i.e. we failed to construct its model);
- formula is satisfiable (i.e. we constructed its model);
- the tableau does not end (we have come to neither of the previeous two conclusions because there is still and will always be a way to implement a rule, i.e. "until no more are applicable" is not the case).
Indeed, if you run the second formula through your tableaux caclulus of choice, you'll see that your tableau might not end (at least, it does not end in the version I've been taught).
But this alone does not prove that the fomula is falsifiable. What does, then? A countermodel does! So, let us build one.
Assume, our universe consists of five objects: $a$, $b$, $c$, $d$ and $e$ such that $forall x A(x,b)$, $neg A(c,e)$ and $neg B(d,a)$. Under this interpretation LHS is false (think, why) but RHS is true (again, think, why).
All other formulas can be easily proved in either a Hilbert style calculus or again using tableaux method.
answered Jul 29 at 19:31
Daniil Kozhemiachenko
1187
Note, that since FOL is undecidable, there is no general way of answering such questions. In other words, the fact that you couldn't prove some formula does not entail that it is unprovable. Or, in yet other and more technically correct words, there are some unprovable first order formulas for which no counter model can be constructed effectively. Fortunately, this is not the case in your task.
Now, we want to "check" whether some of the following formulas are valid. For this task it is better to use analytic tableaux (there are many kinds of tableau calculi, so you may choose whichever you like the most) which are in fact means for constructing models. Putting a formula "into" a tableau and applying rules to it until no more are applicable yields either of the three following answers:
- formula is invalid (i.e. we failed to construct its model);
- formula is satisfiable (i.e. we constructed its model);
- the tableau does not end (we have come to neither of the previeous two conclusions because there is still and will always be a way to implement a rule, i.e. "until no more are applicable" is not the case).
Indeed, if you run the second formula through your tableaux caclulus of choice, you'll see that your tableau might not end (at least, it does not end in the version I've been taught).
But this alone does not prove that the fomula is falsifiable. What does, then? A countermodel does! So, let us build one.
Assume, our universe consists of five objects: $a$, $b$, $c$, $d$ and $e$ such that $forall x A(x,b)$, $neg A(c,e)$ and $neg B(d,a)$. Under this interpretation LHS is false (think, why) but RHS is true (again, think, why).
All other formulas can be easily proved in either a Hilbert style calculus or again using tableaux method.
answered Jul 29 at 19:31
Daniil Kozhemiachenko
1187
answered Jul 29 at 19:31
Daniil Kozhemiachenko
1187
answered Jul 29 at 19:31
Daniil Kozhemiachenko
1187
answered Jul 29 at 19:31
Daniil Kozhemiachenko
1187
1187
add a comment |Â
add a comment |Â
2
According to what attempt? It is difficult to check something that isn't shown.
– Graham Kemp
Jul 27 at 22:05
I think you should consider what distributes and what does not.
– smokeypeat
Jul 28 at 12:13