Mixing
Correct logical quantifier notation with greater than/less than relations
$begingroup$
I’m in the middle of some exercises for an intro to proofs class, and want to know if it is possible to write the following:
“For all real $n geq N$” as $(forall n in mathbb{R} geq N)$.
If that is incorrect syntax, I’d like to know the correct way!
logic proof-writing notation quantifiers
asked Feb 3 at 2:30
kusakusa
775
$endgroup$
add a comment |
$begingroup$
I’m in the middle of some exercises for an intro to proofs class, and want to know if it is possible to write the following:
“For all real $n geq N$” as $(forall n in mathbb{R} geq N)$.
If that is incorrect syntax, I’d like to know the correct way!
logic proof-writing notation quantifiers
asked Feb 3 at 2:30
kusakusa
775
$endgroup$
add a comment |
$begingroup$
I’m in the middle of some exercises for an intro to proofs class, and want to know if it is possible to write the following:
“For all real $n geq N$” as $(forall n in mathbb{R} geq N)$.
If that is incorrect syntax, I’d like to know the correct way!
logic proof-writing notation quantifiers
asked Feb 3 at 2:30
kusakusa
775
$endgroup$
I’m in the middle of some exercises for an intro to proofs class, and want to know if it is possible to write the following:
“For all real $n geq N$” as $(forall n in mathbb{R} geq N)$.
If that is incorrect syntax, I’d like to know the correct way!
logic proof-writing notation quantifiers
logic proof-writing notation quantifiers
asked Feb 3 at 2:30
kusakusa
775
asked Feb 3 at 2:30
kusakusa
775
asked Feb 3 at 2:30
kusakusa
775
asked Feb 3 at 2:30
kusakusa
775
asked Feb 3 at 2:30
kusakusa
775
775
add a comment |
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
While abbreviations like that may be used informally, they are usually not valid formal syntax. Most commonly, you would write $forall ninmathbb R(ngeq N to(dots))$ (or some minor notational variation of this). In fact, the $forall ninmathbb R(dots)$ is usually itself an informal abbreviation for $forall n.(ninmathbb R to (dots))$.
An alternative approach would be to use set builder notation and write $forall nin{xinmathbb Rmid xgeq N}(dots)$.
What exactly is valid depends on the exact formal notation you're using. I would not be surprised, though, if you haven't been given a clear, comprehensive description of the formal syntax you're supposed to be using. The above is based on common conventions, but conventions vary1. If you have been given a description of the formal syntax you're supposed to use, you can check yourself whether your translation is a well-formed formula with respect to that syntax.
I do recommend trying to stick to a clear syntax and not use abbreviations, especially undefined abbreviations, at least early on. It is quite common, for example, for people to not have a clear understanding of the abbreviation $exists xinmathbb R.P(x)$.
1 Eindhoven notation (as illustrated here, for example), explicitly covers this pattern of usage, and would lead to something like $(forall n:mathbb Rmid ngeq Nbullet(dots))$.
answered Feb 3 at 3:27
Derek ElkinsDerek Elkins
17.7k11437
$endgroup$
$begingroup$
Thank you for the very detailed response. It solved my problem, and I will definitely be referring to this in the future.
$endgroup$
– kusa
Feb 3 at 3:30
$begingroup$
I personally think it is a conceptual 'mistake' to treat restricted quantification as an abbreviation. The reason is not even that the symmetry is lost, i.e. $¬∀x∈S ( P(x) ) ≡ ∃x∈S ( ¬P(x) )$, but that the right way to think about mathematical objects is in a multi-sorted logic. I know that most texts on logic only deal with standard one-sorted first-order logic, and I know that multi-sorted logic can be encoded in one-sorted logic, but it seems to me that practically speaking it is conceptually better to use sorts to capture typing. Of course, there's nothing wrong with your answer. =)
$endgroup$
– user21820
Mar 4 at 15:02
add a comment |
$begingroup$
To add to Derek's answer, the restricted quantification syntax is "$∀x∈S ( P(x) )$" or "$∀x:S ( P(x) )$", where $S$ is a set/type and "$P(x)$" is a statement about $x$ that is meaningful in the context where $x∈S$. So we cannot have "$∀x∈mathbb{R}≥N ( ... )$". But we can have "$∀x∈mathbb{R}_{≥N} ( ... )$" after we define $mathbb{R}_{≥N} := { x : x∈mathbb{R} ∧ x≥N }$. This would be not only rigorous but also immediately understandable. Moreover, this syntax makes certain theorems short and elegant:
Strong induction: $∀m∈mathbb{N} ( ∀k∈mathbb{N}_{<m} ( P(k) ) ⇒ P(m) ) ⇒ ∀m∈mathbb{N} ( P(m) )$ for any property $P$ on $mathbb{N}$.
answered Mar 4 at 15:09
user21820user21820
40.3k544163
$endgroup$
$begingroup$
whoa, I can really appreciate this. probably would save lots of time on my tests as well!
$endgroup$
– kusa
Mar 4 at 16:59
add a comment |
Your Answer
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
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%2f3098086%2fcorrect-logical-quantifier-notation-with-greater-than-less-than-relations%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
While abbreviations like that may be used informally, they are usually not valid formal syntax. Most commonly, you would write $forall ninmathbb R(ngeq N to(dots))$ (or some minor notational variation of this). In fact, the $forall ninmathbb R(dots)$ is usually itself an informal abbreviation for $forall n.(ninmathbb R to (dots))$.
An alternative approach would be to use set builder notation and write $forall nin{xinmathbb Rmid xgeq N}(dots)$.
What exactly is valid depends on the exact formal notation you're using. I would not be surprised, though, if you haven't been given a clear, comprehensive description of the formal syntax you're supposed to be using. The above is based on common conventions, but conventions vary1. If you have been given a description of the formal syntax you're supposed to use, you can check yourself whether your translation is a well-formed formula with respect to that syntax.
I do recommend trying to stick to a clear syntax and not use abbreviations, especially undefined abbreviations, at least early on. It is quite common, for example, for people to not have a clear understanding of the abbreviation $exists xinmathbb R.P(x)$.
1 Eindhoven notation (as illustrated here, for example), explicitly covers this pattern of usage, and would lead to something like $(forall n:mathbb Rmid ngeq Nbullet(dots))$.
answered Feb 3 at 3:27
Derek ElkinsDerek Elkins
17.7k11437
$endgroup$
$begingroup$
Thank you for the very detailed response. It solved my problem, and I will definitely be referring to this in the future.
$endgroup$
– kusa
Feb 3 at 3:30
$begingroup$
I personally think it is a conceptual 'mistake' to treat restricted quantification as an abbreviation. The reason is not even that the symmetry is lost, i.e. $¬∀x∈S ( P(x) ) ≡ ∃x∈S ( ¬P(x) )$, but that the right way to think about mathematical objects is in a multi-sorted logic. I know that most texts on logic only deal with standard one-sorted first-order logic, and I know that multi-sorted logic can be encoded in one-sorted logic, but it seems to me that practically speaking it is conceptually better to use sorts to capture typing. Of course, there's nothing wrong with your answer. =)
$endgroup$
– user21820
Mar 4 at 15:02
add a comment |
$begingroup$
While abbreviations like that may be used informally, they are usually not valid formal syntax. Most commonly, you would write $forall ninmathbb R(ngeq N to(dots))$ (or some minor notational variation of this). In fact, the $forall ninmathbb R(dots)$ is usually itself an informal abbreviation for $forall n.(ninmathbb R to (dots))$.
An alternative approach would be to use set builder notation and write $forall nin{xinmathbb Rmid xgeq N}(dots)$.
What exactly is valid depends on the exact formal notation you're using. I would not be surprised, though, if you haven't been given a clear, comprehensive description of the formal syntax you're supposed to be using. The above is based on common conventions, but conventions vary1. If you have been given a description of the formal syntax you're supposed to use, you can check yourself whether your translation is a well-formed formula with respect to that syntax.
I do recommend trying to stick to a clear syntax and not use abbreviations, especially undefined abbreviations, at least early on. It is quite common, for example, for people to not have a clear understanding of the abbreviation $exists xinmathbb R.P(x)$.
1 Eindhoven notation (as illustrated here, for example), explicitly covers this pattern of usage, and would lead to something like $(forall n:mathbb Rmid ngeq Nbullet(dots))$.
answered Feb 3 at 3:27
Derek ElkinsDerek Elkins
17.7k11437
$endgroup$
$begingroup$
Thank you for the very detailed response. It solved my problem, and I will definitely be referring to this in the future.
$endgroup$
– kusa
Feb 3 at 3:30
$begingroup$
I personally think it is a conceptual 'mistake' to treat restricted quantification as an abbreviation. The reason is not even that the symmetry is lost, i.e. $¬∀x∈S ( P(x) ) ≡ ∃x∈S ( ¬P(x) )$, but that the right way to think about mathematical objects is in a multi-sorted logic. I know that most texts on logic only deal with standard one-sorted first-order logic, and I know that multi-sorted logic can be encoded in one-sorted logic, but it seems to me that practically speaking it is conceptually better to use sorts to capture typing. Of course, there's nothing wrong with your answer. =)
$endgroup$
– user21820
Mar 4 at 15:02
add a comment |
$begingroup$
While abbreviations like that may be used informally, they are usually not valid formal syntax. Most commonly, you would write $forall ninmathbb R(ngeq N to(dots))$ (or some minor notational variation of this). In fact, the $forall ninmathbb R(dots)$ is usually itself an informal abbreviation for $forall n.(ninmathbb R to (dots))$.
An alternative approach would be to use set builder notation and write $forall nin{xinmathbb Rmid xgeq N}(dots)$.
What exactly is valid depends on the exact formal notation you're using. I would not be surprised, though, if you haven't been given a clear, comprehensive description of the formal syntax you're supposed to be using. The above is based on common conventions, but conventions vary1. If you have been given a description of the formal syntax you're supposed to use, you can check yourself whether your translation is a well-formed formula with respect to that syntax.
I do recommend trying to stick to a clear syntax and not use abbreviations, especially undefined abbreviations, at least early on. It is quite common, for example, for people to not have a clear understanding of the abbreviation $exists xinmathbb R.P(x)$.
1 Eindhoven notation (as illustrated here, for example), explicitly covers this pattern of usage, and would lead to something like $(forall n:mathbb Rmid ngeq Nbullet(dots))$.
answered Feb 3 at 3:27
Derek ElkinsDerek Elkins
17.7k11437
$endgroup$
While abbreviations like that may be used informally, they are usually not valid formal syntax. Most commonly, you would write $forall ninmathbb R(ngeq N to(dots))$ (or some minor notational variation of this). In fact, the $forall ninmathbb R(dots)$ is usually itself an informal abbreviation for $forall n.(ninmathbb R to (dots))$.
An alternative approach would be to use set builder notation and write $forall nin{xinmathbb Rmid xgeq N}(dots)$.
What exactly is valid depends on the exact formal notation you're using. I would not be surprised, though, if you haven't been given a clear, comprehensive description of the formal syntax you're supposed to be using. The above is based on common conventions, but conventions vary1. If you have been given a description of the formal syntax you're supposed to use, you can check yourself whether your translation is a well-formed formula with respect to that syntax.
I do recommend trying to stick to a clear syntax and not use abbreviations, especially undefined abbreviations, at least early on. It is quite common, for example, for people to not have a clear understanding of the abbreviation $exists xinmathbb R.P(x)$.
1 Eindhoven notation (as illustrated here, for example), explicitly covers this pattern of usage, and would lead to something like $(forall n:mathbb Rmid ngeq Nbullet(dots))$.
answered Feb 3 at 3:27
Derek ElkinsDerek Elkins
17.7k11437
answered Feb 3 at 3:27
Derek ElkinsDerek Elkins
17.7k11437
answered Feb 3 at 3:27
Derek ElkinsDerek Elkins
17.7k11437
answered Feb 3 at 3:27
Derek ElkinsDerek Elkins
17.7k11437
17.7k11437
$begingroup$
Thank you for the very detailed response. It solved my problem, and I will definitely be referring to this in the future.
$endgroup$
– kusa
Feb 3 at 3:30
$begingroup$
I personally think it is a conceptual 'mistake' to treat restricted quantification as an abbreviation. The reason is not even that the symmetry is lost, i.e. $¬∀x∈S ( P(x) ) ≡ ∃x∈S ( ¬P(x) )$, but that the right way to think about mathematical objects is in a multi-sorted logic. I know that most texts on logic only deal with standard one-sorted first-order logic, and I know that multi-sorted logic can be encoded in one-sorted logic, but it seems to me that practically speaking it is conceptually better to use sorts to capture typing. Of course, there's nothing wrong with your answer. =)
$endgroup$
– user21820
Mar 4 at 15:02
add a comment |
$begingroup$
Thank you for the very detailed response. It solved my problem, and I will definitely be referring to this in the future.
$endgroup$
– kusa
Feb 3 at 3:30
$begingroup$
I personally think it is a conceptual 'mistake' to treat restricted quantification as an abbreviation. The reason is not even that the symmetry is lost, i.e. $¬∀x∈S ( P(x) ) ≡ ∃x∈S ( ¬P(x) )$, but that the right way to think about mathematical objects is in a multi-sorted logic. I know that most texts on logic only deal with standard one-sorted first-order logic, and I know that multi-sorted logic can be encoded in one-sorted logic, but it seems to me that practically speaking it is conceptually better to use sorts to capture typing. Of course, there's nothing wrong with your answer. =)
$endgroup$
– user21820
Mar 4 at 15:02
$begingroup$
Thank you for the very detailed response. It solved my problem, and I will definitely be referring to this in the future.
$endgroup$
– kusa
Feb 3 at 3:30
$begingroup$
Thank you for the very detailed response. It solved my problem, and I will definitely be referring to this in the future.
$endgroup$
– kusa
Feb 3 at 3:30
$begingroup$
I personally think it is a conceptual 'mistake' to treat restricted quantification as an abbreviation. The reason is not even that the symmetry is lost, i.e. $¬∀x∈S ( P(x) ) ≡ ∃x∈S ( ¬P(x) )$, but that the right way to think about mathematical objects is in a multi-sorted logic. I know that most texts on logic only deal with standard one-sorted first-order logic, and I know that multi-sorted logic can be encoded in one-sorted logic, but it seems to me that practically speaking it is conceptually better to use sorts to capture typing. Of course, there's nothing wrong with your answer. =)
$endgroup$
– user21820
Mar 4 at 15:02
$begingroup$
I personally think it is a conceptual 'mistake' to treat restricted quantification as an abbreviation. The reason is not even that the symmetry is lost, i.e. $¬∀x∈S ( P(x) ) ≡ ∃x∈S ( ¬P(x) )$, but that the right way to think about mathematical objects is in a multi-sorted logic. I know that most texts on logic only deal with standard one-sorted first-order logic, and I know that multi-sorted logic can be encoded in one-sorted logic, but it seems to me that practically speaking it is conceptually better to use sorts to capture typing. Of course, there's nothing wrong with your answer. =)
$endgroup$
– user21820
Mar 4 at 15:02
add a comment |
$begingroup$
To add to Derek's answer, the restricted quantification syntax is "$∀x∈S ( P(x) )$" or "$∀x:S ( P(x) )$", where $S$ is a set/type and "$P(x)$" is a statement about $x$ that is meaningful in the context where $x∈S$. So we cannot have "$∀x∈mathbb{R}≥N ( ... )$". But we can have "$∀x∈mathbb{R}_{≥N} ( ... )$" after we define $mathbb{R}_{≥N} := { x : x∈mathbb{R} ∧ x≥N }$. This would be not only rigorous but also immediately understandable. Moreover, this syntax makes certain theorems short and elegant:
Strong induction: $∀m∈mathbb{N} ( ∀k∈mathbb{N}_{<m} ( P(k) ) ⇒ P(m) ) ⇒ ∀m∈mathbb{N} ( P(m) )$ for any property $P$ on $mathbb{N}$.
answered Mar 4 at 15:09
user21820user21820
40.3k544163
$endgroup$
$begingroup$
whoa, I can really appreciate this. probably would save lots of time on my tests as well!
$endgroup$
– kusa
Mar 4 at 16:59
add a comment |
$begingroup$
To add to Derek's answer, the restricted quantification syntax is "$∀x∈S ( P(x) )$" or "$∀x:S ( P(x) )$", where $S$ is a set/type and "$P(x)$" is a statement about $x$ that is meaningful in the context where $x∈S$. So we cannot have "$∀x∈mathbb{R}≥N ( ... )$". But we can have "$∀x∈mathbb{R}_{≥N} ( ... )$" after we define $mathbb{R}_{≥N} := { x : x∈mathbb{R} ∧ x≥N }$. This would be not only rigorous but also immediately understandable. Moreover, this syntax makes certain theorems short and elegant:
Strong induction: $∀m∈mathbb{N} ( ∀k∈mathbb{N}_{<m} ( P(k) ) ⇒ P(m) ) ⇒ ∀m∈mathbb{N} ( P(m) )$ for any property $P$ on $mathbb{N}$.
answered Mar 4 at 15:09
user21820user21820
40.3k544163
$endgroup$
$begingroup$
whoa, I can really appreciate this. probably would save lots of time on my tests as well!
$endgroup$
– kusa
Mar 4 at 16:59
add a comment |
$begingroup$
To add to Derek's answer, the restricted quantification syntax is "$∀x∈S ( P(x) )$" or "$∀x:S ( P(x) )$", where $S$ is a set/type and "$P(x)$" is a statement about $x$ that is meaningful in the context where $x∈S$. So we cannot have "$∀x∈mathbb{R}≥N ( ... )$". But we can have "$∀x∈mathbb{R}_{≥N} ( ... )$" after we define $mathbb{R}_{≥N} := { x : x∈mathbb{R} ∧ x≥N }$. This would be not only rigorous but also immediately understandable. Moreover, this syntax makes certain theorems short and elegant:
Strong induction: $∀m∈mathbb{N} ( ∀k∈mathbb{N}_{<m} ( P(k) ) ⇒ P(m) ) ⇒ ∀m∈mathbb{N} ( P(m) )$ for any property $P$ on $mathbb{N}$.
answered Mar 4 at 15:09
user21820user21820
40.3k544163
$endgroup$
To add to Derek's answer, the restricted quantification syntax is "$∀x∈S ( P(x) )$" or "$∀x:S ( P(x) )$", where $S$ is a set/type and "$P(x)$" is a statement about $x$ that is meaningful in the context where $x∈S$. So we cannot have "$∀x∈mathbb{R}≥N ( ... )$". But we can have "$∀x∈mathbb{R}_{≥N} ( ... )$" after we define $mathbb{R}_{≥N} := { x : x∈mathbb{R} ∧ x≥N }$. This would be not only rigorous but also immediately understandable. Moreover, this syntax makes certain theorems short and elegant:
Strong induction: $∀m∈mathbb{N} ( ∀k∈mathbb{N}_{<m} ( P(k) ) ⇒ P(m) ) ⇒ ∀m∈mathbb{N} ( P(m) )$ for any property $P$ on $mathbb{N}$.
answered Mar 4 at 15:09
user21820user21820
40.3k544163
answered Mar 4 at 15:09
user21820user21820
40.3k544163
answered Mar 4 at 15:09
user21820user21820
40.3k544163
answered Mar 4 at 15:09
user21820user21820
40.3k544163
40.3k544163
$begingroup$
whoa, I can really appreciate this. probably would save lots of time on my tests as well!
$endgroup$
– kusa
Mar 4 at 16:59
add a comment |
$begingroup$
whoa, I can really appreciate this. probably would save lots of time on my tests as well!
$endgroup$
– kusa
Mar 4 at 16:59
$begingroup$
whoa, I can really appreciate this. probably would save lots of time on my tests as well!
$endgroup$
– kusa
Mar 4 at 16:59
$begingroup$
whoa, I can really appreciate this. probably would save lots of time on my tests as well!
$endgroup$
– kusa
Mar 4 at 16:59
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
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%2f3098086%2fcorrect-logical-quantifier-notation-with-greater-than-less-than-relations%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
