Mixing
How this statement should be written?
Clash Royale CLAN TAG#URR8PPP
up vote
0
down vote
favorite
If I have a theorem/conjecture of the form "Let $n$ be an [object with some properties], then $P(n)$", how would it be written in logic ? So I have 2 variants:
1)$forall n in A, P(n)$.
2)$(nin A)to(P(n))$.
(By $A$ I mean a set of all such objects with some property).
So is one of my variants right ? Or it should be written in some other form ?
logic logic-translation
edited Aug 2 at 10:58
Bram28
54.5k33880
asked Aug 2 at 9:55
îріù ïрþш
979412
add a comment |Â
up vote
0
down vote
favorite
If I have a theorem/conjecture of the form "Let $n$ be an [object with some properties], then $P(n)$", how would it be written in logic ? So I have 2 variants:
1)$forall n in A, P(n)$.
2)$(nin A)to(P(n))$.
(By $A$ I mean a set of all such objects with some property).
So is one of my variants right ? Or it should be written in some other form ?
logic logic-translation
edited Aug 2 at 10:58
Bram28
54.5k33880
asked Aug 2 at 9:55
îріù ïрþш
979412
So it would be kind of equivalent ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:01
@MauroALLEGRANZA No I meant,are variants I have written equivalent ?Because in my second variant I have no quantifiers, or we can transform second variant using universal generalization ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:04
@MauroALLEGRANZA Yeah, now I realized that the second statement can be true some $n$ and false for the others, so I need "for all" claim anyway, thanks for explaining.
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:22
In so-called 'Agda notation' for dependent type theory, the notation $(n in A) to P(n)$ refers to the dependent product type $prod_n in A P(n)$, which corresponds with the proposition $forall n in A,,P(n)$ under the Curry-Howard correspondence. I'm leaving this as a comment rather than an answer because it would not be considered correct notation in mainstream mathematics.
– Clive Newstead
Aug 2 at 14:26
add a comment |Â
up vote
0
down vote
favorite
up vote
0
down vote
favorite
If I have a theorem/conjecture of the form "Let $n$ be an [object with some properties], then $P(n)$", how would it be written in logic ? So I have 2 variants:
1)$forall n in A, P(n)$.
2)$(nin A)to(P(n))$.
(By $A$ I mean a set of all such objects with some property).
So is one of my variants right ? Or it should be written in some other form ?
logic logic-translation
edited Aug 2 at 10:58
Bram28
54.5k33880
asked Aug 2 at 9:55
îріù ïрþш
979412
If I have a theorem/conjecture of the form "Let $n$ be an [object with some properties], then $P(n)$", how would it be written in logic ? So I have 2 variants:
1)$forall n in A, P(n)$.
2)$(nin A)to(P(n))$.
(By $A$ I mean a set of all such objects with some property).
So is one of my variants right ? Or it should be written in some other form ?
logic logic-translation
edited Aug 2 at 10:58
Bram28
54.5k33880
asked Aug 2 at 9:55
îріù ïрþш
979412
edited Aug 2 at 10:58
Bram28
54.5k33880
edited Aug 2 at 10:58
Bram28
54.5k33880
edited Aug 2 at 10:58
Bram28
54.5k33880
54.5k33880
asked Aug 2 at 9:55
îріù ïрþш
979412
asked Aug 2 at 9:55
îріù ïрþш
979412
asked Aug 2 at 9:55
îріù ïрþш
979412
979412
So it would be kind of equivalent ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:01
@MauroALLEGRANZA No I meant,are variants I have written equivalent ?Because in my second variant I have no quantifiers, or we can transform second variant using universal generalization ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:04
@MauroALLEGRANZA Yeah, now I realized that the second statement can be true some $n$ and false for the others, so I need "for all" claim anyway, thanks for explaining.
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:22
In so-called 'Agda notation' for dependent type theory, the notation $(n in A) to P(n)$ refers to the dependent product type $prod_n in A P(n)$, which corresponds with the proposition $forall n in A,,P(n)$ under the Curry-Howard correspondence. I'm leaving this as a comment rather than an answer because it would not be considered correct notation in mainstream mathematics.
– Clive Newstead
Aug 2 at 14:26
add a comment |Â
So it would be kind of equivalent ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:01
@MauroALLEGRANZA No I meant,are variants I have written equivalent ?Because in my second variant I have no quantifiers, or we can transform second variant using universal generalization ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:04
@MauroALLEGRANZA Yeah, now I realized that the second statement can be true some $n$ and false for the others, so I need "for all" claim anyway, thanks for explaining.
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:22
In so-called 'Agda notation' for dependent type theory, the notation $(n in A) to P(n)$ refers to the dependent product type $prod_n in A P(n)$, which corresponds with the proposition $forall n in A,,P(n)$ under the Curry-Howard correspondence. I'm leaving this as a comment rather than an answer because it would not be considered correct notation in mainstream mathematics.
– Clive Newstead
Aug 2 at 14:26
So it would be kind of equivalent ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:01
So it would be kind of equivalent ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:01
@MauroALLEGRANZA No I meant,are variants I have written equivalent ?Because in my second variant I have no quantifiers, or we can transform second variant using universal generalization ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:04
@MauroALLEGRANZA No I meant,are variants I have written equivalent ?Because in my second variant I have no quantifiers, or we can transform second variant using universal generalization ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:04
@MauroALLEGRANZA Yeah, now I realized that the second statement can be true some $n$ and false for the others, so I need "for all" claim anyway, thanks for explaining.
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:22
@MauroALLEGRANZA Yeah, now I realized that the second statement can be true some $n$ and false for the others, so I need "for all" claim anyway, thanks for explaining.
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:22
In so-called 'Agda notation' for dependent type theory, the notation $(n in A) to P(n)$ refers to the dependent product type $prod_n in A P(n)$, which corresponds with the proposition $forall n in A,,P(n)$ under the Curry-Howard correspondence. I'm leaving this as a comment rather than an answer because it would not be considered correct notation in mainstream mathematics.
– Clive Newstead
Aug 2 at 14:26
In so-called 'Agda notation' for dependent type theory, the notation $(n in A) to P(n)$ refers to the dependent product type $prod_n in A P(n)$, which corresponds with the proposition $forall n in A,,P(n)$ under the Curry-Howard correspondence. I'm leaving this as a comment rather than an answer because it would not be considered correct notation in mainstream mathematics.
– Clive Newstead
Aug 2 at 14:26
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
4
down vote
accepted
$(nin A)to P(n)$ is a good start, but you need something to express the idea that you want this to be true for all $n$. So you should write
$$ forall n : bigl[ nin A to P(n) bigr] $$
This is what "$forall nin A. P(n)$" (with variations in punctuation that don't carry any meaning) is usually considered to be an abbreviation for in formal logic.
answered Aug 2 at 11:08
Henning Makholm
225k16290516
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
4
down vote
accepted
$(nin A)to P(n)$ is a good start, but you need something to express the idea that you want this to be true for all $n$. So you should write
$$ forall n : bigl[ nin A to P(n) bigr] $$
This is what "$forall nin A. P(n)$" (with variations in punctuation that don't carry any meaning) is usually considered to be an abbreviation for in formal logic.
answered Aug 2 at 11:08
Henning Makholm
225k16290516
add a comment |Â
up vote
4
down vote
accepted
$(nin A)to P(n)$ is a good start, but you need something to express the idea that you want this to be true for all $n$. So you should write
$$ forall n : bigl[ nin A to P(n) bigr] $$
This is what "$forall nin A. P(n)$" (with variations in punctuation that don't carry any meaning) is usually considered to be an abbreviation for in formal logic.
answered Aug 2 at 11:08
Henning Makholm
225k16290516
add a comment |Â
up vote
4
down vote
accepted
up vote
4
down vote
accepted
$(nin A)to P(n)$ is a good start, but you need something to express the idea that you want this to be true for all $n$. So you should write
$$ forall n : bigl[ nin A to P(n) bigr] $$
This is what "$forall nin A. P(n)$" (with variations in punctuation that don't carry any meaning) is usually considered to be an abbreviation for in formal logic.
answered Aug 2 at 11:08
Henning Makholm
225k16290516
$(nin A)to P(n)$ is a good start, but you need something to express the idea that you want this to be true for all $n$. So you should write
$$ forall n : bigl[ nin A to P(n) bigr] $$
This is what "$forall nin A. P(n)$" (with variations in punctuation that don't carry any meaning) is usually considered to be an abbreviation for in formal logic.
answered Aug 2 at 11:08
Henning Makholm
225k16290516
edited Aug 2 at 14:22
answered Aug 2 at 11:08
Henning Makholm
225k16290516
answered Aug 2 at 11:08
Henning Makholm
225k16290516
answered Aug 2 at 11:08
Henning Makholm
225k16290516
225k16290516
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%2f2869896%2fhow-this-statement-should-be-written%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
So it would be kind of equivalent ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:01
@MauroALLEGRANZA No I meant,are variants I have written equivalent ?Because in my second variant I have no quantifiers, or we can transform second variant using universal generalization ?
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:04
@MauroALLEGRANZA Yeah, now I realized that the second statement can be true some $n$ and false for the others, so I need "for all" claim anyway, thanks for explaining.
– Ã®Ñ€Ñ–ù ïрþш
Aug 2 at 10:22
In so-called 'Agda notation' for dependent type theory, the notation $(n in A) to P(n)$ refers to the dependent product type $prod_n in A P(n)$, which corresponds with the proposition $forall n in A,,P(n)$ under the Curry-Howard correspondence. I'm leaving this as a comment rather than an answer because it would not be considered correct notation in mainstream mathematics.
– Clive Newstead
Aug 2 at 14:26