Mixing
Does this prove the validity of this First Order Logic formula?
up vote
3
down vote
favorite
Is this a valid proof for the following problem?
Prove:
$$models (exists x : A(x) to forall x : B(x)) to forall x : (A(x) to B(x))$$
Proof by contradiction:
Assume $(exists x: A(x) to forall x : B(x)) land lnot (forall x(A(x) to B(x))$
$ (lnot exists x : A(x) lor forall x : B(x)) land lnotforall x : (A(x) to B(x))$ logical equivalence
$forall x : lnot A(x) lor forall x : B(x)) land lnot(forall x : (A(x) to B(x))$ logical equivalence
$lnot A(a) lor B(a) land lnot((A(a) to B(a))$ instantiation
$((A(a) to B(a)) land lnot((A(a) to B(a))$ a contradiction
$therefore (exists x: A(x) to forall x : B(x)) to forall x(A(x) to B(x))$
Edit: corrected a typo on step 2
proof-verification logic first-order-logic
asked 2 days ago
OldGreg
214
New contributor
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
|
show 8 more comments
up vote
3
down vote
favorite
Is this a valid proof for the following problem?
Prove:
$$models (exists x : A(x) to forall x : B(x)) to forall x : (A(x) to B(x))$$
Proof by contradiction:
Assume $(exists x: A(x) to forall x : B(x)) land lnot (forall x(A(x) to B(x))$
$ (lnot exists x : A(x) lor forall x : B(x)) land lnotforall x : (A(x) to B(x))$ logical equivalence
$forall x : lnot A(x) lor forall x : B(x)) land lnot(forall x : (A(x) to B(x))$ logical equivalence
$lnot A(a) lor B(a) land lnot((A(a) to B(a))$ instantiation
$((A(a) to B(a)) land lnot((A(a) to B(a))$ a contradiction
$therefore (exists x: A(x) to forall x : B(x)) to forall x(A(x) to B(x))$
Edit: corrected a typo on step 2
proof-verification logic first-order-logic
asked 2 days ago
OldGreg
214
New contributor
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
3
Why on Earth is this downvoted? Sure, the user didn't use $LaTeX$, but come on! They're new!
– Shaun
2 days ago
Please use MathJax is future, @OldGreg.
– Shaun
2 days ago
@Shaun: It's not my downvote, but there's a loose group of users who don't like pure proof-verification questions and think they don't add value to the site.
– Henning Makholm
2 days ago
I am of the view that it is better to edit new contributor's work into mathjax rather then downvoting them for that.
– Q the Platypus
2 days ago
Same. I've started the hard parts of editing the mathjax into the post, but I'm a bit strapped on time. Finishing up the mathjax edits would be good editing practice if someone else is interested.
– Larry B.
2 days ago
|
show 8 more comments
up vote
3
down vote
favorite
up vote
3
down vote
favorite
Is this a valid proof for the following problem?
Prove:
$$models (exists x : A(x) to forall x : B(x)) to forall x : (A(x) to B(x))$$
Proof by contradiction:
Assume $(exists x: A(x) to forall x : B(x)) land lnot (forall x(A(x) to B(x))$
$ (lnot exists x : A(x) lor forall x : B(x)) land lnotforall x : (A(x) to B(x))$ logical equivalence
$forall x : lnot A(x) lor forall x : B(x)) land lnot(forall x : (A(x) to B(x))$ logical equivalence
$lnot A(a) lor B(a) land lnot((A(a) to B(a))$ instantiation
$((A(a) to B(a)) land lnot((A(a) to B(a))$ a contradiction
$therefore (exists x: A(x) to forall x : B(x)) to forall x(A(x) to B(x))$
Edit: corrected a typo on step 2
proof-verification logic first-order-logic
asked 2 days ago
OldGreg
214
New contributor
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
Is this a valid proof for the following problem?
Prove:
$$models (exists x : A(x) to forall x : B(x)) to forall x : (A(x) to B(x))$$
Proof by contradiction:
Assume $(exists x: A(x) to forall x : B(x)) land lnot (forall x(A(x) to B(x))$
$ (lnot exists x : A(x) lor forall x : B(x)) land lnotforall x : (A(x) to B(x))$ logical equivalence
$forall x : lnot A(x) lor forall x : B(x)) land lnot(forall x : (A(x) to B(x))$ logical equivalence
$lnot A(a) lor B(a) land lnot((A(a) to B(a))$ instantiation
$((A(a) to B(a)) land lnot((A(a) to B(a))$ a contradiction
$therefore (exists x: A(x) to forall x : B(x)) to forall x(A(x) to B(x))$
Edit: corrected a typo on step 2
proof-verification logic first-order-logic
proof-verification logic first-order-logic
asked 2 days ago
OldGreg
214
New contributor
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 2 days ago
OldGreg
214
New contributor
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
edited 23 hours ago
asked 2 days ago
OldGreg
214
New contributor
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 2 days ago
OldGreg
214
asked 2 days ago
OldGreg
214
214
New contributor
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
OldGreg is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
3
Why on Earth is this downvoted? Sure, the user didn't use $LaTeX$, but come on! They're new!
– Shaun
2 days ago
Please use MathJax is future, @OldGreg.
– Shaun
2 days ago
@Shaun: It's not my downvote, but there's a loose group of users who don't like pure proof-verification questions and think they don't add value to the site.
– Henning Makholm
2 days ago
I am of the view that it is better to edit new contributor's work into mathjax rather then downvoting them for that.
– Q the Platypus
2 days ago
Same. I've started the hard parts of editing the mathjax into the post, but I'm a bit strapped on time. Finishing up the mathjax edits would be good editing practice if someone else is interested.
– Larry B.
2 days ago
|
show 8 more comments
3
Why on Earth is this downvoted? Sure, the user didn't use $LaTeX$, but come on! They're new!
– Shaun
2 days ago
Please use MathJax is future, @OldGreg.
– Shaun
2 days ago
@Shaun: It's not my downvote, but there's a loose group of users who don't like pure proof-verification questions and think they don't add value to the site.
– Henning Makholm
2 days ago
I am of the view that it is better to edit new contributor's work into mathjax rather then downvoting them for that.
– Q the Platypus
2 days ago
Same. I've started the hard parts of editing the mathjax into the post, but I'm a bit strapped on time. Finishing up the mathjax edits would be good editing practice if someone else is interested.
– Larry B.
2 days ago
3
3
Why on Earth is this downvoted? Sure, the user didn't use $LaTeX$, but come on! They're new!
– Shaun
2 days ago
Why on Earth is this downvoted? Sure, the user didn't use $LaTeX$, but come on! They're new!
– Shaun
2 days ago
Please use MathJax is future, @OldGreg.
– Shaun
2 days ago
Please use MathJax is future, @OldGreg.
– Shaun
2 days ago
@Shaun: It's not my downvote, but there's a loose group of users who don't like pure proof-verification questions and think they don't add value to the site.
– Henning Makholm
2 days ago
@Shaun: It's not my downvote, but there's a loose group of users who don't like pure proof-verification questions and think they don't add value to the site.
– Henning Makholm
2 days ago
I am of the view that it is better to edit new contributor's work into mathjax rather then downvoting them for that.
– Q the Platypus
2 days ago
I am of the view that it is better to edit new contributor's work into mathjax rather then downvoting them for that.
– Q the Platypus
2 days ago
Same. I've started the hard parts of editing the mathjax into the post, but I'm a bit strapped on time. Finishing up the mathjax edits would be good editing practice if someone else is interested.
– Larry B.
2 days ago
Same. I've started the hard parts of editing the mathjax into the post, but I'm a bit strapped on time. Finishing up the mathjax edits would be good editing practice if someone else is interested.
– Larry B.
2 days ago
|
show 8 more comments
3 Answers
3
active
oldest
votes
up vote
1
down vote
In step 2 you make use of the equivalence
$neg(exists x . A(x) lor forall x.B(x)) iff forall x . neg A(x) ∨ forall x . B(x) $
This is not a real equivalence compare it to demorgans law.
$neg(exists x . A(x) lor forall x.B(x)) iff neg(exists x . A(x)) land neg(forall x.B(x))$
answered 2 days ago
Q the Platypus
2,754933
add a comment |
up vote
1
down vote
If you want a syntactic proof for a conditional statement, I suggest that you should use a Conditional Proof format.
So assume $exists x~A(x)toforall x~B(x)$ and do something to derive $forall x~(A(x)to B(x))$.
Then discharge the assumption with conditional introduction.
$deffitch#1#2{quadbegin{array}{|l} #1\hline #2end{array}}
fitch{}{fitch{1.~exists x~A(x)~to~forall x~B(x)}{fitch{~ldots}{~ddots}\8.~forall x~(A(x)to B(x))}\9.~(exists x~A(x)toforall x~B(x))toforall x~(A(x)to B(x))}$
answered yesterday
Graham Kemp
83.9k43378
add a comment |
up vote
1
down vote
Step 4 is wrong!
It looks like you instantiated all universals with an $a$, but you cannot do that when the universals are part of a larger sentence.
Consider: Suppose you have
$$neg forall x P(x) land neg forall x neg P(x)$$
Now, if we are allowed to just instantiate each of these universals with an $a$, we would get $neg P(a) land neg neg P(a)$, which is a contradiction. But, the orginal statement is not a contradiction at all; if we interpret $P(x)$ as '$x$ is even', and the domain is all numbers, then the original statement is obviously true.
Even more fundamentally, if you have $neg forall x P(x)$, you cannot fill in anything you want. Using the same interpretation as before, it is clear that $neg forall x P(x)$ is true, but $neg P(0)$ is not. So, you cannot instantiate a universal with anything you wany if it is being negated, but this is what you did when in step 4 you went from $neg forall x (A(x) rightarrow B(x))$ to $neg (A(a) rightarrow B(x))$
Step 2 is also wrong. The result of rewriting the conditional as an implication should be:
$(neg exists x A(x) lor forall x B(x)) land neg forall x (A(x) rightarrow B(x))$
Interestingly, given your step 2, step 3 is also wrong, as pointed out by @QthePlatypus, but with this corrected step 2, your step 3 actually would follow ... so maybe this was just a typo on your part?
answered yesterday
Bram28
58k44185
Thank you for the detailed example. I am a beginner, and I am still struggling with understanding when instantiation is allowed, I don't yet have a good strategy. It looks like a strategy might be to translate the line into informal English, in order to see whether or not instantiating will lead to a contradiction. Would a translation of your example be something like: "No number x is both even and not even."? If you know of any good resources, I would love more practice with quantifiers and instantiation, the more examples the better.
– OldGreg
yesterday
thanks again, I made the correction to step 2.
– OldGreg
yesterday
@oldgreg The official rule of instantiation is such that you can only use it when the whole statement is a universal. Any universal that is part of a larger statement cannit be instantiated.
– Bram28
yesterday
add a comment |
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
In step 2 you make use of the equivalence
$neg(exists x . A(x) lor forall x.B(x)) iff forall x . neg A(x) ∨ forall x . B(x) $
This is not a real equivalence compare it to demorgans law.
$neg(exists x . A(x) lor forall x.B(x)) iff neg(exists x . A(x)) land neg(forall x.B(x))$
answered 2 days ago
Q the Platypus
2,754933
add a comment |
up vote
1
down vote
In step 2 you make use of the equivalence
$neg(exists x . A(x) lor forall x.B(x)) iff forall x . neg A(x) ∨ forall x . B(x) $
This is not a real equivalence compare it to demorgans law.
$neg(exists x . A(x) lor forall x.B(x)) iff neg(exists x . A(x)) land neg(forall x.B(x))$
answered 2 days ago
Q the Platypus
2,754933
add a comment |
up vote
1
down vote
up vote
1
down vote
In step 2 you make use of the equivalence
$neg(exists x . A(x) lor forall x.B(x)) iff forall x . neg A(x) ∨ forall x . B(x) $
This is not a real equivalence compare it to demorgans law.
$neg(exists x . A(x) lor forall x.B(x)) iff neg(exists x . A(x)) land neg(forall x.B(x))$
answered 2 days ago
Q the Platypus
2,754933
In step 2 you make use of the equivalence
$neg(exists x . A(x) lor forall x.B(x)) iff forall x . neg A(x) ∨ forall x . B(x) $
This is not a real equivalence compare it to demorgans law.
$neg(exists x . A(x) lor forall x.B(x)) iff neg(exists x . A(x)) land neg(forall x.B(x))$
answered 2 days ago
Q the Platypus
2,754933
edited 2 days ago
answered 2 days ago
Q the Platypus
2,754933
answered 2 days ago
Q the Platypus
2,754933
answered 2 days ago
Q the Platypus
2,754933
2,754933
add a comment |
add a comment |
up vote
1
down vote
If you want a syntactic proof for a conditional statement, I suggest that you should use a Conditional Proof format.
So assume $exists x~A(x)toforall x~B(x)$ and do something to derive $forall x~(A(x)to B(x))$.
Then discharge the assumption with conditional introduction.
$deffitch#1#2{quadbegin{array}{|l} #1\hline #2end{array}}
fitch{}{fitch{1.~exists x~A(x)~to~forall x~B(x)}{fitch{~ldots}{~ddots}\8.~forall x~(A(x)to B(x))}\9.~(exists x~A(x)toforall x~B(x))toforall x~(A(x)to B(x))}$
answered yesterday
Graham Kemp
83.9k43378
add a comment |
up vote
1
down vote
If you want a syntactic proof for a conditional statement, I suggest that you should use a Conditional Proof format.
So assume $exists x~A(x)toforall x~B(x)$ and do something to derive $forall x~(A(x)to B(x))$.
Then discharge the assumption with conditional introduction.
$deffitch#1#2{quadbegin{array}{|l} #1\hline #2end{array}}
fitch{}{fitch{1.~exists x~A(x)~to~forall x~B(x)}{fitch{~ldots}{~ddots}\8.~forall x~(A(x)to B(x))}\9.~(exists x~A(x)toforall x~B(x))toforall x~(A(x)to B(x))}$
answered yesterday
Graham Kemp
83.9k43378
add a comment |
up vote
1
down vote
up vote
1
down vote
If you want a syntactic proof for a conditional statement, I suggest that you should use a Conditional Proof format.
So assume $exists x~A(x)toforall x~B(x)$ and do something to derive $forall x~(A(x)to B(x))$.
Then discharge the assumption with conditional introduction.
$deffitch#1#2{quadbegin{array}{|l} #1\hline #2end{array}}
fitch{}{fitch{1.~exists x~A(x)~to~forall x~B(x)}{fitch{~ldots}{~ddots}\8.~forall x~(A(x)to B(x))}\9.~(exists x~A(x)toforall x~B(x))toforall x~(A(x)to B(x))}$
answered yesterday
Graham Kemp
83.9k43378
If you want a syntactic proof for a conditional statement, I suggest that you should use a Conditional Proof format.
So assume $exists x~A(x)toforall x~B(x)$ and do something to derive $forall x~(A(x)to B(x))$.
Then discharge the assumption with conditional introduction.
$deffitch#1#2{quadbegin{array}{|l} #1\hline #2end{array}}
fitch{}{fitch{1.~exists x~A(x)~to~forall x~B(x)}{fitch{~ldots}{~ddots}\8.~forall x~(A(x)to B(x))}\9.~(exists x~A(x)toforall x~B(x))toforall x~(A(x)to B(x))}$
answered yesterday
Graham Kemp
83.9k43378
answered yesterday
Graham Kemp
83.9k43378
answered yesterday
Graham Kemp
83.9k43378
answered yesterday
Graham Kemp
83.9k43378
83.9k43378
add a comment |
add a comment |
up vote
1
down vote
Step 4 is wrong!
It looks like you instantiated all universals with an $a$, but you cannot do that when the universals are part of a larger sentence.
Consider: Suppose you have
$$neg forall x P(x) land neg forall x neg P(x)$$
Now, if we are allowed to just instantiate each of these universals with an $a$, we would get $neg P(a) land neg neg P(a)$, which is a contradiction. But, the orginal statement is not a contradiction at all; if we interpret $P(x)$ as '$x$ is even', and the domain is all numbers, then the original statement is obviously true.
Even more fundamentally, if you have $neg forall x P(x)$, you cannot fill in anything you want. Using the same interpretation as before, it is clear that $neg forall x P(x)$ is true, but $neg P(0)$ is not. So, you cannot instantiate a universal with anything you wany if it is being negated, but this is what you did when in step 4 you went from $neg forall x (A(x) rightarrow B(x))$ to $neg (A(a) rightarrow B(x))$
Step 2 is also wrong. The result of rewriting the conditional as an implication should be:
$(neg exists x A(x) lor forall x B(x)) land neg forall x (A(x) rightarrow B(x))$
Interestingly, given your step 2, step 3 is also wrong, as pointed out by @QthePlatypus, but with this corrected step 2, your step 3 actually would follow ... so maybe this was just a typo on your part?
answered yesterday
Bram28
58k44185
Thank you for the detailed example. I am a beginner, and I am still struggling with understanding when instantiation is allowed, I don't yet have a good strategy. It looks like a strategy might be to translate the line into informal English, in order to see whether or not instantiating will lead to a contradiction. Would a translation of your example be something like: "No number x is both even and not even."? If you know of any good resources, I would love more practice with quantifiers and instantiation, the more examples the better.
– OldGreg
yesterday
thanks again, I made the correction to step 2.
– OldGreg
yesterday
@oldgreg The official rule of instantiation is such that you can only use it when the whole statement is a universal. Any universal that is part of a larger statement cannit be instantiated.
– Bram28
yesterday
add a comment |
up vote
1
down vote
Step 4 is wrong!
It looks like you instantiated all universals with an $a$, but you cannot do that when the universals are part of a larger sentence.
Consider: Suppose you have
$$neg forall x P(x) land neg forall x neg P(x)$$
Now, if we are allowed to just instantiate each of these universals with an $a$, we would get $neg P(a) land neg neg P(a)$, which is a contradiction. But, the orginal statement is not a contradiction at all; if we interpret $P(x)$ as '$x$ is even', and the domain is all numbers, then the original statement is obviously true.
Even more fundamentally, if you have $neg forall x P(x)$, you cannot fill in anything you want. Using the same interpretation as before, it is clear that $neg forall x P(x)$ is true, but $neg P(0)$ is not. So, you cannot instantiate a universal with anything you wany if it is being negated, but this is what you did when in step 4 you went from $neg forall x (A(x) rightarrow B(x))$ to $neg (A(a) rightarrow B(x))$
Step 2 is also wrong. The result of rewriting the conditional as an implication should be:
$(neg exists x A(x) lor forall x B(x)) land neg forall x (A(x) rightarrow B(x))$
Interestingly, given your step 2, step 3 is also wrong, as pointed out by @QthePlatypus, but with this corrected step 2, your step 3 actually would follow ... so maybe this was just a typo on your part?
answered yesterday
Bram28
58k44185
Thank you for the detailed example. I am a beginner, and I am still struggling with understanding when instantiation is allowed, I don't yet have a good strategy. It looks like a strategy might be to translate the line into informal English, in order to see whether or not instantiating will lead to a contradiction. Would a translation of your example be something like: "No number x is both even and not even."? If you know of any good resources, I would love more practice with quantifiers and instantiation, the more examples the better.
– OldGreg
yesterday
thanks again, I made the correction to step 2.
– OldGreg
yesterday
@oldgreg The official rule of instantiation is such that you can only use it when the whole statement is a universal. Any universal that is part of a larger statement cannit be instantiated.
– Bram28
yesterday
add a comment |
up vote
1
down vote
up vote
1
down vote
Step 4 is wrong!
It looks like you instantiated all universals with an $a$, but you cannot do that when the universals are part of a larger sentence.
Consider: Suppose you have
$$neg forall x P(x) land neg forall x neg P(x)$$
Now, if we are allowed to just instantiate each of these universals with an $a$, we would get $neg P(a) land neg neg P(a)$, which is a contradiction. But, the orginal statement is not a contradiction at all; if we interpret $P(x)$ as '$x$ is even', and the domain is all numbers, then the original statement is obviously true.
Even more fundamentally, if you have $neg forall x P(x)$, you cannot fill in anything you want. Using the same interpretation as before, it is clear that $neg forall x P(x)$ is true, but $neg P(0)$ is not. So, you cannot instantiate a universal with anything you wany if it is being negated, but this is what you did when in step 4 you went from $neg forall x (A(x) rightarrow B(x))$ to $neg (A(a) rightarrow B(x))$
Step 2 is also wrong. The result of rewriting the conditional as an implication should be:
$(neg exists x A(x) lor forall x B(x)) land neg forall x (A(x) rightarrow B(x))$
Interestingly, given your step 2, step 3 is also wrong, as pointed out by @QthePlatypus, but with this corrected step 2, your step 3 actually would follow ... so maybe this was just a typo on your part?
answered yesterday
Bram28
58k44185
Step 4 is wrong!
It looks like you instantiated all universals with an $a$, but you cannot do that when the universals are part of a larger sentence.
Consider: Suppose you have
$$neg forall x P(x) land neg forall x neg P(x)$$
Now, if we are allowed to just instantiate each of these universals with an $a$, we would get $neg P(a) land neg neg P(a)$, which is a contradiction. But, the orginal statement is not a contradiction at all; if we interpret $P(x)$ as '$x$ is even', and the domain is all numbers, then the original statement is obviously true.
Even more fundamentally, if you have $neg forall x P(x)$, you cannot fill in anything you want. Using the same interpretation as before, it is clear that $neg forall x P(x)$ is true, but $neg P(0)$ is not. So, you cannot instantiate a universal with anything you wany if it is being negated, but this is what you did when in step 4 you went from $neg forall x (A(x) rightarrow B(x))$ to $neg (A(a) rightarrow B(x))$
Step 2 is also wrong. The result of rewriting the conditional as an implication should be:
$(neg exists x A(x) lor forall x B(x)) land neg forall x (A(x) rightarrow B(x))$
Interestingly, given your step 2, step 3 is also wrong, as pointed out by @QthePlatypus, but with this corrected step 2, your step 3 actually would follow ... so maybe this was just a typo on your part?
answered yesterday
Bram28
58k44185
edited yesterday
answered yesterday
Bram28
58k44185
answered yesterday
Bram28
58k44185
answered yesterday
Bram28
58k44185
58k44185
Thank you for the detailed example. I am a beginner, and I am still struggling with understanding when instantiation is allowed, I don't yet have a good strategy. It looks like a strategy might be to translate the line into informal English, in order to see whether or not instantiating will lead to a contradiction. Would a translation of your example be something like: "No number x is both even and not even."? If you know of any good resources, I would love more practice with quantifiers and instantiation, the more examples the better.
– OldGreg
yesterday
thanks again, I made the correction to step 2.
– OldGreg
yesterday
@oldgreg The official rule of instantiation is such that you can only use it when the whole statement is a universal. Any universal that is part of a larger statement cannit be instantiated.
– Bram28
yesterday
add a comment |
Thank you for the detailed example. I am a beginner, and I am still struggling with understanding when instantiation is allowed, I don't yet have a good strategy. It looks like a strategy might be to translate the line into informal English, in order to see whether or not instantiating will lead to a contradiction. Would a translation of your example be something like: "No number x is both even and not even."? If you know of any good resources, I would love more practice with quantifiers and instantiation, the more examples the better.
– OldGreg
yesterday
thanks again, I made the correction to step 2.
– OldGreg
yesterday
@oldgreg The official rule of instantiation is such that you can only use it when the whole statement is a universal. Any universal that is part of a larger statement cannit be instantiated.
– Bram28
yesterday
Thank you for the detailed example. I am a beginner, and I am still struggling with understanding when instantiation is allowed, I don't yet have a good strategy. It looks like a strategy might be to translate the line into informal English, in order to see whether or not instantiating will lead to a contradiction. Would a translation of your example be something like: "No number x is both even and not even."? If you know of any good resources, I would love more practice with quantifiers and instantiation, the more examples the better.
– OldGreg
yesterday
Thank you for the detailed example. I am a beginner, and I am still struggling with understanding when instantiation is allowed, I don't yet have a good strategy. It looks like a strategy might be to translate the line into informal English, in order to see whether or not instantiating will lead to a contradiction. Would a translation of your example be something like: "No number x is both even and not even."? If you know of any good resources, I would love more practice with quantifiers and instantiation, the more examples the better.
– OldGreg
yesterday
thanks again, I made the correction to step 2.
– OldGreg
yesterday
thanks again, I made the correction to step 2.
– OldGreg
yesterday
@oldgreg The official rule of instantiation is such that you can only use it when the whole statement is a universal. Any universal that is part of a larger statement cannit be instantiated.
– Bram28
yesterday
@oldgreg The official rule of instantiation is such that you can only use it when the whole statement is a universal. Any universal that is part of a larger statement cannit be instantiated.
– Bram28
yesterday
add a comment |
OldGreg is a new contributor. Be nice, and check out our Code of Conduct.
OldGreg is a new contributor. Be nice, and check out our Code of Conduct.
OldGreg is a new contributor. Be nice, and check out our Code of Conduct.
OldGreg is a new contributor. Be nice, and check out our Code of Conduct.
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
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3003048%2fdoes-this-prove-the-validity-of-this-first-order-logic-formula%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
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
Required, but never shown
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
Required, but never shown
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
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
3
Why on Earth is this downvoted? Sure, the user didn't use $LaTeX$, but come on! They're new!
– Shaun
2 days ago
Please use MathJax is future, @OldGreg.
– Shaun
2 days ago
@Shaun: It's not my downvote, but there's a loose group of users who don't like pure proof-verification questions and think they don't add value to the site.
– Henning Makholm
2 days ago
I am of the view that it is better to edit new contributor's work into mathjax rather then downvoting them for that.
– Q the Platypus
2 days ago
Same. I've started the hard parts of editing the mathjax into the post, but I'm a bit strapped on time. Finishing up the mathjax edits would be good editing practice if someone else is interested.
– Larry B.
2 days ago